search

nomeata / incredible

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

Does last tautology in "Hilbert system" provable? #100

Closed yuxuanchiadm closed 5 years ago

yuxuanchiadm commented 5 years ago

Does (A→B)→((¬A→B)→B) aka "Law of Excluded Middle" provable only using modus ponens and 3 axioms provided? And every theorem actually checked is provable before adding to tasks?

nomeata commented 5 years ago

Yes, it is provable. But it is a surprising big task to solve that one.

yuxuanchiadm commented 5 years ago

So challenge accepted! :p

yuxuanchiadm commented 5 years ago

Ok. It's provable. Takes 8 custom blocks and total exact 200 blocks (incredible coincidence!) for me to complete. Custom blocks are really important here.

michaelgwelch commented 5 years ago

Ok. It's provable. Takes 8 custom blocks and total exact 200 blocks (incredible coincidence!) for me to complete.

Well that explains why I never got even close to solving this one. My only exposure to Hilbert has been thru these 3 proofs and finding tips and tricks on the web for doing anything useful with the system seemed difficult. I just gave up.

nomeata commented 5 years ago

That is, in a way, the purpose of this section: it looks like it is a nice and simple system, but completely impractical

alreadydone commented 5 years ago

From http://us.metamath.org/mmsolitaire/pmproofs.txt from http://us.metamath.org/mmsolitaire/mms.html: ((P -> Q) -> ((~ P -> Q) -> Q)); ! *2.61 ((P -> Q) -> ((~ P -> Q) -> Q)); ! Result of proof DD2D1D2D1DD2DD2D13D2DD2D1311DD2D1DD2DD2D121D1DD2D13D2D1D3DD2DD2D13DD2 D1311DD2D121; ! 81 steps I think one step exactly corresponds to one block.