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