Formal Logic

Overview

Formal logic is the branch of logic that studies the forms of valid inference by constructing artificial languages. Instead of analyzing natural-language sentences, formal logic translates argument patterns into symbols — variables, connectives, quantifiers, and predicates — so that the structure of reasoning can be examined with mathematical precision. Its great discovery is that validity is a matter of form: arguments are valid not because of their content but because of their shape. "If it rains, the ground is wet; it rains; therefore the ground is wet" and "If it is a bird, it has wings; it is a bird; therefore it has wings" share the form "If p, then q; p; therefore q" — and it is the form, not the content, that makes both valid.

Formal logic is standardly divided into two layers. Propositional logic (or sentential logic) studies the truth-functional connectives — "not," "and," "or," "if...then" — and the arguments built from simple propositions. Predicate logic (or first-order logic) adds names, predicates, and quantifiers — "all," "some" — capturing the internal structure of propositions that propositional logic must treat as indivisible atoms. It was predicate logic that revealed the full power of formalization, and it remains the default logic of mathematics, computer science, and the formal study of natural language.

Historical Development

Formal logic begins with Aristotle, whose syllogistic was the first genuine formal system: it classified argument patterns by their "figures and moods" and proved which are valid. The Stoics added the logic of propositions, analyzing conditionals and the rules of modus ponens and modus tollens. Medieval logicians, including William of Ockham, refined the theory of supposition and consequence. Yet for two millennia, logic remained essentially syllogistic, and it proved unable to represent the full range of mathematical reasoning — including relational arguments such as "All A's are related to some B; all B's are related to some C; therefore..." that resisted syllogistic analysis.

The revolution came in 1879, when Gottlob Frege published the Begriffsschrift. Frege introduced the quantifier — the formal device for expressing "all" and "some" — and with it the modern predicate calculus, showing how to represent relational arguments, multiple generality, and the logic of mathematics. Bertrand Russell and Alfred North Whitehead built on this foundation in Principia Mathematica, attempting to derive all of mathematics from logical axioms, while simultaneously discovering the set-theoretic paradoxes that forced the development of type theory. [David Hilbert] and his school then established proof theory and metamathematics: the study of formal systems as mathematical objects. In the 1930s, [Alfred Tarski] defined the model-theoretic notion of truth and logical consequence, and Kurt Gödel proved the completeness of first-order logic — and, more dramatically, the incompleteness of arithmetic.

Core Ideas

Syntax and Semantics

A formal language has a syntax — the rules for constructing well-formed formulas — and a semantics — the rules for interpreting them. In propositional logic, atomic sentences are assigned truth values and connectives are defined by truth tables. In predicate logic, formulas are interpreted in models: domains of objects with relations and functions assigned to the predicates and names. A formula is valid (a logical truth) if it is true in every model; an argument is valid if its conclusion is true in every model in which its premises are true. This semantic conception of consequence, due to Tarski, is the modern successor to the intuitive notion of "impossible for premises to be true and conclusion false."

Proof Systems

Complementing semantics is proof theory: the rules of inference by which conclusions are derived from premises in a formal system. A natural deduction system mirrors human reasoning with introduction and elimination rules for each connective; a Hilbert-style axiom system uses axioms and a single rule (modus ponens); a sequent calculus makes all structural rules explicit. The central metatheorems connect the two perspectives: first-order logic is sound (everything provable is valid) and complete (everything valid is provable) — results proved by Gödel in 1930 that vindicate the formalist program for logic itself.

The Expressive Power and Limits of Formal Systems

The incompleteness theorems of 1931 marked the boundary of formalization: any consistent formal system strong enough to encode arithmetic contains truths it cannot prove. This result, shocking at the time, established permanent limits to the logicist program of Frege and Russell and transformed the philosophy of mathematics. It also illuminates the difference between truth and provability — between the semantic and syntactic faces of logic. Later developments extended formal logic in new directions: modal logic, given its Kripke semantics by Saul Kripke; intuitionistic logic; many-valued and fuzzy logics; and second-order and higher-order systems.

Key Thinkers

Aristotle (384–322 BCE) founded formal logic with the syllogism. William of Ockham (c. 1287–1347) advanced medieval logic of terms and consequences. Gottlob Frege (1848–1925) created the predicate calculus and initiated logicism. Bertrand Russell (1872–1970) developed the theory of types and the logicist program in Principia Mathematica. [David Hilbert] (1862–1943) established proof theory and metamathematics. [Alfred Tarski] (1901–1983) gave the semantic definition of truth and logical consequence. Willard Van Orman Quine (1908–2000) wrote the standard textbook of modern logic. Saul Kripke (1940–2022) provided the semantics of modal logic.

Influence

Formal logic is the working language of the exact sciences of reasoning. It underlies mathematics, whose proofs are formalizable in principle; computer science, where hardware implements Boolean algebra and programs are evaluated as formal systems; linguistics, where logical form is a level of syntactic and semantic analysis; and philosophy, where the tools of formalization illuminate everything from the philosophy of language to epistemology. For the student of critical thinking, formal logic supplies the sharpest instruments of argument evaluation; for the student of informal logic, it provides the idealized standard from which everyday reasoning departs. The rigor it teaches — precision, explicitness, and respect for the rules of inference — is the intellectual discipline at the heart of the scientific attitude.

Sources

1. Stanford Encyclopedia of Philosophy, "Classical Logic." A comprehensive technical and philosophical introduction to first-order logic.
2. Stanford Encyclopedia of Philosophy, "Logical Consequence." The authoritative account of the semantic and syntactic conceptions of consequence.
3. Internet Encyclopedia of Philosophy, "Logic." An accessible introduction to formal systems and their interpretation.