Frege's propositional calculus

Frege's propositional calculus

In mathematical logic Frege's propositional calculus was the first axiomatization of propositional calculus. It was invented by Gottlob Frege, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus (although Charles Peirce was the first to use the term "second-order" and developed his own version of the predicate calculus independently of Frege).

It makes use of just two logical operators: implication and negation, and it is constituted by six axioms and one inference rule: modus ponens.

"THEN-1:" A → (B → A)
"THEN-2:" (A → (B → C)) → ((A → B) → (A → C))
"THEN-3:" (A → (B → C)) → (B → (A → C))
"FRG-1:" (A → B) → (¬B → ¬A)
"FRG-2:" ¬¬A → A
"FRG-3:" A → ¬¬A

Inference Rule
"MP:" P, P→Q ⊢ Q

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 the theory of Frege's PC.

(A theory, also called here, for figurative purposes, a "theorem-space", is a set of theorems which are a subset of a universal set of well-formed formulas. The theorems are linked to each other in a directed manner by inference rules, forming a sort of dendritic network. At the roots of the theorem-space are found the axioms, which "generate" the theorem-space much like a generating set generates a group.)

Rule THEN-1*: A ⊢ B→A

Rule FRG-1*: A→B ⊢ ¬B→¬A

Theorem TH2: A→(¬A→¬B)

Theorem TH5: (A→¬B)→(B→¬A)

Theorem TH8: A→((A→B)→B)

Note: ¬(A→¬B)→A (TH4), ¬(A→¬B)→B (TH6), and A→(B→¬(A→¬B)) (TH10), so ¬(A→¬B) behaves just like A∧B (compare with axioms AND-1, AND-2, and AND-3).

Theorem TH11: (A→B)→((A→¬B)→¬A)

Rule TH14*: A→(B→P), P→Q ⊢ A→(B→Q)

Theorem TH17: (¬A→B)→(¬B→A)

Note: A→((A→B)→B) (TH8), B→((A→B)→B) (TH9), and(A→C)→((B→C)→(((A→B)→B)→C)) (TH19), so ((A→B)→B) behaves just like A∨B. (Compare with axioms OR-1, OR-2, and OR-3.)

Theorem TH20: (A→¬A)→¬A

Theorem ST2: A→¬¬A

ST4 is axiom FRG-2 of Frege's PC.

Prove ST5: (A→(B→C))→(B→(A→C))

ST5 is axiom THEN-3 of Frege's PC.

Theorem ST6: (A→B)→(¬B→¬A)

ST6 is axiom FRG-1 of Frege's PC.

Each of Frege's axioms can be derived from the standard axioms, and each of the standard axioms can be derived from Frege's axioms. This means that the two sets of axioms are interdependent and there is no axiom in one set which is independent from the other set. Therefore the two sets of axioms generate the same theory: Frege's PC is equivalent to standard PC.

(For if the theories should be different, then one of them should contain theorems not contained by the other theory. These theorems can be derived from their own theory's axiom set: but as has been shown this entire axiom set can be derived from the other theory's axiom set, which means that the given theorems can actually be derived solely from the other theory's axiom set, so that the given theorems also belong to the other theory. Contradiction: thus the two axiom sets span the same theorem-space. By construction: Any theorem derived from the standard axioms can be derived from Frege's axioms, and vice versa, by first proving as theorems the axioms of the other theory as shown above and then using those theorems as lemmas to derive the desired theorem.)

ee also



*cite conference | first = Samuel | last = Buss | title = An introduction to proof theory | booktitle = Handbook of proof theory | pages = 1–78 | publisher = Elsevier | date = 1998 | id = ISBN 0-444-89840-9

Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Propositional calculus — In mathematical logic, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules… …   Wikipedia

  • propositional calculus — The logical calculus whose expressions are letters representing sentences or propositions, and constants representing operations on those propositions, to produce others of higher complexity. The operations include conjunction, disjunction,… …   Philosophy dictionary

  • Propositional formula — In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional… …   Wikipedia

  • Frege, Gottlob — (1848–1925) German mathematician and philosopher of mathematics. Frege was born in the small town of Wismar in Pomerania, and was sent to the university of Jena when he was twenty one. He obtained his doctorate at Göttingen, and worked almost the …   Philosophy dictionary

  • Monadic predicate calculus — In logic, the monadic predicate calculus is the fragment of predicate calculus in which all predicate letters are monadic (that is, they take only one argument), and there are no function letters. All atomic formulae have the form P(x), where P… …   Wikipedia

  • Begriffsschrift — is the title of a short book on logic by Gottlob Frege, published in 1879, and is also the name of the formal system set out in that book. Begriffsschrift is usually translated as concept writing or concept notation ; the full title of the book… …   Wikipedia

  • List of mathematics articles (F) — NOTOC F F₄ F algebra F coalgebra F distribution F divergence Fσ set F space F test F theory F. and M. Riesz theorem F1 Score Faà di Bruno s formula Face (geometry) Face configuration Face diagonal Facet (mathematics) Facetting… …   Wikipedia

  • Function (mathematics) — f(x) redirects here. For the band, see f(x) (band). Graph of example function, In mathematics, a function associates one quantity, the a …   Wikipedia

  • logic, history of — Introduction       the history of the discipline from its origins among the ancient Greeks to the present time. Origins of logic in the West Precursors of ancient logic       There was a medieval tradition according to which the Greek philosopher …   Universalium

  • History of logic — Philosophy ( …   Wikipedia