Re: [tlaplus] Leibniz substitution as an axiom & TLA+/TLAPS for Introduction to Formal Logic

CONSTANT E(_)

THEOREM Leibniz == \A p,q : (p = q) => (E(p) \equiv E(q))

OBVIOUS

Similarly,

p && q == p /\ q

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 elided the parts of the proof that refer to facts that come from elsewhere.)

Stephan

On 8 May 2025, at 11:14, Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:

Dear all,

This is a quick note, in case anybody else were to try to use TLAPS, only for checking correct syntactic manipulations (without deep logic embedding), when practicing writing equivalence proofs, in the style advocated in "A Logical Approach to Discrete Mathematics".

I have figured out how to write Leibniz substitution as an axiom:

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

--
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/CAF6T5KoC9%2BKZ2axkZkXHP%3Dsq1JLz4ozseeFPo%2BBPJQrOVF2M0A%40mail.gmail.com.