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

Hi Stephan and Karolis,

Aah yes. Indeed, this need not be an axiom in TLA+ if I use the built-in implication. Thanks for pointing this out.

Similarly, there is indeed no need for extra facts to prove Thm3_84a above because TLAPS can prove all theorems of propositional logic directly. This is definitely a good thing for someone already familiar with formal logic that is trying to prove interesting things about algorithms, without having to redefine the foundations of mathematics.

It would however need to be an axiom if I had used a user-defined operator for implication, say '|-':

CONSTANT E(_)

AXIOM Leibniz == \A p,q : (p = q) |- (E(p) \equiv E(q))

The reason I am redefining basic operators is purely pedagogical, because I do not have familiarity with formal logic. I am starting with propositional logic and closely following the progression of "A logical approach to discrete mathematics" to develop intuitions about the equivalences between all operators, learn how formal logic is constructed, and how proofs are structured. The use of TLA+ and TLAPS in my case is not (yet) to prove interesting things about new algorithms, it is only to verify my proofs for already existing and well-established facts.

So far I do find the proof format of Lamport, and the use of TLA+ and TLAPS, a lot more approachable than the previous brief and unsuccessful attempt I had with Coq a decade ago, and the initial impression I had when looking at Isabelle a few weeks ago. That makes me think there is potential for teaching, to students who like myself, had an education that lacked sufficient exposure to logic and mathematics but are still eager to remedy the situation.

I hope that makes sense, and thanks again for your help, this is already quite helpful.

Best regards,

Erick

On Thu, May 8, 2025 at 12:05 PM Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:

Hi! This can be proved without introducing an axiom.

LEMMA ASSUME NEW a, NEW b, NEW E(_), a = b PROVE E(a) <=> E(b)
OBVIOUS

As well as

LEMMA ASSUME NEW E(_) PROVE \A a, b : a = b => E(a) <=> E(b)
OBVIOUS

Karolis

On Thu, May 8, 2025 at 12:15 PM 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.

--
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/CAFteovJqSmb4PekXC4%2BboPkhQX3EskwH8DiX0LBFOeQAER7%3DsQ%40mail.gmail.com.