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 -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACKrHR87Hjhw7Zx4cVEX8eyig3UeQ%2B9r1KSQpr0vLORUKFDUeA%40mail.gmail.com.
