# Logical calculus

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:

1. The letters of the alphabet (usually capitalized).
2. Symbols denoted logical operators: ¬, , , ,
3. Parenthesis for grouping a wff as a sub-wff of a compound wffs: (, )

The rules for the formation of wffs:

1. Letters of the alphabet (usually capitalized) are wffs.
2. If φ is a wff, then ¬ φ is a wff.
3. If φ and ψ are wffs, then (φ ψ), (φ ψ), (φ ψ), and (φ ψ) are wffs.

Repeated applications of these three rules permit the generation of complex wffs. For example:

1. By rule 1, A is a wff.
2. By rule 2, ¬ A is a wff.
3. By rule 1, B is a wff.
4. 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.