Shortest possible axiom for propositional calculus

[heiph...@wilsonb.com]

In the discussion below, Samiro mentioned ~ retbwax1, which got me looking at
~ meredith and friends:
https://groups.google.com/d/msgid/metamath/bc1cdba2626540ad8582917ddcec4d74%40rwth-aachen.de

The comment in ~ meredith mentions that it's "thought to be the shortest
possible axiom for propositional calculus", but then ~ merco1 and ~ merco2 go
on to show ones that appear shorter. Does the ~ meredith comment still apply,
and if so how is length of an axiom defined in this game?

[samiro.d...@rwth-aachen.de]

Meredith's axiom under https://us.metamath.org/mpeuni/meredith.html is a minimal axiom (one out of seven) in the Hilbert system with operators {→,¬} and modus ponens.

Since 2021, assuming general correctness of Walsh's and Fitelson's paper (which is still declared as under review), it has been proven by exhaustive search that it is indeed not only smallest-known, but minimal.

In contrast, https://us.metamath.org/mpeuni/merco1.html is a minimal axiom in the Hilbert system with operators { →, ⊥} and modus ponens.

Such things always depend on which operators and rule(s) of inference are allowed. There are propositional systems with even smaller axioms, but those systems are not even based on modus ponens, e.g.: https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/. (Note that all systems based on modus ponens must have formulas written in terms of →.)

I am researching systems of minimal axioms in terms of {→,¬} with open access at https://github.com/xamidi/pmGenerator/discussions/2 in case you are interested — you could even contribute to the project. On the project's main page I also wrote a few things about Metamath's propositional system of set.mm, which I called "Frege's calculus simplified by Łukasiewicz" due to its origin, and I used it as a default system for my tool.

[Gino Giotto]

> There are propositional systems with even smaller axioms, but those systems are not even based on modus ponens, e.g.: https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/.

So this is the linked single NAND axiom for propositional calculus by Stephen Wolfram:

((p·q)·r)·(p·((p·r)·p))=r

My question is: how would this translate into Metamath? The set.mm database does not introduce the primitive "=" symbol until ax-6, so we are not allowed to use its properties at that stage. Given how Metamath works, my guess is that you'll need more than one "$a |-" statement anyway.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/90b6ca2b-f4d5-442e-890d-ae85bcea56e1n%40googlegroups.com.

[Thierry Arnoux]

The `=` sign here is set.mm's biconditional `<->`and we would probably count it as a second operation, which needs to be defined, etc.

But maybe could encode it into two Metamath axioms:

${
    ax-1.1 $e |- ((p·q)·r)·(p·((p·r)·p))
    ax-1 $a |- r
$}

and

${
    ax-2.1 $e |- r
    ax-2 $a |- ((p·q)·r)·(p·((p·r)·p))
$}

_
Thierry

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAPKSAW5oD62rvGSbcsL4eJHbdxiOh4GaSdf7Cqq8B8s7DFz4Vw%40mail.gmail.com.

[Discher, Samiro]

I don't like NAND-based systems because they tend to have rather complicated rules of inference (which doesn't make them look fundamental, which is the whole point of single-axiom systems).
Whichever rule(s) Stephen Wolfram's system implicitly use(s), he didn't even write them down explicitly — apparently not aware that this is important, but possibly hiding the actual complex definition of the system.

His axiom written in Metamath's language is simply

|- (((ph -/\ ps) -/\ ch) -/\ (ph -/\ ((ph -/\ ch) -/\ ph))) <-> ch

in ASCII tokens (https://us.metamath.org/mpeuni/mmascii.html), or

⊢((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ))↔χ

in Unicode symbols.

---

Von: 'Thierry Arnoux' via Metamath <meta...@googlegroups.com>
Gesendet: Donnerstag, 6. Juni 2024 11:42:40
An: meta...@googlegroups.com; Gino Giotto
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus

 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4f007556-4d80-4b8c-934e-01c52e43ce26%40gmx.net.

[Discher, Samiro]

Corrections:

"Whichever rule(s) Stephen Wolfram's systems implicitly use [...] His minimal axiom written",

"|- ( ( ( ( ph -/\ ps) -/\ ch) -/\ (ph -/\ ((ph -/\ ch) -/\ ph ) ) ) <-> ch )",

"⊢(((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ))↔χ)"

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Discher, Samiro <samiro....@rwth-aachen.de>
Gesendet: Donnerstag, 6. Juni 2024 16:18:52
An: Gino Giotto; meta...@googlegroups.com
Betreff: AW: [Metamath] Re: Shortest possible axiom for propositional calculus

 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b32870b9c8b64b5cb90ee1b3fac08a24%40rwth-aachen.de.

[samiro.d...@rwth-aachen.de]

It was supposed to be ⊢((((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ)))↔χ) .

Since parentheses are messy and unnecessary: In normal Polish notation (which has no parentheses), the formula is just EDDDpqrDpDDprpr, which could also be written in terms of {¬,→} as

¬(((((p→¬q)→¬r)→¬(p→¬((p→¬r)→¬p)))→r)→¬(r→(((p→¬q)→¬r)→¬(p→¬((p→¬r)→¬p))))) [or NCCCCCpNqNrNCpNCCpNrNprNCrCCCpNqNrNCpNCCpNrNp in normal Polish notation]

in the way https://us.metamath.org/mmsolitaire/pmproofs.txt does it — this time converted by my program. :-)

[Gino Giotto]

>  Whichever rule(s) Stephen Wolfram's system implicitly use(s), he didn't even write them down explicitly — apparently not aware that this is important, but possibly hiding the actual complex definition of the system.

This is what makes me skeptical. By reading his post, he claims that his axiom is all you need, but this doesn't look right to me. Let's assume that his "=" is really the same thing as the metamath  "<-> " and go forward to prove all true propositional statements. Now let's say I want to prove the simple tautology "|-  ( ph -/\ ( ph -/\ ph ) )", to me it's immediately noticeable that this is impossible (in metamath), unless you add a rule of inference or other shorter axioms (in metamath there is no way to unify a goal with a statement that has more symbols than it).

Thierry second interpretation makes more sense to me. His "=" is not really the set.mm "<-> ", but rather a bidirectional version of our  "⇒", which is the symbol the website uses to express  the relashionship between hypothesis and conclusion (e.g. ax-mp:  ⊢ 𝜑  &  ⊢ (𝜑 → 𝜓)  ⇒  ⊢ 𝜓). In this interpretation his system would be composed of two rules of inferences and no axioms.

[Discher, Samiro]

> This is what makes me skeptical.

And rightfully so. These kind of systems with weird rules are a thing, as you can see for example at https://web.ics.purdue.edu/~dulrich/Twenty-six-open-questions-page.htm (where NAND is calleld "Sheffer's joint-denial operator") or https://en.wikipedia.org/wiki/Nicod%27s_axiom (which mentions a rule "Nicod's modus ponens"), but rules should indeed always be stated explicitly. Wolfram's article wouldn't pass peer review without modifications.

> Thierry second interpretation makes more sense to me.

But that one is definitely false since a rule with more than 0 premises is not an axiom, and furthermore he stated that his axiom has 15 symbols, i.e. "=" is a single operator.

Moreover, the point was to state a single-axiom system. But given that for handing both '<->' and '-/\' you most likely need multiple rules, the whole approach is moot. Since when using multiple rules you do not need *any* axioms for propositional logic (as we know, for example, from natural deduction systems).

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Gino Giotto <ginogiott...@gmail.com>
Gesendet: Donnerstag, 6. Juni 2024 17:16:50
An: Metamath

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/caf85902-88ae-4633-bad7-56ccbcaaa8a1n%40googlegroups.com.

[samiro.d...@rwth-aachen.de]

> he stated that his axiom has 15 symbols

Upon rereading Wolfram's articles (including https://www.wolfram.com/language/12/algebraic-computation/the-shortest-possible-axiom-for-boolean-logic.html), I couldn't even confirm this (I read them several years ago).

Claiming that one found "The Shortest Possible Axiom for Boolean Logic" without even stating for which rules of inference and how long the axiom is and by which metric seems rather chaotic and bold..

But the metric I assumed is used here: https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf

On page 3, Wolfram's single axiom is denoted as (Sh₁), and they write:

> Equation (Sh₁) is a member of a list of 25 candidates sent to us by Stephen Wolfram [17], who asked whether Otter could prove any of the candidates to be single axioms. [...]

> In Section 4 we show that (Sh₁), which has length 15, is a shortest single axiom in terms of the Sheffer stroke, and in Section 5 we narrow the list of possible length-15 Sheffer axioms to 16 candidates."

You could read that paper and references in order to understand what these systems really are.

[Mario Carneiro]

Wolfram's axiom is in "equational logic". That means that all theorems are of the form |- A = B, and the rules of inference are more or less:

* symmetry: If |- A = B then |- B = A

* instantiation: If |- A = B then |- A[sigma] = B[sigma] for any substitution sigma to the variables in A and B

* substitution: If |- A = B and |- C[A] = D[A] then |- C[B] = D[B] where C[_] and D[_] are contexts, i.e. terms with a hole in them which are filled by A and B respectively

For example, I asked FindEquationalProof to prove |- (a|a)|(a|a) = a from wolfram's axiom |- ((a|b)|c)|(a|((a|c)|a)) = c, and the first step was:

|- a|((a|b)|a) = b|((a|c)|(((a|c)|(a|((a|b)|a)))|(a|c)))

which is obtained from the rules above as:

1. |- ((a|b)|c)|(a|((a|c)|a)) = c   (axiom)

2. |- (((a|b)|c)|(a|((a|c)|a)))|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) = a|((a|c)|a)   (instantiate a -> a|b, b -> c, c -> a|((a|c)|a) in 1)
3. |- c|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) = a|((a|c)|a)   (substitute 1 in 2, with pattern _|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b))) = a|((a|c)|a))
4. |- a|((a|c)|a) = c|((a|b)|(((a|b)|(a|((a|c)|a)))|(a|b)))   (symmetry 3)
5. |- a|((a|b)|a) = b|((a|c)|(((a|c)|(a|((a|b)|a)))|(a|c)))   (instantiate a -> a, b -> c, c -> b)

(this is actually one step in wolfram's logic, which does certain operations like symmetry and bound variable renaming in zero steps).

This is a fundamentally different kind of logic from metamath's usual FOL style inferential system, where the proof goals are of the form |- phi and modus ponens is traditionally the main inference rule. See ql.mm (https://us.metamath.org/qleuni/mmtheorems1.html#ax-a1) for an example of an equational logic implemented in metamath.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0d6f9a46-fb9c-4ff8-916a-1f60b80eb5b1n%40googlegroups.com.

[Mario Carneiro]

On Thu, Jun 6, 2024 at 11:07 AM Gino Giotto <ginogiott...@gmail.com> wrote:

So this is the linked single NAND axiom for propositional calculus by Stephen Wolfram:

((p·q)·r)·(p·((p·r)·p))=r

My question is: how would this translate into Metamath?

To answer this question directly, here's a metamath axiomatization of wolfram's axiom system and a proof of step 1:

$c term wff |- = ( ) $.
$v p q r s ph $.
tp $f term p $.
tq $f term q $.
tr $f term r $.
ts $f term s $.
wph $f wff ph $.
weq $a wff p = q $. $( equality $)
tna $a term ( p q ) $. $( nand $)

${ symm.1 $e |- p = q $.
   symm $a |- q = p $. $}
${ trans.1 $e |- p = q $.  trans.2 $e |- q = r $.
   trans $a |- p = r $. $}
${ naeq.1 $e |- p = q $.  naeq.2 $e |- r = s $.
   naeq $a |- ( p r ) = ( q s ) $. $}

ax $a |- ( ( ( p q ) r ) ( p ( ( p r ) p ) ) ) = r $.

refl $p |- p = p $=
  ( tna ax symm trans ) AAABABZAFBBZAGAAAACZDHE $.

step1 $p |- ( p ( ( p q ) p ) ) = ( q ( ( p r ) ( ( ( p r ) ( p ( ( p q ) p ) ) ) ( p r ) ) ) ) $=
  ( tna ax symm refl naeq trans ) AABDADDZACDZBDJDZKKJDKDDZDZBMDNJKBJEFLBMMACBE
  MGHI $.

[Gino Giotto]

I could not have wished for a better answer. He does actually assume inferences about equality. So, we can't even formalize it in set.mm chapter about alternative axiom systems for propositional calculus at all.

[samiro.d...@rwth-aachen.de]

> So, we can't even formalize it in set.mm chapter about alternative axiom systems for propositional calculus at all.

Why not? What features are used by Wolfram's rules that cannot be described in Metamath language? Shouldn't propositional logic alone suffice (as I mentioned earlier), let alone ZFC?

[Gino Giotto]

> Why not? What features are used by Wolfram's rules that cannot be described in Metamath language? Shouldn't propositional logic alone suffice (as I mentioned earlier), let alone ZFC?

I am referring to the chapter called "Other axiomatizations related to classical propositional calculus", which appears before the properties about equality (and set theory) are introduced. To formalize Wolfram's system into that chapter, you have to find a way to eliminate/translate the equality inference rules (which I don't think it's possible).

Note that simply replacing the "=" with  "<->" will lead you to an incomplete system, because you have no way to derive a propositional statement where the "<->"  is not present. The tautology "|-  ( ph -/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) )" is not derivable for example. However, if you keep the "=" as a foreign symbol from classical propositional calculus then you can derive an equivalent formulation as "|-   ( ph -/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) )  = T." ("true" can be defined in terms of NAND).

you might say that replacing "=" with  "<->" would allow to derive "|-  ( ph -/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) )  <-> T." anyway, but the axioms in Mario's formalization would not provide all properties that you need to know the full behaviour of the classical biconditional operator.

In Wolfram's system the biconditional can be added with a conservative definition "|-  ( ph <-> ps ) = ( ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) -/\ ( ph -/\ ps ) )" and statements like  "|- ( ps <-> ph ) = ( ph <-> ps )" are derivable without issues. But what happens if I add a definition of biconditional when the symbol "<->" was already used in the system? Then I can now rewrite any biconditional into NAND operations, and eventually derive expressions that do not contain any biconditional. This was impossible before, therefore I didn't add a definition, I added an axiom, so my original axiomatic system was not sufficient to properly describe classical propositional calculus.

[Discher, Samiro]

> Note that simply replacing the "=" with  "<->" will lead you to an incomplete system, because you have no way to derive a propositional statement where the "<->"  is not present.

Using "<->" was what I proposed. I cannot follow your statement. When you have multiple rules that can do everything that is semantically defined by Boolean algebra, you sure can derive everything that semantically follows. The question is, why you wouldn't be able to define the required rules in Metamath (and prove them in set.mm based on only propositional primitives).

> the axioms in Mario's formalization would not provide all properties that you need to know the full behaviour of the classical biconditional operator

Which in set.mm is meaningless. All you need is to derive whichever rules are required (in Metamath such is called "Theorem" with an "Hypothesis"), but based on ax-1, ax-2, ax-3, ax-mp, df-bi, and df-nan (which includes df-an). How can this not be possible? If it is not, there must be a lack of expressiveness in the Metamath language, or Wolfram's "=" must do something that is not true for "<->". Since the propositional calculus is complete.

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Gino Giotto <ginogiott...@gmail.com>

Gesendet: Freitag, 7. Juni 2024 16:53:19
An: Metamath
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus

 

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fdfa1b17-a73c-41e7-b857-9af877a638c9n%40googlegroups.com.

[Gino Giotto]

Can you tell me how would you formalize Wolfram's axiom in Metamath without equality? (So that I can be sure we are on the same page).

[Discher, Samiro]

> Can you tell me how would you formalize Wolfram's axiom in Metamath without equality? (So that I can be sure we are on the same page).

"<->" / "=" is an equivalence relation, so reflexivity, transitivity and symmetry of it must be covered by rules. (https://en.wikipedia.org/wiki/Equivalence_relation#Definition)

Essentially, I would look at what Wolfram's system is able to do and introduce rules until they (in combination) can do everything that is required. Then also provide the axiom, and you're done.

I understood Mario's approach as doing just that, except that he provided a fundamental axiomatization, not one merely proven on top of another system (like set.mm).

If you are asking for technical details, sorry but I do not care enough about "Boolean algebra" to work these out. I think it is a complicated mess that has no pure logical character whatsoever (which is also why I think we would need several rules only to encode what "=" does). In particular, I think it is very hard and may even be impossible to provide an "elegant" axiomatization that doesn't need to combine a bunch of rules for what in Boolean algebra is considered a single step.

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Gino Giotto <ginogiott...@gmail.com>

Gesendet: Freitag, 7. Juni 2024 17:51:14

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/56b4641b-2f9a-4786-a04f-d5ec0d63f137n%40googlegroups.com.

[Gino Giotto]

> Essentially, I would look at what Wolfram's system is able to do and introduce rules until they (in combination) can do everything that is required. Then also provide the axiom, and you're done.

Well, that's the point. If you allow yourself to add as many rules as you want then you are formalizing something different than what the OTTER theorem prover was doing on page 7 and 8 of https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf and the what Wolfram showed about in the middle of the writing of https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ to prove the first Sheffer axiom.

>  If you are asking for technical details, sorry but I do not care enough about "Boolean algebra" to work these out. I think it is a complicated mess that has no pure logical character whatsoever

By the way, this is unrelated, but I know you are the person that created https://github.com/xamidi/pmGenerator/tree/1.2.0, and I wanted you to know that I tried your program a few weeks ago and I like it a lot. The metamath set.mm database does not really care about minimal proofs all the way back to the axioms, but I do. You might see me contributing some time in the future (particularly regarding the challenges of https://github.com/xamidi/pmGenerator/discussions/2).

[samiro.d...@rwth-aachen.de]

> Well, that's the point.

Didn't Mario do the same in his example? I might've just misunderstood this due to my lack in understanding of Metamath syntax, but his statement "this is actually one step in wolfram's logic, which does certain operations like symmetry and bound variable renaming in zero steps" seems to confirm that he used multiple steps in Metamath for a single step in Wolfram's system.

> If you allow yourself to add as many rules as you want then you are formalizing something different than what the OTTER theorem prover was doing on page 7 and 8 of https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf and the what Wolfram showed about in the middle of the writing of https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ to prove the first Sheffer axiom.

Only as many as required, but now you actually motivated me to look into some details in order to confirm my guesses. Their OTTER proofs(in https://www.cs.unm.edu/~mccune/papers/basax/DN-1.in) only used:

list(usable).

x = x.

% Denial of the Robbins basis.

B + A != A + B | (A + B) + C != A + (B + C) | ((A + B) @ + (A @ + B) @) @ != B | $Ans(Robbins_basis).

end_of_list.

The latter seems like an encoding of symmetry/commutativity, associativity and "Robbins". Note that due to it being a clause set, all but the last clauses are negated premises of a rule, but the conclusion is empty, so each of the premises is actually an axiom. So it makes sense that they have previously called this "3-basis {(Commutativity+),(Associativity+),(Robbins)}".

They did not specify any actual rules, but instead allowed resolution to occur. So their "proofs" are actually metaproofs to any imaginary Hilbert system (the kind of proof systems which Metamath can implement) of which they omitted details, which you have to define as you see fit when you are building one. This confirms my previous guesses. I don't know if there is any well-definedness in what they measure as a "single proof step", but translated in a Hilbert system, my guess is still that you need to combine multiple steps into one in order to count proof lengths like they do.

Of course, a correct definition must entail that syntactical consequences (which are independent of proof length) do not differ.

I might have totally missed your point here. I am really confused on where you take issue and why only now and not about Mario's solution, and after I already criticized what I'd consider the same issue.

>  By the way, this is unrelated, but I know you are the person that created https://github.com/xamidi/pmGenerator/tree/1.2.0, and I wanted you to know that I tried your program a few weeks ago and I like it a lot. [...] You might see me contributing some time in the future (particularly regarding the challenges of https://github.com/xamidi/pmGenerator/discussions/2).

Nice, thanks for the feedback! I currently have quite a contribution for w3 of the challenge in the making and I am still terribly failing with w2. (Though, I have an idea how to tackle it, but this is an implementation effort for which I need to make time).

I am looking forward to your findings. Which system(s) are you looking into?

> The metamath set.mm database does not really care about minimal proofs all the way back to the axioms, but I do.

But while .mm databases may not care about fundamental proof lengths (since they care about compressed proof size instead), it was the Metamath project that inspired all of my work on condensed detachment.

In an email correspondence with Norman Megill in 2020 I asked him about minimal proofs regarding set.mm, and he led me to Metamath's mmsolitaire project and inspired me to create pmGenerator with the following words:

"There is a separate project to find the "shortest after unfolding" proofs, i.e. shortest proofs directly from axioms, for the propositional calculus theorems in Principia Mathematica.  The page is here: http://us.metamath.org/mmsolitaire/pmproofs.txt
These proofs are shown in "condensed detachment" notation. [...]

For pmproofs.txt, the basic unification algorithm for proofs in D-notation is given as "Rule D" in the "A finitely axiomatized..." paper on the Metamath Home Page.  The program drule.c implements this in the function dAlgorithm(), which might provide hints if you want to write your own.  (The drule.c internals are a little rough and ad-hoc, originally intended for my personal experiments and not for public release.  It may be easier to write your own program rather than modify it.)"

When I figured out there wasn't even a single tool to fully parse condensed detachment proofs (but only Norman's version to compute final conclusions over proofs, and only supporting propositional axioms of set.mm), I felt there was a strong need for such a tool. I find the elegance and simplicity of condensed detachment very appealing, but apparently I mostly fail to inspire others.

[Mario Carneiro]

On Fri, Jun 7, 2024 at 6:07 PM Discher, Samiro <samiro....@rwth-aachen.de> wrote:

If you are asking for technical details, sorry but I do not care enough about "Boolean algebra" to work these out. I think it is a complicated mess that has no pure logical character whatsoever (which is also why I think we would need several rules only to encode what "=" does). In particular, I think it is very hard and may even be impossible to provide an "elegant" axiomatization that doesn't need to combine a bunch of rules for what in Boolean algebra is considered a single step.

The axiomatization I provided, based on wolfram's axiom, is complete for Boolean algebra already. That's exactly the point. I think you can be slightly more minimalistic and use euc instead of trans, as follows:

${ euc.1 $e |- p = q $.  euc.2 $e |- p = r $.
   euc $a |- q = r $. $}

${ naeq.1 $e |- p = q $.  naeq.2 $e |- r = s $.
   naeq $a |- ( p r ) = ( q s ) $. $}

ax $a |- ( ( ( p q ) r ) ( p ( ( p r ) p ) ) ) = r $.

refl $p |- p = p $=

  ( tna ax euc ) AABABZAEBBAAAAACZFD $.

${ symm.1 $e |- p = q $.

   symm $p |- q = p $=
     ( refl euc ) ABACADE $. $}

${ trans.1 $e |- p = q $.  trans.2 $e |- q = r $.

   trans $p |- p = r $=
     ( symm euc ) BACABDFEG $. $}

What it means to be "complete for boolean algebra" here is that metamath can prove |- ( ph <-> ps ) iff the above axiomatization can prove |- p = q, where p and q are the encodings of ph and ps as NAND formulas respectively.

> Can you tell me how would you formalize Wolfram's axiom in Metamath without equality? (So that I can be sure we are on the same page).

"<->" / "=" is an equivalence relation, so reflexivity, transitivity and symmetry of it must be covered by rules. (https://en.wikipedia.org/wiki/Equivalence_relation#Definition)

Essentially, I would look at what Wolfram's system is able to do and introduce rules until they (in combination) can do everything that is required.

Then also provide the axiom, and you're done.

I understood Mario's approach as doing just that, except that he provided a fundamental axiomatization, not one merely proven on top of another system (like set.mm).

 

The most natural way to do this in set.mm would be to simply take the equivalents of the above axioms as pseudo-axioms in a section, namely {bicomi,bitri} | bitr3i, nanbi12i, and wolfram (i.e. the axiom you get by transcribing 'ax' above using wnan and wbi).

To be clear, this axiom system will not be able to prove all theorems in propositional logic: it is quite obviously restricted to theorems of the form |- ( ph <-> ps ), and it is also language-restricted to only use formulas in terms of NAND unless you add some definitions. But we would say that propositional logic is a conservative extension of equational boolean algebra, since all the theorems in the image of the translation are provable iff they are provable in the equational logic.

If you wanted to stick something minimal on top of this system to make it complete for propositional logic, I would suggest adding some definitions to the source language:

* !p = p | p

* p /\ q = !(p | q)

* p -> q = p | !q

* p \/ q = !p -> q

* 1 = p \/ !p

and then using the inference rule  |- ( ph <-> T. ) ==> |- ph to allow interpreting proofs of the form |- p = 1 as playing the role of |- p (which is not otherwise well formed in equational logic). You can also add the following definition:

* (p <-> q) = (p -> q) /\ (q -> p)

but then you will want to prove |- (p <-> q) = 1  <==>  |- p = q to ensure conservativity (since the translation makes <-> and = the same thing and thus implicitly implies that these two are equivalent).

 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e754e9f197134a08b7b74774cd8173f4%40rwth-aachen.de.

[samiro.d...@rwth-aachen.de]

> but instead allowed resolution to occur

Oops, resolution and paramodulation, as noted on Otter's wiki article.

> The axiomatization I provided, based on wolfram's axiom, is complete for Boolean algebra already. [...] To be clear, this axiom system will not be able to prove all theorems in propositional logic: it is quite obviously restricted to theorems of the form |- ( ph <-> ps ) [...]

Ok, I might now understand what Gino was about. This is a great clarification!

I'd like to add that as long as the operators of a system are functionally complete and it proves all theorems over those formulas, the system implicitly proves all theorems in propositional logic, which can be taken as aliases, just like pmproofs.txt does it  — e.g. to prove *1.2:"((P v P) -> P)", one actually proves "((~ P -> P) -> P)".

For Boolean algebra over {⊼}, this could be solved by using something like x⊼(x⊼x)=f(ψ) as an alias for each propositional formula ψ, where f converts any propositional formula over any desired operators into a corresponding formula in terms of ⊼, e.g. f(⊤)= x⊼(x⊼x), f(a∨b)=(a⊼a)⊼(b⊼b), etc.

Metamath avoids implicit aliases by using "definitions" which are in fact axioms, since they introduce further symbols into the object language for convenience. Minimalistic deductive systems do not do this.

 >  By the way, this is unrelated, but I know you are the person that created https://github.com/xamidi/pmGenerator/tree/1.2.0 [...]

I should probably also note that version 1.2.0 was released 3 months ago, and https://github.com/xamidi/pmGenerator links to the current version (e.g. I recently added some nice graphical overviews to the readme file).

[Gino Giotto]

> I am looking forward to your findings. Which system(s) are you looking into?

For now I'll keep doing something simple, just to get more confidence with the tool. In the discussion https://github.com/xamidi/pmGenerator/discussions/2 I read that it should be easy to handle Walsh's fift axiom https://xamidi.github.io/pmGenerator/svg/walsh5th.svg, so I think I'll try to minimize the proof of "id" from it (since I also read that you exhausted the search up to 55 steps, but the shortest proof that you know of id is 65 steps, this means that even if I don't find anything, I could confirm that the current known proof is the shortest possible, which is interesting information).

My computer is relatively mediocre, but it's not the first time I stress it to do long running math related computations (like minimizing set.mm proofs, reducing

axioms in set.mm or excluding a composite number in GIMPS https://www.mersenne.org/).

>  Ok, I might now understand what Gino was about. This is a great clarification!

It was helpful for me as well to understand what Wolfram really meant.

[samiro.d...@rwth-aachen.de]

> I could confirm that the current known proof is the shortest possible

Finding a shorter proof may still be possible if you're lucky, but proving it to be minimal is very unlikely, unless you have massive amounts of resources at your hands:

Estimated from w5's data table, you would have to generate files with a combined size of around 404054704152 * 2.37^((63-55)/2) bytes, which are approx. 12.75 TB in order to cover all proofs up to lenght 63, which would ensure the 65-step proof is minimal.
Moreover, the final step alone would require pmGenerator around 2173.65*(2173.65 / 759.14)^4 ≈ 146103.49 core-h (i.e. around 16.67 years CPU-time) and 759.14*(759.14/320.89)^4 ≈ 23778.51 GiB of RAM, assuming that the exponential growth factors do not increase (which they probably do, so it most likely is even worse).

As you can see from w5's behavioral graph, most formulas quickly generated in w5 are insanely long, but this leads to making filtering really easy, which led to the short proofs of w5 at https://github.com/xamidi/pmGenerator/discussions/2#challenge-proofs without too much effort. This also means that w5's conclusions seem to be nicely distributed over the whole range of formulas. But since its known proofs are so small already, you have to be lucky to still find improvements, and minimal proofs might use very long formulas. So I'm not sure w5 is a good choice. Regardless of what you'll choose in the end, I wish you good luck and much success!

[Gino Giotto]

>  Estimated from w5's data table, you would have to generate files with a combined size of around 404054704152 * 2.37^((63-55)/2) bytes, which are approx. 12.75 TB in order to cover all proofs up to lenght 63, which would ensure the 65-step proof is minimal.

Nope, ok, definitely I should have looked at those data in the first place (you have a nice detailed documentation btw). I'll took some care to look at what seems promising. At the moment, this is really just an excuse to get a better hand at pmGenerator options and functionalities (basically the same thing I did for metamath).

[Gino Giotto]

> I'll took some care

*I'll take*

[Gino Giotto]

I think I found a shorter proof of  Łukasiewicz's second axiom (L2) from Walsh's second axiom (w2):

Statement of L2: CCNppp

My proof of L2: DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111

I verified this finding with the command:

pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111 -b -n -o L2.txt

Which generates a text file called "L2.txt" containing the output string: "1. CCNppp"

If I understand correctly, the output string should be the statement generated by the provided proof, written in Polish notation.  The table on https://github.com/xamidi/pmGenerator/discussions/2 reports that the shortest known proof of L2 from w2 is 781 steps long, while my proof is 535 steps long, so, if everything checks out, mine would be shorter.

@xamidi Does this seem correct to you?

The difficulty of Walsh's second axiom (w2) is rated as "horrible - 10/10" on pmGenerator Github page, so this would be a nice result :-)

[Discher, Samiro]

Yes, this is a w2: L2: 781↦535 improvement, congratulations!

Using

$ ./pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111 -s -n -o data/tmp.txt
$ ./pmGenerator --transform data/tmp.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -p -2 -d

reveals that CpCNpq is not part of the proof, so via combining the outputs of

$ ./pmGenerator --transform data/tmp.txt -f -n -t CpCqp,Cpp,CCNppp -j -1 -e
$ ./pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -e

this results in

$ ./pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse DDD11DDD11D11DDDDD111111DDDDD111111,DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D111,DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD1111111,DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111DDDDD1111111DDDD11DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111DDD1DDD11D1DDD11DDD1D111DDDDD1111111DDD11DDD1DDD1DD1D111111DDDDD1111111DDD1DDD1DDD1DDD1DDDDD111111D1111DDDDD1111111DDDDD1111111DDDDD111111DDDDD11111DDDDD1111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111 -s -n -o data/w2-tmp.txt

i.e.

    CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
[2] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
[3] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = D[2]1
[4] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[3]1
[5] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[4]
[6] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][4]
[7] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[1][4]
[8] CpCCNqCCNrsCNqCCNCtpuNCvCCwCvxCCNxCCNyzwCyxCrq = D[3][4]
[9] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][7]
[10] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1DD[5][0]11
[11] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[9]1
[12] Cpp = DD[0][6][4]
[13] CCpCCqqrCCNrCCNstpCsr = D1[12]
[14] CpCqCrCsCtq = DDDDD1DD[0][1][4]1[4]11
[15] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[14]1
[16] CpCqp = DD[15][0]1
[17] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[7]D[9][4]
[18] CpCNpq = D[17]1
[19] CpCqCrp = DD[0][9][14]
[20] CCNppp = DDDD[13]1DDD[0]DDD1[19][0][11]DDD1DDD[0]D1[10][4]DD[0][5][4]DDD1[15]1[4][8]1DDD[0][19]DDD1DD[0]D1[11]DD[0]DDD1DDD1[1]111[4]1DDD1DDD1D[10][4]1[4]1[4][8]1DDD1D[17]DD[0][2]DD[0]DDD1DDD1[6]111[4]1[13]D[6]DD1[16]1

combined for CpCqp,Cpp,CpCNpq,CCNppp, which can be written via

$ ./findCompactSummary data/w2-tmp.txt CpCqp,Cpp,CpCNpq,CCNppp

as

$ ./pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCqCrp

    CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CpCqCrp = DDD11DD11DDD1D111[0][2]
[6] CCNppp = DDDDD1[1]1DDDD11DDD1[5]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0]DDDDD11111[0]1DDDD11[5]DDD1DDD11D1DDD11DDD1D111[0]1DDD11DDD1DDD1DD1D111111[0]1DDD1DDD1DDD1DDD1[0]D1111[0]1[0]1[0]DDDDD11111[0]1DDD1DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1D1[1]DDDD11D11[0]DD1[3]1

in a more compact way.

Could you post your solution (and what you did, if you like) as a new answer in https://github.com/xamidi/pmGenerator/discussions/2?

Thank you for your contribution. :-)

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Gino Giotto <ginogiott...@gmail.com>

Gesendet: Donnerstag, 13. Juni 2024 19:39:30

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b61d2655-3593-4c33-85a8-036d1239e3c1n%40googlegroups.com.

[Discher, Samiro]

Correction:

Sorry, I messed up the part after

$ ./pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -e

which should of course use your proof instead of the old one, and 

$ ./pmGenerator --transform data/w2-tmp.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCqCrp

---

Von: Discher, Samiro
Gesendet: Donnerstag, 13. Juni 2024 20:07:33
An: Metamath
Betreff: AW: [Metamath] Re: Shortest possible axiom for propositional calculus

 

[Discher, Samiro]

So this leads to

$ ./pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse DDD11DDD11D11DDDDD111111DDDDD111111,DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D111,DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD1111111,DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111 -s -n -o data/w2-tmp.txt
[...]
$ ./pmGenerator --transform data/w2-tmp.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq -p -2 -d

    CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1

[5] CCNppp = DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDD1DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1D1[1]DDDD11D11[0]DD1[3]1

as a new compact solution, with debug output

There are 35 steps towards Cpp / C0.0 (index 8).
There are 53 steps towards CpCqp / C0C1.0 (index 12).
There are 57 steps towards CpCNpq / C0CN0.1 (index 14).
There are 535 steps towards CCNppp / CCN0.0.0 (index 15).

---

Von: Discher, Samiro
Gesendet: Donnerstag, 13. Juni 2024 20:14:01

[Steven Nguyen]

I don't know if this will help, but I found proofs of mpi and a1d from welsh's second axiom:
MM> show proof w2mpi
16     min=w2luk2  $p |- ( ( -. ps -> ps ) -> ps )
19     maj=w2ax1   $p |- ( ( ( -. ps -> ps ) -> ps ) -> ( -. ch -> ( ( -. ps ->
                                                               ps ) -> ps ) ) )
20   min=ax-mp   $a |- ( -. ch -> ( ( -. ps -> ps ) -> ps ) )
29     min=w2mpi.2 $e |- ( ps -> ( ph -> ch ) )
34       min=w2mpi.1 $e |- ph
40       maj=ax-w2   $a |- ( ph -> ( ( ps -> ( ph -> ch ) ) -> ( ( -. ch -> ( (
                                  -. ps -> ps ) -> ps ) ) -> ( ps -> ch ) ) ) )
41     maj=ax-mp   $a |- ( ( ps -> ( ph -> ch ) ) -> ( ( -. ch -> ( ( -. ps ->
                                             ps ) -> ps ) ) -> ( ps -> ch ) ) )
42   maj=ax-mp   $a |- ( ( -. ch -> ( ( -. ps -> ps ) -> ps ) ) -> ( ps -> ch )
                                                                              )
43 w2mpi=ax-mp $a |- ( ps -> ch )

MM> show proof w2a1d
17     min=w2luk2    $p |- ( ( -. ch -> ch ) -> ch )
20     maj=w2ax1     $p |- ( ( ( -. ch -> ch ) -> ch ) -> ( -. ps -> ( ( -. ch
                                                            -> ch ) -> ch ) ) )
21   w2mpi.1=ax-mp $a |- ( -. ps -> ( ( -. ch -> ch ) -> ch ) )
33       min=w2a1d.1   $e |- ( ph -> ps )
36       maj=w2ax1     $p |- ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )
37     w2mpi.1=ax-mp $a |- ( ch -> ( ph -> ps ) )
43     w2mpi.2=ax-w2 $a |- ( ph -> ( ( ch -> ( ph -> ps ) ) -> ( ( -. ps -> ( (
                                  -. ch -> ch ) -> ch ) ) -> ( ch -> ps ) ) ) )
44   w2mpi.2=w2mpi $p |- ( ph -> ( ( -. ps -> ( ( -. ch -> ch ) -> ch ) ) -> (
                                                                 ch -> ps ) ) )
45 w2a1d=w2mpi   $p |- ( ph -> ( ch -> ps ) )