# 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^{[1]}. |

Module usage |
---|

Parameters |

none |

Imported by |

Principia Mathematica propositional logic |

Exported by |

Nicod's reduction of Principia Mathematica |

## Well-formed formulas[edit]

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)

## Logical connectives[edit]

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

Though not strictly needed for the axioms, Principia also defines conjunction (-symbol) and the biconditional (-symbol):

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.

## The axioms[edit]

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 next axiom, called *Taut* for tautology, asserts the idempotency of disjunction in one direction:

The *Add* axiom, for addition, asserts that a disjunction may be added to a wff.

The *Perm* axiom, for permutation, asserts the commutativity of disjunction.

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.

## References[edit]

- ↑ A. Whitehead, B. Russell, Principia Mathematica,
*Cambridge University Press*, 1910.

Interface module parsed successfully