> I managed to prove ax3 from w2 manually!
Indeed, nice.
Compactly written, that is
CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CCNppp =
DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
[6] CpCCNqqq = D[3][5]
[7] CCNpNqCqp = DDD1[6]DDD1DDD1DDD1[6]DDD1[5]1[6][6][1]11[6][6]
and
./pmGenerator --transform data/w2.txt -f -n -t
CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -p -2 -d
now prints
There are 35 steps towards Cpp / C0.0 (index 8).
There are 53 steps towards CpCqp / C0C1.0 (index 11).
There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
There are 417 steps towards CCNppp / CCN0.0.0 (index 14).
There are 3301 steps towards CCNpNqCqp / CCN0N1C1.0 (index 16).
i.e. this is a "w2: A3: ω↦3301" improvement, the biggest so far 😃.
Congratulations!
Could you also post your solution and procedure/details at
https://github.com/xamidi/pmGenerator/discussions/2?
________________________________
Von: [email protected] <[email protected]> im Auftrag von
Steven Nguyen <[email protected]>
Gesendet: Mittwoch, 10. Juli 2024 18:24:46
An: [email protected]
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus
I managed to prove ax3 from w2 manually!
(append this to ./data/w2.txt to verify)
[15] CpCCNqqq = D[11][14]
% Axiom 3
[16] CCNpNqCqp = DDD1[15]DDD1DDD1DDD1[15]DDD1[14]1[15][15][8]11[15][15]
Based on how procedural/repetitive this manual proof looks compared to the more
brute force proofs, there’s probably a shorter proof of this.
I found this manually-ish by looking at random pmGenerator proofs and only
filling in steps that require lots of syntax to match. Doing this generalizes a
pmGenerator proof to an inference proof. Unfortunately due to inane reasons my
desktop computer doesn't have internet but I took relevant photos
Details:
Letting w2 be 1, a1dt (frege24) be 2, luk2 be 3, partially proving
DDD1DD2DD1D233321 in metamath.exe resulted in w2-q, which I then repurposed for
ax3
I think proofs with hypotheses are more intuitive for humans, but I’m not sure
how much this can help computers.
I tried to send photos of my metamath proofs but for some reason each photo is
like 8 mb and gmail refuses to send that long of an email. I posted them to
https://github.com/icecream17/Stuff/blob/main/math/<https://github.com/icecream17/Stuff/blob/main/math/IMG_0057.jpeg>
and the files are in the format “IMG_00xx.JPEG”
--
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]<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com<https://groups.google.com/d/msgid/metamath/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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/a8843977b98b4eea83543ca6156a94e9%40rwth-aachen.de.
