> [...] 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
Nice to read from more people attempting this. :-) Do you have issues building pmGenerator? In that case, the shell build script cited at https://github.com/xamidi/pmGenerator/releases/tag/1.2.0 should still work for the most recent commit (and probably won't change for the next release). You can replace mpicxx with g++ or clang++, but the resulting binaries may not support MPI via any mpiexec depending on your compiler installation. My issues were building the dependencies (oneTBB on Linux via their build instructions <https://github.com/oneapi-src/oneTBB/blob/master/INSTALL.md>), and finding suitable binaries on Windows (GCC-variants are linked in the release notes, these have to be additionally included via -I -L and -l flags in the build script). However, I usually don't use build scripts but the automated build system provided by Eclipse CDT (works great on both platforms; I'm using 2022-06, due to some issues I had with more recent versions). PS: Thanks Jeff for taking on that headache so we don't have to :○) [email protected] schrieb am Samstag, 6. Juli 2024 um 16:48:04 UTC+2: > 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/eacd7fa9-c058-4579-9aec-50c15edf2dbdn%40googlegroups.com.
