[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 26 Nov 2023 18:53:20 +0100*References*: <0d5368ca-6221-404a-a144-362e874a1431n@googlegroups.com> <6883916B-8B2D-426C-90C9-E7AC3781E981@gmail.com> <CAGNViOMZFg-7EEeH9xFMHGdoqiwVgXPq=kJ33d324Xm4T+GHHw@mail.gmail.com> <6178623B-7D82-4711-854B-26091E6EF685@gmail.com> <CAGNViONzco7vTcTobuMdVY24dYjUojSx7qvDfPRb3ABX9Q5xiw@mail.gmail.com>

Thanks for the nice explanations, and indeed I should have pointed you to Spot right away. I believe I now understand that what bothered you is a fundamental reasoning principle in modal / temporal logics, namely what logicians call the necessitation rule F |- []F It asserts that if F is a valid formula (true in all interpretations of interest) then so is []F. Indeed, if sigma |= F holds for all sequences of states sigma, then also sigma[n ..] |= F holds for all n (i.e., F is true for all suffixes of sigma), since every suffix sigma[n..] is again a sequence of states, and so sigma |= []F holds. However, quite obviously the implication F => []F is not valid, so in temporal reasoning you cannot equate implication and consequence, as we are used to from ordinary first-order logic. This is why Leslie keeps saying that temporal logic is evil. In TLAPS, "|-" is written ASSUME ... PROVE ..., and we wanted it to be the ordinary consequence relation from first-order logic because that's where 95% of the reasoning is done. When we designed how to handle the temporal logic part of TLA+, we debated adding a separate "temporal consequence" relation that could have been written []ASSUME ... []PROVE ... We decided that this would have been a complication that we didn't want to introduce. Instead, the PTL backend silently promotes every formula F that has been derived in a constant context (more generally, a context in which all assumptions are equivalent to formulas []G) to []F. The price to pay is that ASSUMEs with state- or action-level hypotheses are useless in contexts where temporal reasoning will be performed. However, you can freely use them in purely predicate-logic proof blocks. This explains the standard pattern in invariance proofs <1>1. Init => Inv <1>2. Inv /\ [Next]_v => Inv' \* stated as an implication because the step will be used in temporal reasoning <2>. SUFFICES ASSUME Inv, [Next]_v PROVE Inv' \* switch to ASSUME ... PROVE, since it is more useful for first-order reasoning <2>. QED <1>. QED BY <1>1, <1>2, PTL By the way, if you are more comfortable with applying proof rules, Leslie's proof rules in the original TLA paper [1] are a good starting point. They are mostly propositional and will therefore be understood by the PTL decision procedure without needing to apply them explicitly. Stephan
-- [1] http://lamport.azurewebsites.net/pubs/pubs.html#lamport-actions
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6567F8E6-380D-4637-97D9-97E50E0FE70D%40gmail.com. |

**References**:**[tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Ramon Snir

**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Stephan Merz

**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Ramon Snir

**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Stephan Merz

**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Ramon Snir

- Prev by Date:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Next by Date:
**[tlaplus] Re: Practice questions and answers for TLA+** - Previous by thread:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Next by thread:
**[tlaplus] Reddeadredemptionpcpassword** - Index(es):