With a few more manually proved short statements ( https://github.com/icecream17/Stuff/blob/main/~w2.mm) I think that a new search with id, ax1, luk2, luk3 as base axioms as well as w2 has high potential to find new proofs for the missing theorems ax2 ax3 luk1. I tried to do this but it's hard as ever to get c++ code to compile On Saturday, July 6, 2024 at 2:51:56 AM UTC-5 Jeff Hoffman wrote:
> Concerning Sheffer stroke equational proofs, it's worth noting that > there's a duality at play. Wolfram's axiom holds even if the stroke is > interpreted as NOR instead of NAND. |- (p(pp)) <-> (q(qq)) with either > interpretation, so the truth-value of (p(pp)) is constant, independent of > the value of p. However, it takes an axiom like |- (p(pp)) to nail down > that constant as TRUE and the interpretation as NAND. > > "this interpretation his system would be composed of two rules of > inferences and no axioms" > I played with this approach using a 2basis ( > https://www.cs.unm.edu/~veroff/DOCS/2basis.pdf) which is a precursor to > Wolfram's axiom. However, I added the axiom |-(p(pp)) so that tautologies > without biconditionals could be expressed. The plus is that makes mappings > to set.mm seem a bit more tractable. The minus is that it takes gobs to > get to something like https://us.metamath.org/mpegif/dfbi1ALT.html or > https://us.metamath.org/mpegif/nic-bi1.html that express equality in this > system. It got way messy, so I bailed on the idea. > > And yeah, it's very weird. Because the inference rules are mirrors of > each other, all proofs are reversable. Because the inference rules don't > have & (like modus ponens), proofs don't have a tree-like structure. It's > more like a linear sequence. If you have a proof of |-a, you can make an > interface T=>a and a=>T. By "* instantiation" you also have a(bb) > =>T(bb). Because T can be written with any variable, the lemma (b(bb))(bb) > => b can be tacked on. So in the end, given |-a, a(bb)=>b Very messy for > one application of modus ponens. > > > On Friday, June 14, 2024 at 9:41:43 PM UTC-5 [email protected] wrote: > >> I don't know if this will help, but I found proofs of mpi and a1d from >> welsh's second axiom: >> MM> show proof w2mpi >> 16 min=w2luk2 $p |- ( ( -. ps -> ps ) -> ps ) >> 19 maj=w2ax1 $p |- ( ( ( -. ps -> ps ) -> ps ) -> ( -. ch -> ( ( -. >> ps -> >> ps ) -> ps >> ) ) ) >> 20 min=ax-mp $a |- ( -. ch -> ( ( -. ps -> ps ) -> ps ) ) >> 29 min=w2mpi.2 $e |- ( ps -> ( ph -> ch ) ) >> 34 min=w2mpi.1 $e |- ph >> 40 maj=ax-w2 $a |- ( ph -> ( ( ps -> ( ph -> ch ) ) -> ( ( -. ch >> -> ( ( >> -. ps -> ps ) -> ps ) ) -> ( ps -> ch ) >> ) ) ) >> 41 maj=ax-mp $a |- ( ( ps -> ( ph -> ch ) ) -> ( ( -. ch -> ( ( -. >> ps -> >> ps ) -> ps ) ) -> ( ps -> ch >> ) ) ) >> 42 maj=ax-mp $a |- ( ( -. ch -> ( ( -. ps -> ps ) -> ps ) ) -> ( ps >> -> ch ) >> >> ) >> 43 w2mpi=ax-mp $a |- ( ps -> ch ) >> >> MM> show proof w2a1d >> 17 min=w2luk2 $p |- ( ( -. ch -> ch ) -> ch ) >> 20 maj=w2ax1 $p |- ( ( ( -. ch -> ch ) -> ch ) -> ( -. ps -> ( ( >> -. ch >> -> ch ) -> ch >> ) ) ) >> 21 w2mpi.1=ax-mp $a |- ( -. ps -> ( ( -. ch -> ch ) -> ch ) ) >> 33 min=w2a1d.1 $e |- ( ph -> ps ) >> 36 maj=w2ax1 $p |- ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) ) >> 37 w2mpi.1=ax-mp $a |- ( ch -> ( ph -> ps ) ) >> 43 w2mpi.2=ax-w2 $a |- ( ph -> ( ( ch -> ( ph -> ps ) ) -> ( ( -. ps >> -> ( ( >> -. ch -> ch ) -> ch ) ) -> ( ch -> ps ) >> ) ) ) >> 44 w2mpi.2=w2mpi $p |- ( ph -> ( ( -. ps -> ( ( -. ch -> ch ) -> ch ) ) >> -> ( >> ch -> ps >> ) ) ) >> 45 w2a1d=w2mpi $p |- ( ph -> ( ch -> ps ) ) >> > -- 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/1bb96ad7-e17d-4cf2-8c30-7eae073a3692n%40googlegroups.com.
