<u>Axioms</u> <br />THEN-1: A → (B → A) <br />THEN-2: (A → (B → C)) → ((A → B) → (A → C)) <br />THEN-3: (A → (B → C)) → (B → (A → C)) <br />FRG-1: (A → B) → (¬B → ¬A) <br />FRG-2: ¬¬A → A <br />FRG-3: A → ¬¬A <br />
<u>Inference Rule</u> <br>MP: P, P→Q ⊢ Q <br />
Frege's propositional calculus is equivalent to any other classical propositional calculus, such as the "standard PC" with 11 axioms. Frege's PC and standard PC share two common axioms: THEN-1 and THEN-2. Notice that axioms THEN-1 through THEN-3 only make use of (and define) the implication operator, whereas axioms FRG-1 through FRG-3 define the negation operator.
The following theorems will aim to find the remaining nine axioms of standard PC within the "theorem-space" of Frege's PC, showing that the theory of standard PC is contained within... Read More