  Encyclopedia > Logical calculus

Article Content

Propositional calculus

Redirected from 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.

Double 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.

If we can derive both ψ and ¬ ψ from the introduction of the hypothesis φ, we may infer ¬ φ and discharge the hypothesis.

Introducing a 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.

With wffs and rules of inference, it's possible to derive wffs; the derivation[?] is a valid argument form[?], while the derived wff is known as a lemma.

All Wikipedia text is available under the terms of the GNU Free Documentation License

Search Encyclopedia
 Search over one million articles, find something about almost anything!

Featured Article
 Ludvika ... Falun  |  Gagnef  |  Hedemora  |  Leksand  |  LudvikaMalung  |  Mora  |  Orsa  |  Rättvik ...  