(CW: mathematical logic.)
Current mood: looking up proof-theoretic treatments of linear temporal logic. (The LTL I encountered in university, primarily in concurrency-related courses, was approached model-theoretically and didn't describe how to prove program properties outside of brute force.)
Alas, it turns out that there are no finitistic (i.e. having decidable axioms) axiomatisations of LTL in general [Sz86]. (This should not be surprising, given that the model-theoretic definition of LTL relies upon the structure of the natural numbers, and hence that we encroach upon Gödelian territory.) It's unclear from my initial research whether this incompleteness result extends to the more restricted case of Boolean/propositional LTL with finite state.
In this post I consider two attempts to axiomatise the most important
properties of LTL in a way conducive to proving simple program properties, and show that despite their similar structure, one is a strict logical consequence of the other.
