Interface:Principia Mathematica propositional logic
From Wikiproofs
| 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 |
Contents |
[edit] Well-formed formulas
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, p,q,r, as placeholders for wffs.
var (wff p q r)
[edit] Logical connectives
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.
[edit] The axioms
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 p, and also that p implies q (i.e.,
), then one may infer q.
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.
[edit] References
- ↑ A. Whitehead, B. Russell, Principia Mathematica, Cambridge University Press, 1910.
Interface module parsed successfully
