| If I understand correctly what you mean, Leibniz substitution can be expressed as
LEMMA ASSUME NEW F(_), NEW x, NEW y, x = y PROVE F(x) = F(y)
which is proved by OBVIOUS.
For the rest, it looks to me that you are thinking about what is called a deep embedding of (propositional) logic in TLA+. This first requires defining a (set corresponding to the) inductive data type of formulas. There is no good support (yet) for such definitions in the TLAPS libraries, so you would probably have to inductively define a set of formulas of "size n", and then take their union, as in
makeForm(op, args) == [op |-> op, args |-> args] True == makeForm("T", << >>) Neg(f) == makeForm("neg", <<f>>) Equiv(f,g) == makeForm("equiv", <<f,g>>)
Form[n \in Nat] == IF n = 0 THEN {True} ELSE Form[n-1] \union { Neg(arg) : arg \in Form[n-1] } \union { Equiv(args[1], args[2]) : args \in Form[n-1] \X Form[n-1] }
Formula == UNION { Form[n] : n \in Nat }
You would then prove that formulas are closed under the application of operators:
LEMMA TrueFormula == True \in Formula
LEMMA NegFormula == ASSUME NEW f \in Formula PROVE Neg(f) \in Formula
LEMMA EquivFormula == ASSUME NEW f \in Formula, NEW g \in Formula PROVE Equiv(f,g) \in Formula
(Proving this will first require showing that Form is well-defined and also that Form[i] \subseteq Form[j] whenever i ≤ j._
You can then define the semantics of formulas
Interp[n \in Nat, f] == IF n = 0 THEN f = True \* assign TRUE to True, FALSE to everything else ELSE IF \in Form[n-1] THEN Interp[n-1, f] ELSE IF \E arg \in Form[n-1] : f = Neg(arg) THEN ~ Interp[n-1, arg] ELSE IF \E args \in Form[n-1] \X Form[n-1] : f = Equiv(args[1], args[2]) THEN Interp[n-1, args[1]] <=> Interp[n-1, args[2]] ELSE FALSE \* arbitrary
Interpretation(f) == LET n == CHOOSE n \in Nat : f \in Form[n] IN Interp[n, f]
and show that this is again well-behaved:
LEMMA ASSUME NEW f \in Formula PROVE Interpretation(f) \in BOOLEAN
LEMMA InterpTrue == Interpretation(True)
LEMMA InterpNeg == ASSUME NEW f \in Formula PROVE Interpretation(Neg(f)) = (~ Interpretation(f))
LEMMA InterpEquiv == ASSUME NEW f \in Formula, NEW g \in Formula PROVE Interpretation(Equiv(f,g)) = (Interpretation(f) <=> Interpretation(g))
After all this preparatory work, you will be able to prove the axioms, stated over interpretations of formulas: indeed there is no reason to expect, say,
AXIOM EqSym == \A p,q \in Form : (p \equiv q) \equiv (q \equiv p)
to hold, since elements of set Form are not Booleans.
However, this will be a lot of effort, and it is not clear to me if this effort is really well worth it?
Stephan
On 3 Apr 2025, at 17:38, Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:
Thanks both to @Calvin and @Stephen for your detailed answers. That was really useful. I also stumbled upon "Encoding TLA+ into unsorted and many-sorted first-order logic" ( https://doi.org/10.1016/j.scico.2017.09.004) from Stephen, with Section 3.1. on the liberal interpretation of Boolification of TLAPS that helped me understand why I could use propositional logic operators on variables whose possible values are elements of an unconstrained set. My end goal is to use TLAPS for proving properties of distributed algorithms. I do understand that I should avoid using custom axioms when doing so, for it could unintentionally hide errors. However, my background knowledge on formal mathematics and logic is somewhat lacking, so I am ramping up with the same tools I intend to use later, to validate my reasoning, practice the proof format advocated by Lamport, and learn the limitations of the tools.
I am impressed that all interesting theorems of propositional calculus from Gries and Schneider (1993) could be obviously proven with TLAPS, except for Leibniz substition (which I could not find how to express). That defeats my goal of verifying my hand proofs however because the Proof Manager succeeds at them regardless of which facts I am supplying to justify intermediate steps (so I cannot catch errors in mis-selecting relevant facts). I understand this is intentional: working engineers should not have to reprove basics of propositional calculus.
So in the last days, I have been experimenting with using the axioms given by Gries and Schneider (1993) with custom syntax / operators except for equivalence, in order to force the provers to work by re-writing. TLAPS successfully verifies the followings theorems from the book this way:
CONSTANT Form
True == <<"T">>
False == <<"F">>
Neg(f) == <<"neg", f>>
a ## b == Neg(a \equiv b)
AXIOM EqAssoc == \A p,q,r \in Form : ((p \equiv q) \equiv r) \equiv (p \equiv (q \equiv r))
AXIOM EqSym == \A p,q \in Form : (p \equiv q) \equiv (q \equiv p)
AXIOM EqIden == \A p \in Form : (True \equiv (p \equiv p))
THEOREM Thm3_4 ==
ASSUME NEW p \in Form
PROVE True
<1>1 True \equiv (True \equiv True)
BY EqIden
<1>2 (True \equiv True) \equiv (True \equiv (p \equiv p))
BY EqIden (* By replacing 2nd True with (p \equiv p) *)
<1>3 (True \equiv (p \equiv p))
BY EqIden (* Axiom *)
<1>z QED
BY <1>1,<1>2,<1>3
AXIOM NegDistrOverEq == \A p,q \in Form : Neg(p \equiv q) \equiv (Neg(p) \equiv q)
THEOREM Thm3_11 ==
ASSUME NEW p \in Form,
NEW q \in Form
PROVE (Neg(p) \equiv q) \equiv (p \equiv Neg(q))
<1>1 (Neg(p) \equiv q) \equiv Neg(p \equiv q)
BY NegDistrOverEq
<1>2 (p \equiv Neg(q)) \equiv Neg(p \equiv q)
<2>1 (p \equiv Neg(q)) \equiv (Neg(q) \equiv p)
BY EqSym
<2>2 (Neg(q) \equiv p) \equiv Neg(q \equiv p)
BY NegDistrOverEq
<2>3 Neg(q \equiv p) \equiv Neg(p \equiv q)
BY EqSym
<2>4 (Neg(p) \equiv q) \equiv Neg(p \equiv q)
BY NegDistrOverEq
<2>5 QED
BY <2>1, <2>2, <2>3, <2>4
<1>z QED
BY <1>1, <1>2, EqSym
However, I did not manage to restrict the "Form" set to only contain valid formulas (rather than being an unconstrained set). The various ways I have tried to define the infinite set of valid formulas seem to run into limitations of TLAPS.
I understand this is possible since Integers and Sequences are infinite sets themselves, but as far as I can tell they are defined in Isabelle rather TLA+. So is what I am trying possible?
Thanks again for your previous help, that was really useful.
Best regards,
Erick
LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n \div 2 = 0
fails
Well, fortunately TLAPS fails to prove this ... I meant to write
LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n % 2 = 0
which is indeed proved by OBVIOUS. Still, there are many intuitively obvious facts that TLAPS fails to prove: for example, it will not prove essentially any assertion involving the Cardinality operator.
Stephan
--
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 visit https://groups.google.com/d/msgid/tlaplus/e7535dbc-0eeb-49a4-ba50-aac7a35bc9dfn%40googlegroups.com.
--
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 visit https://groups.google.com/d/msgid/tlaplus/CAF6T5KoX_vLw_prW3LEzfE6tN0339FoxVE54KfOy0ByEbN0NiQ%40mail.gmail.com.
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 visit https://groups.google.com/d/msgid/tlaplus/31D77B61-9162-4F58-8F79-D28CBC8E42D2%40gmail.com.
|