145 views

Skip to first unread message

Aug 4, 2017, 8:07:25 AM8/4/17

to meta...@googlegroups.com

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".

Aug 4, 2017, 12:15:05 PM8/4/17

to Metamath

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

Aug 5, 2017, 9:15:34 AM8/5/17

to meta...@googlegroups.com

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"

Aug 5, 2017, 1:37:26 PM8/5/17

to meta...@googlegroups.com

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.

Aug 5, 2017, 2:05:28 PM8/5/17

to Metamath

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

Aug 5, 2017, 2:45:58 PM8/5/17

to Metamath

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

Norm

Norm

Aug 6, 2017, 9:17:56 AM8/6/17

to meta...@googlegroups.com

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.

Aug 8, 2017, 8:31:57 AM8/8/17

to meta...@googlegroups.com

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

Aug 8, 2017, 8:53:00 AM8/8/17

to Metamath

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

Norm

Norm

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu