IV · The structural turn
Formal logic
logica formalis · ‘reasoning examined by its shape’
Inference treated as a property of structure. Strip the content of an argument and ask only what the symbols permit; the rules of inference are the licenses that survive that operation.
Orientation
What ‘formal’ means
A formal system specifies a precise vocabulary (symbols and formation rules), a notion of well-formed formula, a set of inference rules, and — separately — a semantics that says which formulas count as true under which conditions. The validity of an argument is then a property of its syntactic shape, decidable without consulting the world the symbols are meant to be about.
The aspiration is precision. Where an informal argument may hinge on contested meaning or unstated assumption, a formal proof has every premise stated and every inference licensed by an explicit rule. The cost is reach: formal systems capture only what their vocabulary can express. Each system below extends the previous one's reach by adding vocabulary.
- Syntax
- The alphabet and grammar of the language — which strings of symbols count as well-formed formulas, and which sequences of formulas count as proofs.
- Semantics
- The interpretation that assigns meaning to formulas. In propositional logic, truth-table semantics; in predicate logic, model-theoretic semantics; in modal logic, Kripke semantics over possible worlds. See truth.
- Inference rules
- Patterns that license the introduction of a formula given earlier formulas. Always belong to a specific system: the rules of propositional logic are not the rules of predicate logic, though the latter contains the former.
- Soundness · completeness
- A system is sound if every formula it proves is semantically valid, and complete if every semantically valid formula is provable. The classical systems below are both.
The systems
Four to know
The classical systems form a nested sequence: propositional sits inside predicate, which sits inside modal predicate, and so on. The non-classical survey collects systems that depart from this lineage by altering its foundational assumptions.
- I
Propositional
Atoms · ¬ ∧ ∨ → ↔
Atomic propositions combined by truth-functional connectives. The smallest formal apparatus that handles real arguments; foundation for everything that follows.
Visit - II
Predicate
Atoms · connectives · ∀ ∃
Adds predicates, terms, and quantifiers. Lets formulas talk about objects and their properties — the natural home for mathematical and ontological statements.
Visit - III
Modal
Atoms · connectives · □ ◇
Adds operators for necessity and possibility. Kripke semantics interprets them over possible worlds, with axioms (K, T, 4, 5) selecting which modal facts hold.
Visit - IV
Non-classical
Various — drops or alters classical principles
A survey of systems that depart from classical logic: intuitionistic (no excluded middle), many-valued, fuzzy, paraconsistent, relevant, linear.
Visit
Lineage
A short genealogy
Formal logic descends from two ancient roots: Aristotle's syllogistic (c. 350 BC), which was a categorical logic of terms, and Stoic propositional logic (c. 300 BC), which treated whole sentences and connectives. The Stoic line was lost in the West and rediscovered only in the twentieth century. The Aristotelian line was elaborated by Avicenna, the Latin schoolmen, and the Port-Royal logicians, but produced no major formal advance for nearly two thousand years.
The modern era begins with George Boole's The Laws of Thought(1854), which gave propositional logic its algebraic treatment. Gottlob Frege's Begriffsschrift(1879) introduced quantification and the modern predicate calculus — the most consequential single advance in the field's history. Russell and Whitehead's Principia Mathematica(1910–13) applied the apparatus to mathematics. Tarski, Gödel, and Gentzen filled in the meta-theory in the 1930s. Kripke gave modal logic its possible-worlds semantics in 1959. Subsequent work has mostly been generalisation, refinement, and the development of non-classical alternatives.