A logical calculus is a formal, axiomatic system for recursively generating well-formed formulas (wffs). Essentially, it's a definition of a vocabulary, rules for the formation of well-formed formulas (wffs), and rules of inference permitting the generation of all valid argument forms expressible in the calculus.
The propositional calculus is the foundation of symbolic logic; more complex logical calculi are usually defined by adding new operators and rules of transformation to it. It is generally defined as follows:
The vocabulary is composed of:
- The letters of the alphabet (usually capitalized).
- Symbols denoted logical operators: ¬, ∧, ∨, →, ↔
- Parenthesis for grouping a wff as a sub-wff of a compound wffs: (, )
The rules for the formation of wffs:
- Letters of the alphabet (usually capitalized) are wffs.
- If φ is a wff, then ¬ φ is a wff.
- If φ and ψ are wffs, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), and (φ ↔ ψ) are wffs.
Repeated applications of these three rules permit the generation of complex wffs. For example:
- By rule 1, A is a wff.
- By rule 2, ¬ A is a wff.
- By rule 1, B is a wff.
- By rule 3, ( ¬ A ∨ B ) is a wff.
The propositional calculus has ten inference rules. The first eight are non-hypothetical, meaning that they do not involve hypothetical reasoning: specifically, the introduction of hypothetical premises is not used; the last two rules are hypothetical. These rules are introduction and elimination rules for each logical operator, used for deriving argument forms.
- Negative Elimination
- From the wff ¬ ¬ φ, we may infer φ
- Conjunction Introduction
- From any wff φ and any wff ψ, we may infer ( φ ∧ ψ ).
- Conjunction Elimination
- From any wff ( φ ∧ ψ ), we may infer φ or ψ
- Disjunction Introduction
- From any wff φ, we may infer the disjunction of φ with any other wff.
- Disjunction Elimination
- From wffs of the form ( φ ∧ ψ ), ( φ → χ ), and ( ψ → χ ), we may infer χ.
- Biconditional Introduction
- From wffs of the form ( φ → ψ ) and ( ψ → φ ), we may infer ( φ ↔ ψ ).
- Biconditional Elimination
- From the wff ( φ ↔ ψ ), we may infer ( φ → ψ ) or ( ψ → φ ).
- Modus Ponens
- From wffs of the form φ and ( φ → ψ ), we may infer ψ.
- Conditional Proof
- If ψ can be derived from the hypothesis φ, we may infer ( φ → ψ ) and discharge the hypothesis.
- Reductio ad Absurdum
- If we can derive both ψ and ¬ ψ from the introduction of the hypothesis φ, we may infer ¬ φ and discharge the hypothesis.
Introducing an hypothesis means adding a wff to a derivation not originally present as a premise; discharging the hypothesis means eliminating the wff justifiably--any wffs correctly derived from the hypothesis justify the introduction of the hypothesis after the fact.