Interface:Principia Mathematica propositional logic

From Wikiproofs
Jump to: navigation, search
Principia Mathematica Propositional Logic
This interface defines the "primitive ideas" (axioms) making up the propositional logic part of the Principia Mathematica[1].
Module usage
Imported by
Principia Mathematica propositional logic
Exported by
Nicod's reduction of Principia Mathematica

Standard axioms imply Principia Mathematica axioms

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.

kind (wff)
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)) # Negation

term (wff ( wff wff)) # Disjunction

def (( p q) ((¬ p)  q)) # Implication, *1.01

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

def (( p q) (¬ ((¬ p)  (¬ q)))) # Conjunction, *3.01
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:

stmt (applyModusPonens () (p (p  q)) q) # *1.1

The next axiom, called Taut for tautology, asserts the idempotency of disjunction in one direction:

stmt (Taut () () ((p  p)  p)) # *1.2

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

stmt (Add () () (q  (p  q))) # *1.3

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

stmt (Perm () () ((p  q)  (q  p))) # *1.4

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.

stmt (Assoc () () ((p  (q  r))  (q  (p  r)))) # *1.5

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.

stmt (Sum () () ((q  r)  ((p  q)  (p  r)))) # *1.6

From these axioms, all true statements of propositional logic can be derived.


  1. A. Whitehead, B. Russell, Principia Mathematica, Cambridge University Press, 1910.

Interface module parsed successfully