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

Another way of trying to explain what I am doing is:

I am trying to figure out the minimum number of built-in operators I need to reuse to re-derive all interesting theorems of propositional logic, and verify the proofs I did by hand, so that the proof steps are only syntactic manipulation of equivalence formulas that closely follow the approach suggested by Gries and Schneider. But I do not want to define a deep logical embedding because defining the set of valid expressions, and an interpretation over those requires more advanced proof techniques than what I know already. (This is covered later in the same book, so by the end I think I should be able to.)

So far the required built-ins are:

- equivalence (\equiv)

- operator (Op(_)) to represent substitution

- constants to represent expressions

- universal quantifier (\A) to define axioms over all possible expressions

- user-defined operators to define the syntax of all propositional logic operators (True, False, Negation, Not equivalent, Disjonction, Conjunction, Implication)

- ASSUME NEW q, ... PROVE ... to express theorems

The proof techniques are simply chains of equivalences, until either once side of the theorem can be transformed into the other side, or the entire _expression_ can be reduced to an axiom. Aside from equivalences, I have had to use only two proof "techniques" when the prover had trouble:

1. "Focus"

ASSUME NEW u, NEW v, u \equiv v

PROVE E(u) \equiv E(v) (* where E(u) is an _expression_ containing u (but not v), etc.*)

BY E(u) \equiv E(v)

To focus the prover when the _expression_ that changed, but is equivalent, is buried in a sub-_expression_.

2. "Abstract"

<1> DEFINE u == ... (* where ... is a sub-_expression_ *)

<1> DEFINE v == ...

<1> HIDE DEF u,v

<2>1 Exp(u,v) \equiv Exp2(u,v) (* where Exp(u,v) is an _expression_ containing both u and v *)

....

<2> QED BY <2>1, ... DEF u,v

Which allows abstraction over sub-expressions to make it easier for the prover to unify with existing theorems, with later expansion of definitions after a step is shown to be true.

The interesting part to me is that doing so, the resulting proofs are really close to what one would have written by hand following the style of Gries and Schneider.

Pedagogically, regarding my goal of better understanding TLAPS on simpler examples: I ran into limitations of the prover in terms of the size of expressions that can be proven; I also noticed the difficulty for the prover to find a good sequence of symmetry and associativity transformations, to prove the steps. This is much easier to notice and debug when the statement that I am trying to prove looks obvious. Otherwise, if I had tried to do that on complicated algorithms already, then I would not know if what I am trying to prove is incorrect, or whether I am running into a limitation of the prover.

And regarding developing a familiarity regarding proof techniques, this approach also gave me first-hand experience on how some proof scan be laborious but not necessarily difficult, and also the joy of finding a clever way of reusing theorems to simplify proofs.

Maybe all I am saying looks obvious to those familiar with TLA+ and formal mathematics and proof techniques already, but to me, this is the first time I am actually enjoying learning all of this. I also feel confident learning this on my own because the prover helps me find mistakes. So I think there is something really neat about TLA+ and the associated tooling.

I hope again that will help clarify where I am going with this.

Best regards,

Erick

On Thu, May 8, 2025 at 3:02 PM Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:

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.