Intuitionistic Metric Temporal Logic

on YouTube ↗27m

" summary

Defines Intuitionistic Metric Temporal Logic (IMTL) that extends intuitionistic temporal calculi to dense time with explicit intervals and gives every proof a computational meaning so proofs carry a moment-in-time and may only act at or move forward in time via a delay rule. Main theorem is syntactic cut elimination; cut reductions correspond to temporal interactions. Demonstrates modeling of a NOT gate with propagation and contamination delays and proves temporal causality plus temporal monotonicity; not yet a full programming language.

AI-written summary · about

" chapters (15)

1. 0:00Introduction
2. 1:09Hardware design example
3. 4:01Limitations of linear and metric temporal logic
4. 6:30Introducing intuitionistic metric temporal logic
5. 7:11Core concepts
6. 9:21Sequent calculus rules
7. 12:12Interval operator rules
8. 13:16Proving temporal propositions
9. 16:06Box and diamond connectives
10. 16:27Inverter gate modeling
11. 19:37Propagation and contamination delay
12. 20:01Cut elimination and meta theory
13. 21:50Temporal causality
14. 22:12Summary and future work
15. 23:19Questions and answers on branching and discrete time