Megill: A Finitely Axiomatized Formalization of ...

[Tony Häger]

I have read parts of the paper. I have two comments.

On page 9, lemmas L7 and L8 don't seem to be sufficient to be able to move two arbitrary disjuncts to the left. For instance from (a ∨ b)  ∨ (c ∨ d) I can't get to  (a ∨ c)  ∨ (b ∨ d).

On page 20, the proof for L11 can be shortened to "DDD21DD2S21S21D1DD211".

[Norman Megill]

On Friday, August 4, 2017 at 8:07:25 AM UTC-4, Tony wrote:

I have read parts of the paper. I have two comments.

On page 9, lemmas L7 and L8 don't seem to be sufficient to be able to move two arbitrary disjuncts to the left. For instance from (a ∨ b)  ∨ (c ∨ d) I can't get to  (a ∨ c)  ∨ (b ∨ d).

I should have included the other direction of associativity, call it L8a:

(L8a) ((P v (Q v R)) -> S) -> (((P v Q) v R) -> S)

However, I think it is possible to prove L8a from L7 and L8 if I didn't make a mistake.  I didn't concern myself with proof length below, and a shorter proof may be possible.  Applying L7 to embedded disjuncts like the first step P v (Q v R) to P v (R v Q) needs extra steps I didn't show.

P v (Q v R)
P v (R v Q)  L7
(R v Q) v P  L7
R v (Q v P)  L8
R v (P v Q)  L7
(P v Q) v R  L7
P v (Q v R)  L8
(Q v R) v P  L7
Q v (R v P)  L8
(R v P) v Q  L7
R v (P v Q)  L8
(P v Q) v R  L7

If you want to do a direct proof of L8a, I'll include it in the paper with an acknowledgment to you.  Hints can be obtained from the proofs on http://us.metamath.org/mmsolitaire/pmproofs.txt which for propositional calculus uses the same axioms and D-proof notation except for the "S" that abbreviates "DD2D1".

It might be useful as well to show the swapping of embedded disjuncts:

(L7a) (((P v Q) v R) -> S) -> (((Q v P) v R) -> S)

(The other nesting direction is obtained applying L7 before and after L7a.)

As for (a v b)  v  (c v d) to (a v c)  v (b v d), once you have L8a you can consult the set.mm proof of or4 for hints.

If you want to provide direct proofs of L8a and/or L7a, I will include them in the paper with an acknowledgment to you.

On page 20, the proof for L11 can be shortened to "DDD21DD2S21S21D1DD211".

Great!  I'll also mention this with an acknowledgment to you.

Thanks,
Norm

[Tony Häger]

On Fri, 4 Aug 2017 09:15:05 -0700 (PDT)

Norman Megill wrote:

> I should have included the other direction of 

>associativity, call it L8a:

> 

> (L8a) ((P v (Q v R)) -> S) -> (((P v Q) v R) -> S)

> It might be useful as well to show the swapping of 

>embedded disjuncts:

> 

> (L7a) (((P v Q) v R) -> S) -> (((Q v P) v R) -> S)

> 

Unfortunately, even with those two additional lemmas you can't rearrange more than three disjuncts to all possible configurations. I have tried it with a program that applies the rules to generate all reachable permutations. However, with more lemmas of the form:

L7a ((P∨Q)∨R⇒S)⇒((Q∨P)∨R⇒S)

L7b (((P∨Q)∨R)∨S⇒T)⇒(((Q∨P)∨R)∨S⇒T)

L7c ((((P∨Q)∨R)∨S)∨T⇒U)⇒((((Q∨P)∨R)∨S)∨T⇒U)

and

L8a (((P∨Q)∨R)∨S⇒T)⇒((P∨(Q∨R))∨S⇒T)

L8b ((((P∨Q)∨R)∨S)∨T⇒U)⇒(((P∨(Q∨R))∨S)∨T⇒U) 

it seems like all possible configurations can be generated. I have only tested it for up to five disjuncts. I Haven't found a proof of it.

The extended versions of L7 and L8 can be proved (from L7 and L8) by repeated use of:

 ((P⇒Q)⇒(R⇒Q))⇒((P∨S⇒Q)⇒(R∨S⇒Q))

which is proved by:  "SDS21DS21SDD23D11D2S31DDDDD22D12DS1DD22D11D1DD22D11S2SD2D-

12SD2D11SD2D12SD2D11DDDD22D11DS12S21DDDD22D11DS12S21DDD22D11DS12S31SDS21S3D-

S21DS3DD22D11S3S31DDDDD22D12DS1DD22D11D1DD22D11S2S1S21D2D11"

[Tony Häger]

After some more thinking and testing I have concluded that having two more lemmas is sufficient to move any two disjuncts to the far left.

L7  (P∨Q⇒R)⇒(Q∨P⇒R)

L8  ((P∨Q)∨R⇒S)⇒(P∨(Q∨R)⇒S)

L7a  ((P∨Q)∨R⇒S)⇒((Q∨P)∨R⇒S)

L8a  (((P∨Q)∨R)∨S⇒T)⇒((P∨(Q∨R))∨S⇒T)

It can be proved by induction on the number of disjuncts.

[Norman Megill]

Great!  If you wish to provide D-proofs of L7a and L8a, I will add them to the paper.

While you were looking at this, I thought of another approach, which is to add the converses of L5  that will split its disjunction into two theorems, which I may as well document here.

(L5a) ((P v Q) -> R) -> (P -> R)
(L5b) ((P v Q) -> R) -> (Q -> R)

Then we can work on the two parts of a complicated disjunction separately.  (With L5a and L5b, we can dispense with L7a.  While the other associativity direction L8a is optional, it will still be convenient to have so as not to have to repeat its long proof each time.)

Our final goal is to get the disjunction of some two variables, say P and Q, to be  the left-most disjunct in order to apply L9 or L10.  The order and nesting of the rest doesn't matter, since the antecedent is discarded by L11.  In the most general case, P and Q will be embedded into two halves of an outermost disjunction:

((...P...) v (...Q...)) -> R

Applying L5a and L5b, these become the pair

(...P...) -> R   and   (...Q...) -> R.

We work on each one separately (again breaking up disjunctions with L5a and L5b and recombining with L5 as needed) to move P and Q to the right to obtain

(P v (...)) -> R   and   (Q v (...)) -> R.

Combining these using L5, we have

((P v (...)) v (Q v (...))) -> R

and subsequently

(((P v (...)) v Q) v (...)) -> R  L8a
((P v (...)) v Q) -> R and (...) -> R  L5a,L5b
(Q v (P v (...))) -> R and (...) -> R  L7
((Q v P) v (...)) -> R and (...) -> R  L8a
(((Q v P) v (...)) v (...)) -> R  L5
((Q v P) v ((...) v (...))) -> R  L8

which prepares it for L10.

Another approach is to apply L7, L8, and L8a to make sure the P and Q above are always the leftmost disjuncts during the construction of the disjunction i.e. before we apply L5 or L6.

A shortcut applicable to all methods is to keep only two disjuncts, one containing a P and the other containing a Q, and discard all others with L5a and L5b during the construction.  This should greatly reduce the size of the final proof.

Norm

[Norman Megill]

I see your L8a isn't the reverse associativity I mentioned before.  Below when I mention L8a I mean the reverse associativity version.

Norm

[Tony Häger]

On Sat, 5 Aug 2017 11:05:28 -0700 (PDT)

Norman Megill wrote:

> Great! If you wish to provide D-proofs of L7a and L8a, 

>I will add them to 

> the paper.

L7a:   ((P∨Q)∨R⇒S)⇒((Q∨P)∨R⇒S)

DDDD22D11DS12S21DDDD22D11DS12S21DDDS21S3DS21DS3DD22D11S3S31DDDD22D11DS12S21DDD22D11S3S31S3DS21DS3DD22D11S3S31

L8a (my version):  (((P∨Q)∨R)∨S⇒T)⇒((P∨(Q∨R))∨S⇒T)

DSDS21DS21SDD23D11D2S31DDDDD22D12DS1DD22D11D1DD22D11S2SD2D12SD2D11SD2D12SD2D11DDDD22D11DS12S21DDDD22D11DS12S21DDD22D11DS12S31SDS21S3DS21DS3DD22D11S3S31DDDDD22D12DS1DD22D11D1DD22D11S2S1S21D2D11DD2S21D1SS3D2D1D3DD2S3S311SSDD22D11S12D2DDD21S3D21D1S3D2D1D3DD2S3S311

> 

> While you were looking at this, I thought of another 

>approach, which is to 

> add the converses of L5 that will split its disjunction 

>into two theorems, 

> which I may as well document here.

> 

> (L5a) ((P v Q) -> R) -> (P -> R)

> (L5b) ((P v Q) -> R) -> (Q -> R)

> 

> Then we can work on the two parts of a complicated 

>disjunction separately. 

It might be convenient to split the disjunktion completely and then force variables to become equal by detaching from

(P⇒Q)⇒((P⇒Q)⇒(P⇒Q))

and then form a disjunction only in the end and remove it with L11. This way L7 and L8 are not needed at all.

[Tony Häger]

I have found shorter proof strings for some more lemmas.

(L2)

DD2SSD2SD2D1DD2S3D2S311SDD2S21D1S3D2D1D3DD2S3S311S211D2D1SSD2S8DD28D3DD2S31SaSD4GDD2S95571S5SDD21bD4GSD3DD2S31SaSD4GDD2S95575D1S8S5SDD21bD4GSD3DD2S31SaSD4GDD2S95575

(L3)

DD2SSD2SD2D1DD2S3D2S311SDD2S21D1S3D2D1D3DD2S3S311S211D2D1SdS5SDD21bD4GSD3DD2S31SaSD4GDD2S95575D1ScS5SDD21bD4GSD3DD2S31SaSD4GDD2S95575

(L6)

DD2SSSDD22D11S12SD2D1SD2SD2D1DD2S3D2S311SDD2S21D1S3D2D1D3DD2S3S311S211S21D1S4D4GSD155D2D1SD2DDD21DD22D151DD2S21D15

(L7a): (((P∨Q)∨R)⇒S)⇒(((Q∨P)∨R)⇒S), shorter than the one a I posted before

DSD2S211DSD2S211DSS3SDD22D2S3S311D2D1D3DD2S3S311S3D2D1D3DD2S3S311

(L8): (((P⇒Q)∨R)⇒S)⇒((P⇒(Q∨R))⇒S)

DD2S21D1SS3D2D1D3DD2S3S311SSDD22D11S12D2D1S3D2D1D3DD2S3S311

(L8a) reverse associativity version: ((P⇒(Q∨R))⇒S)⇒(((P⇒Q)∨R)⇒S)

DSD2S211SD2D1S3D2D1D3DD2S3S311SSDD22D11S12S3D2D1D3DD2S3S311

(L8a, my version):  ((((P⇒Q)∨R)∨S)⇒T)⇒(((P⇒(Q∨R))∨S)⇒T), shorter than the one a I posted before

DSD2D1D2D1DD2S3D2S311DDSDD22D11S12S2SD2D12SD2D11SD2D12SD2D11DSD2S211DD2S21D1SD2S311SD2D1S3D2D1D3DD2S3S311DDSDD22D11S12S2S1S21D2D11DD2S21D1SS3D2D1D3DD2S3S311SSDD22D11S12D2D1S3D2D1D3DD2S3S311

(L11), shorter than the one a I posted before

DDD2S21D2D11D1DD211

((P⇒Q)⇒(R⇒Q))⇒(((P∨S)⇒Q)⇒((R∨S)⇒Q)), shorter than the one a I posted before

SD2D1D2D1DD2S3D2S311DDSDD22D11S12S2SD2D12SD2D11SD2D12SD2D11DSD2S211DD2S21D1SD2S311SD2D1S3D2D1D3DD2S3S311DDSDD22D11S12S2S1S21D2D11

[Norman Megill]

Nice work, thank you.  I will update the paper's pre-print with these soon.

Norm