search

nomeata / incredible

The Incredible Proof Machine
MIT License
358 stars 36 forks source link

Add more tasks to hilbert system #101

Closed yuxuanchiadm closed 5 years ago

yuxuanchiadm commented 5 years ago

So solving "Law of Excluded Middle" will be easier by creating custom blocks. And composing proofs to bigger proof. :p

yuxuanchiadm commented 5 years ago

Related to #100

nomeata commented 5 years ago

@lohner I think you originally added the Hilbert system. Do you want to review this contribution?

lohner commented 5 years ago

Good work solving these really tough tasks @yuxuanchiadm :clap:

I don't remember being the one who added the Hilbert session though.... :man_shrugging:

However, the tasks should definitely be solvable (from a theoretic point of view - I didn't try to solve them). And I suspect that at least some of them could be used well for solving task 3 of that session. I therefore suggest to approximately order the tasks according to difficulty.

Further, I am sure you solved all of them @yuxuanchiadm. So it would be nice if you also added some min block counts to the tasks of this session.

alreadydone commented 5 years ago

You should be able to fetch min-blocks counts from http://us.metamath.org/mmsolitaire/pmproofs.txt and I think they're hard to beat...

alreadydone commented 5 years ago

Also check out https://i.stack.imgur.com/zpFi0.png from https://codegolf.stackexchange.com/a/170881/74466 from this thread (cool genetic algorithm to shorten proofs).

I think counting custom blocks as just one block makes things more fun; this is essentially what Terry Tao does in his QED. The following is a proof that uses commutativity and left associativity of AND, both "custom blocks" proved before. It's just one line shorter than the naive approach. If you expand the proofs of commutativity and left associativity then of course you get much more than 7 lines.

A AND (B AND C). [given]
From A AND (B AND C): deduce (B AND C) AND A. [AND IS COMMUTATIVE]
From (B AND C) AND A: deduce B AND (C AND A). [AND IS ASSOCIATIVE (left)]
From B AND (C AND A): deduce (C AND A) AND B. [AND IS COMMUTATIVE]
From (C AND A) AND B: deduce C AND (A AND B). [AND IS ASSOCIATIVE (left)]
From C AND (A AND B): deduce (A AND B) AND C. [AND IS COMMUTATIVE]
QED!
yuxuanchiadm commented 5 years ago

Just reordered tasks and add my block count as min blocks .

yuxuanchiadm commented 5 years ago

Actually if someone can translate proofs from http://us.metamath.org/mmsolitaire/pmproofs.txt to http://incredible.pm/. We should use that count as min blocks 😄

yuxuanchiadm commented 5 years ago

I think counting custom blocks as just one block makes things more fun; this is essentially what Terry Tao does in his QED. The following is a proof that uses commutativity and left associativity of AND, both "custom blocks" proved before. It's just one line shorter than the naive approach. If you expand the proofs of commutativity and left associativity then of course you get much more than 7 lines.

But then min blocks is always 1 + (number of assumptions) + (number of conclusions). That's not fun either. I think instead. we should improve this by ignore "Helper block", "Assumptions", "Conclusions". Because these blocks actually does nothing. Then the block counts corresponding to actually how many axioms, deduction rules used.

nomeata commented 5 years ago

Are the numbers in this patch really from the Incredible Proof Machine (and not from pmproofs.txt)?

(I’d really hate if if turns out that there is not a direct correspondence and someone tries hard to reach the min number and they fail and in the end we have to tell them that the number was wrong.)

yuxuanchiadm commented 5 years ago

Are the numbers in this patch really from the Incredible Proof Machine

Yes. It directly from my proof.

yuxuanchiadm commented 5 years ago

Also I'll double check them later. And try do my best to minimize them. 😄

nomeata commented 5 years ago

I’ll merge it as it is, but double-checking is of course welcome!

yuxuanchiadm commented 5 years ago

Double checked. Also previously existing one "~A→A→B" from 32 to 12 by reconstructing proof.

nomeata commented 5 years ago

Bumped in 237f5ff

alreadydone commented 5 years ago

Solving (A→B)→((¬A→B)→B) all by myself takes 362 blocks ... now will be working on translating the proofs from pmproofs.txt. It's actually pretty straightforward to translate (reverse Polish notation, pre-order(NRL) depth-first traversal of proof tree), but you probably want to define custom blocks on the way.

Here is a shorter proof of "~A→A→B". image I got 22, 20, 60, 126, 362 for the remaining five problems, while pmproofs.txt says they can get 20, 18, 20, 60, 82 (possibly smaller if there are duplicates).

alreadydone commented 5 years ago

image (directly translated from pmproofs.txt)

((P -> (Q -> R)) -> (Q -> (P -> R))); ! *2.04 Comm
((P -> (Q -> R)) -> (Q -> (P -> R))); ! Result of proof
DD2D1DD22D11DD2D112; ! 19 steps

not as modular and simple as the proof I came up with (of the same size): imageimage

Custom blocks will lead to repeated subsequence, but not vice versa I think ... For example, DD2D1 corresponds to B->C, A->B |- A->C.

alreadydone commented 5 years ago

image image transcribed from

((~ P -> P) -> P); ! *2.18
((~ P -> P) -> P); ! Result of proof
DD2DD2D13D2DD2D1311; ! 19 steps

the proof is a bit hard to conceive IMO. With the custom block D2DD2D13 denoted by T, the proof is just DTT11.

I realized that the rule for spotting custom blocks from the sequence is to look for sequences starting from D, such that the running count of D's plus 1 is at least the running count of 1,2,3 combined.

alreadydone commented 5 years ago

Bottom up constructions; have verified the numbers 20, 18, 20, 60, 82 except the last one (should be easy too).

I. A→B, B→C |-  A→C
DD2D1; 5 steps

((Q -> R) -> ((P -> Q) -> (P -> R))); ! *2.05 Syll
[I=DD2D1]21; ! 7 steps

((P -> Q) -> ((Q -> R) -> (P -> R))); ! *2.06 Syll
[I=DD2D1]D2[*2.05=DD2D121]1; ! 15 steps

II. (A→((B→A)→C))→(A→C)
DD22D11; ! 7 steps

((P -> (Q -> R)) -> (Q -> (P -> R))); ! *2.04 Comm
[I=DD2D1][II=DD22D11][I=DD2D1]12; ! 19 steps

III. C->(~A->~B) |-  (C->B)->(C->A)
D2[I=DD2D1]3; ! 8 steps

((~ P -> P) -> P); ! *2.18
D[III=D2DD2D13][III=D2DD2D13]11; ! 19 steps

IV. A→(¬B→¬C) |-  A→(C→B)
DD2D13; ! 6 steps

V. (~~A->B)->(~~A->A)
D2[IV=DD2D13][IV=DD2D13]1; ! 15 steps

(~ ~ P -> P); ! *2.14
D[V=D2DD2D13DD2D131]1; ! 17 steps

(P -> ~ ~ P); ! *2.12
D3[*2.14=DD2DD2D13DD2D1311]; ! 19 steps

VI. (¬¬B→(B→C))→(¬¬B→C)
DD22[V=D2DD2D13DD2D131]; ! 19 steps
((P -> ~ Q) -> (Q -> ~ P)); ! *2.03
[I=DD2D1]3[I=DD2D1][VI=DD22D2DD2D13DD2D131]1; ! 31 steps

VII. (A→B)→(A→¬¬B)
D2D1[*2.12=D3DD2DD2D13DD2D1311]; ! 23 steps
((~ P -> Q) -> (~ Q -> P)); ! *2.15 Transp
[I=DD2D1]3[VII=D2D1D3DD2DD2D13DD2D1311]; ! 29 steps
((P -> Q) -> (~ Q -> ~ P)); ! *2.16
[I=DD2D1][*2.03=DD2D13DD2D1DD22D2DD2D13DD2D1311][VII=D2D1D3DD2DD2D13DD2D1311]; ! 59 steps

((P -> Q) -> ((~ P -> R) -> (~ R -> Q))); ! *2.37 Result of proof
[I=DD2D1]DD2[*2.05=DD2D121]D1[*2.15=DD2D13D2D1D3DD2DD2D13DD2D1311][*2.05=DD2D121]; ! 53 steps
((P -> Q) -> ((~ P -> Q) -> Q)); ! *2.61
[I=DD2D1]D2D1[*2.18=DD2DD2D13D2DD2D1311][*2.37=DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121]; ! 81 steps
Compare:
((P -> Q) -> ((~ P -> R) -> (~ Q -> R))); ! *2.38 Result of proof
[I=DD2D1][*2.06=DD2D1D2DD2D1211][*2.16=DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311]; ! 79 steps
((~ P -> Q) -> ((P -> Q) -> Q)); ! *2.6
[I=DD2D1]D2[*2.61=DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2D1311DD2D121]1; ! 89 steps
nomeata commented 5 years ago

Just to avoid mistakes on my side: Can you create a PR that updates the numbers?