Completeness Theorem Script

[Scott Fenton]

Hi all,

Some time ago, I wrote a script implementing the completeness theorem for propositional calculus in the form of a tautology prover for Metamath. I just uploaded it to Github. You can find it at https://github.com/sctfn/completeness.

To use the script to prove biid, you would call "./completeness biid '( ph <-> ph )'". This will produce an uncompressed $p statement that you can incorporate into set.mm. Furthermore, if called with the "-d" flag, the script will instead produce a D-rule proof of the theorem.

Let me know what you think!

-Scott

[David A. Wheeler]

Cool! Thanks for posting!

I suggest including in the README an example of how to invoke it (and maybe a sample response).

Here's one that worked for me:

./completeness foo '( ph <-> ph )'
foo $p |- ( ph <-> ph ) $= wph wn wph wph wb wi wph wph wb wph wn wph wph wi wph wph wi wn wi wn wi wph wn wph wph wb wi wph wn wph wph wi wn wn wi wph wn wph wph wi wph wph wi wn wi wn wi wph wn wph wph wi wi wph wn wph wph wi wn wn wi wph wph pm2.21 wph wph wi wph wph wi wn wn wi wph wn wph wph wi wi wph wn wph wph wi wn wn wi wi wph wph wi notnot wph wph wi wph wph wi wn wn wph wn imim2 ax-mp ax-mp wph wn wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wn wph wph wi wn wn wi wph wn wph wph wi wph wph wi wn wi wn wi wi wph wn wph wph wi wi wph wn wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wph pm2.21 wph wph wi wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wn wph wph wi wi wph wn wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wi wph wph wi wph wph wi wn mth8 wph wph wi wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wph wn imim2 ax-mp ax-mp wph wn wph wph wi wn wn wph wph wi wph wph wi wn wi wn ax-2 ax-mp ax-mp wph wph wi wph wph wi wn wi wn wph wph wb wi wph wn wph wph wi wph wph wi wn wi wn wi wph wn wph wph wb wi wi wph wph wb wph wph wi wph wph wi wn wi wn wb wph wph wi wph wph wi wn wi wn wph wph wb wi wph wph dfbi1 wph wph wb wph wph wi wph wph wi wn wi wn biimpr ax-mp wph wph wi wph wph wi wn wi wn wph wph wb wph wn imim2 ax-mp ax-mp wph wph wph wb wi wph wn wph wph wb wi wph wph wb wi wph wph wph wi wph wph wi wn wi wn wi wph wph wph wb wi wph wph wph wi wn wn wi wph wph wph wi wph wph wi wn wi wn wi wph wph wph wi wi wph wph wph wi wn wn wi wph wph ax-1 wph wph wi wph wph wi wn wn wi wph wph wph wi wi wph wph wph wi wn wn wi wi wph wph wi notnot wph wph wi wph wph wi wn wn wph imim2 ax-mp ax-mp wph wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wph wph wi wn wn wi wph wph wph wi wph wph wi wn wi wn wi wi wph wph wph wi wi wph wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wph ax-1 wph wph wi wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wph wph wph wi wi wph wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wi wi wph wph wi wph wph wi wn mth8 wph wph wi wph wph wi wn wn wph wph wi wph wph wi wn wi wn wi wph imim2 ax-mp ax-mp wph wph wph wi wn wn wph wph wi wph wph wi wn wi wn ax-2 ax-mp ax-mp wph wph wi wph wph wi wn wi wn wph wph wb wi wph wph wph wi wph wph wi wn wi wn wi wph wph wph wb wi wi wph wph wb wph wph wi wph wph wi wn wi wn wb wph wph wi wph wph wi wn wi wn wph wph wb wi wph wph dfbi1 wph wph wb wph wph wi wph wph wi wn wi wn biimpr ax-mp wph wph wi wph wph wi wn wi wn wph wph wb wph imim2 ax-mp ax-mp wph wph wph wb pm2.61 ax-mp ax-mp $.

I believe the minimized Metamath proof would be a lot smaller :-).

--- David A. Wheeler

> --
> 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/CACKrHR87Hjhw7Zx4cVEX8eyig3UeQ%2B9r1KSQpr0vLORUKFDUeA%40mail.gmail.com.

[Thierry Arnoux]

This looks great!

This is the kind of things Norm would have announced on the "Recent news items" section of the web pages.

_
Thierry