Description: Derivation of ax-2 from the Tarski-Bernays axiom set { ax-1 , imim1 , peirce }. Note that no inference rule other than ax-mp is used in this proof. This proof establishes a circle of equivalence: From { impsingle }, { ax-1 , imim1 , peirce } was proved. From { ax-1 , imim1 , peirce }, { ax-1 , ax-2 and peirce } was proved. From { ax-1 , ax-2 and peirce }, { impsingle } was proved. Therefore, the theorems that can be proved by selecting any one of these three distinct axiom sets must be equivalent. Prover9 and mmj2 were used to help constuct this proof. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | tarski-bernays-ax2 | |