CONSTANT E(_)
AXIOM Leibniz == \A p,q : (p = q) => (E(p) \equiv E(q))
Implicitly, E refers to boolean expressions of propositional logic, in which a variable might be substituted for another variable, passed as argument to E in TLA+. However, we do not define E explicitly, we only use it to verify our manipulation steps, as in the following example:
THEOREM Thm3_84a ==
ASSUME NEW e, NEW f
PROVE (e = f) && E(e) \equiv (e = f) && E(f)
<1>1 ((e = f) && E(e) \equiv (e = f) && E(f)) \equiv
((e = f) && (E(e) \equiv E(f)) \equiv (e = f))
<2> DEFINE t == (e = f)
<2> DEFINE u == E(e)
<2> DEFINE v == E(f)
<2> HIDE DEF u,v,t
<2>1 t && (u \equiv v) \equiv (t && u \equiv (t && v \equiv t))
BY Thm3_49
<2>2 (t && (u \equiv v) \equiv (t && u \equiv (t && v \equiv t))) \equiv
((t && u \equiv t && v) \equiv (t && (u \equiv v) \equiv t))
BY EqAssoc
<2> QED BY <2>1, <2>2 DEF t, u, v
<1>2 @ \equiv ((e = f) => (E(e) \equiv E(f)))
BY ImplDef3
<1> QED BY <1>1, <1>2, Leibniz
I think it is pretty neat that TLA+ and TLAPS can validate those manipulation, in a way that is really close to what one would write by hand.
This was the last puzzle to solve to prove all theorems of propositional logics in the book I am using. This allowed me to teach myself, and automatically verify all my proofs, with minimal guidance and without requiring someone else to manually go over my proofs to validate.
Would there be any interest, if I were to write that as a short paper, to explain how to use TLA+ and TLAPS for that purpose? I think that could be a good reference for students and maybe for using TLA+ and TLAPS in teaching introductory courses to formal logic.
Best regards,
Erick