Interface:Principia Mathematica propositional logic
|Principia Mathematica Propositional Logic|
|This interface defines the "primitive ideas" (axioms) making up the propositional logic part of the Principia Mathematica.|
|Principia Mathematica propositional logic|
|Nicod's reduction of Principia Mathematica
We first introduce the kind of well-formed formulas, abbreviated as "wff". This kind subsumes the Principia Mathematica concepts of elementary and non-elementary propositions and, due to the recursive nature of JHilbert, propositional functions as well. We also introduce three variables, , as placeholders for wffs.
var (wff p q r)
Of the standard five logical connectives of classical propositional logic, Principia requires only disjunction ( -symbol) and implication ( -symbol) for its axioms. However, disjunction and negation ( -symbol) are actually used as primitive logical connective. Implication is defined from them:
term (wff (∨ wff wff)) # Disjunction
def ((↔ p q) ((p → q) ∧ (q → p))) # Biconditional, *4.01
Note that Principia actually uses different symbols for negation, implication, conjunction and the biconditional. However, the present symbols reflect current usage.
We are now in the position to state the six axioms for propositional logic of Principia (five, if you don't count the rule of detachment). The sole rule of detachment in Principia works like this:
- If one may assert , and also that implies (i.e., ), then one may infer .
This rule has become known as modus ponens. Since the corresponding JHilbert statement requires hypotheses, we fomulate it in imperative form:
The Add axiom, for addition, asserts that a disjunction may be added to a wff.
The next axiom, Assoc for associativity, asserts the associative law for disjunction. However, there is a twist. A commutation is built in the axiom as well. Thus, the axiom obtains more deductive power than plain associativity alone.
The final axiom, Sum for summation, provides the basic building block for assembling complex formulas. It states that , meaning that an arbitrary formula may be added to both antecedent and consequent of an implication.
From these axioms, all true statements of propositional logic can be derived.
- A. Whitehead, B. Russell, Principia Mathematica, Cambridge University Press, 1910.
Interface module parsed successfully