Formal Logic
Formal logic is the study of reasoning as a matter of form: a symbolic system with a precisely specified language and explicit rules of inference, so that whether a conclusion follows from premises can be checked by looking at the shapes of the statements, without appeal to their meaning. For artificial intelligence it supplied the first and most influential picture of what a reasoning machine might be, and a vocabulary of soundness, completeness, and decidability that still frames the limits of automated deduction.
The oldest strand is Aristotle's syllogism, from the Prior Analytics of the fourth century BC, which showed that some arguments are valid by virtue of their pattern alone. All men are mortal, Socrates is a man, therefore Socrates is mortal: the validity belongs to the structure, all A are B and C is an A so C is a B, and any content could be substituted. For more than two thousand years this stood as the core of logic in the West. Its limits were real, though, since the syllogism handles statements about whole classes and cannot express relations such as being greater than, or statements with several nested quantifiers, which mathematics requires constantly.
The nineteenth century turned logic into algebra and then into a full formal language. George Boole's 1854 book An Investigation of the Laws of Thought treated propositions as symbols obeying algebraic laws, laying groundwork for Boolean algebra and later digital circuits. Gottlob Frege's 1879 Begriffsschrift went further, introducing quantifiers and a precise notation in which proofs became sequences of rule applications, which is the first modern predicate logic. Alfred North Whitehead and Bertrand Russell's three-volume Principia Mathematica, published from 1910 to 1913, then carried out a long derivation of arithmetic from logical axioms, demonstrating that large areas of mathematics could be expressed in a single formal system with explicit steps.
David Hilbert's program in the 1920s asked whether mathematics could be placed on a secure footing by formalizing it and proving the formal system consistent and complete by finite methods, and the answers shaped both logic and computing. Gödel proved in 1929 that first-order logic is complete, so every valid statement has a proof, then showed in 1931 that any consistent formal system strong enough for arithmetic contains true statements it cannot prove, and cannot prove its own consistency. In 1936, Alonzo Church and Alan Turing independently showed there is no general procedure that decides whether a first-order statement is provable. Turing's machines, devised to settle the question, became the theoretical model of computers, so that the limit results of formal logic gave birth to the notion of computation itself.
Logic gave early AI both a method and an ambition. Newell, Shaw, and Simon's Logic Theorist of 1956 proved 38 of the first 52 theorems in Chapter 2 of Principia, using heuristic search over proofs rather than exhaustive derivation, which showed that mechanical deduction could be made practical and also that the search strategy mattered more than the rules. John McCarthy's 1959 Advice Taker proposal envisaged a system that would reason about the world by deduction from sentences, and J. A. Robinson's 1965 resolution principle supplied a single rule suited to computers. Logic programming, with Prolog developed in the early 1970s by Alain Colmerauer and Robert Kowalski and their colleagues, ran programs as logical statements, and knowledge-based systems of the 1970s and 1980s relied on explicit rules.
The weaknesses that emerged are as instructive as the successes. Logical systems are brittle when knowledge is incomplete or exceptions abound, since classical deduction is monotonic and more premises never retract a conclusion, whereas everyday reasoning often revises its beliefs. Describing what stays unchanged when something happens, known as the frame problem, proved hard in a purely logical setting, and encoding enough common knowledge by hand turned out to be enormously laborious. These difficulties, together with the rise of statistical learning, shifted attention away from pure logic, though the failure was one of scope rather than of validity.
Misconceptions are common in both directions. Boole's title notwithstanding, formal logic is not a theory of how people actually think, and psychological studies show that human reasoning departs from classical rules in systematic ways. Equally, Gödel's theorems do not prove that machines cannot be intelligent; they limit what any single consistent formal system can prove about itself, a point sometimes stretched in arguments about minds. Meanwhile logic is quietly everywhere: SAT and SMT solvers verify chips and software, proof assistants such as Coq and Lean check mathematics, databases are built on relational logic, and neuro-symbolic research tries to combine learned pattern recognition with explicit reasoning.
Read formal logic as the project of making inference a mechanical operation on symbols: from Aristotle's patterns to Frege's notation and Gödel's limits, it handed AI its first model of a reasoning machine and its sharpest account of what such a machine can and cannot prove.