% Meredith's Axiom (CCCCCpqCNrNsrtCCtpCsp), i.e. ((((0→1)→(¬2→¬3))→2)→4)→((4→0)→(3→0)) % Fitch-style natural deduction proof constructor: https://mrieppel.github.io/FitchFX/ % % Related Hilbert system: https://xamidi.github.io/pmGenerator/data/m.txt % Conversion to Hilbert-style condensed detachment proof summary: % - [base:CpCqp,CCpCqrCCpqCpr,CCNpNqCqp]: pmGenerator --ndconvert data/m_ffx.txt -n % - [.txt]: pmGenerator --ndconvert data/m_ffx.txt -n -b .txt Problem: |- (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A))) 1 | |_ ((((A > B) > (~C > ~D)) > C) > E) Assumption 2 | | |_ (E > A) Assumption 3 | | | |_ D Assumption 4 | | | | |_ ~A Assumption 5 | | | | | |_ ((A > B) > (~C > ~D)) Assumption 6 | | | | | | |_ ~C Assumption 7 | | | | | | | |_ A Assumption 8 | | | | | | | | |_ ~B Assumption 9 | | | | | | | | | # ~E 4,7 10 | | | | | | | | B IP 8-9 11 | | | | | | | (A > B) >I 7-10 12 | | | | | | | (~C > ~D) >E 5,11 13 | | | | | | | ~D >E 6,12 14 | | | | | | | # ~E 3,13 15 | | | | | | C IP 6-14 16 | | | | | (((A > B) > (~C > ~D)) > C) >I 5-15 17 | | | | | E >E 1,16 18 | | | | | A >E 2,17 19 | | | | | # ~E 4,18 20 | | | | A IP 4-19 21 | | | (D > A) >I 3-20 22 | | ((E > A) > (D > A)) >I 2-21 23 | (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A))) >I 1-22