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/50647516-8a36-4b5b-9583-cdfe65ba566en%40googlegroups.com.
