Predicate Logic
Predicate logic, in its standard form called first-order logic, extends propositional logic with variables ranging over objects, predicates that state properties of and relations between those objects, and the quantifiers "for all" and "there exists." Where propositional logic must treat "Socrates is mortal" as an opaque atom, predicate logic writes Mortal(socrates) and can therefore say that Man(x) → Mortal(x) holds for every x, then draw the conclusion about Socrates by instantiation. It is the language in which most of mathematics, database theory and classical AI knowledge representation is formalized.
Gottlob Frege created the first full system of quantificational logic in his 1879 Begriffsschrift, replacing the subject-predicate grammar inherited from Aristotle with function-and-argument analysis. Treating "loves" as a two-place predicate allowed him to express nested quantifier patterns that had defeated traditional logic, such as the difference between "everyone loves someone" and "someone is loved by everyone." Frege's notation was two-dimensional and unwieldy, and the modern symbols descend from Peano, Russell and Hilbert's school, but the core idea is his. Charles Sanders Peirce and Oscar Howard Mitchell arrived at quantifiers independently in the 1880s. The restriction to first-order means that quantifiers range over individuals only, never over predicates or sets of individuals, which is what keeps the logic's good metatheory intact.
Kurt Gödel proved in his 1929 doctoral dissertation, published in 1930, that first-order logic is complete: every formula true in all models has a formal proof. This completeness theorem ties semantics (truth in all interpretations) to syntax (derivability), so that a finite, mechanical proof system captures the whole of logical consequence for the first-order language. It is easily confused with his incompleteness theorems of 1931, which say something different: any consistent, effectively axiomatized theory strong enough to express arithmetic contains true statements it cannot prove. Completeness is about pure logic, incompleteness about particular mathematical theories. A related consequence, compactness, says that if every finite subset of a set of sentences has a model then so does the whole set.
Completeness does not make the logic decidable, and the contrast with propositional logic is the central fact about it. The Entscheidungsproblem, posed by Hilbert and Ackermann in 1928, asked for an algorithm to decide whether a first-order sentence is valid. Alonzo Church in 1936 and Alan Turing in 1936-37 independently showed that none exists. What does exist is a procedure that, given a valid sentence, eventually finds its proof: validity is semi-decidable. If the sentence is not valid, the search may run forever, with no way to know that no proof is coming. Propositional validity, by contrast, can always be settled by a truth table in finite time. Certain fragments of first-order logic, such as the monadic fragment, are decidable, and much of automated reasoning consists of finding useful fragments that stay on the decidable side.
The most influential mechanization of predicate logic was J. A. Robinson's resolution principle, published in 1965 in the Journal of the ACM as "A Machine-Oriented Logic Based on the Resolution Principle." Earlier machine provers, built on the work of Herbrand and Skolem, had generated enormous numbers of ground instances; Robinson's contribution was unification, an algorithm that finds the most general substitution making two literals match, so that a single inference step covers infinitely many instances. To prove a goal, the formula is negated, converted to clauses with Skolem functions replacing existential quantifiers, and resolved until the empty clause appears. This refutation method underlies theorem provers, and its restricted form, SLD resolution, became the execution model of Prolog in the early 1970s through the work of Colmerauer, Kowalski and their colleagues.
Modern descendants of predicate logic are everywhere, often hidden beneath other names. Relational databases rest on first-order queries, SQL being close to relational calculus; description logics, a decidable family of first-order fragments, underlie the OWL ontologies used in knowledge graphs; SMT solvers combine propositional search with theories and discharge first-order verification conditions; and proof assistants add higher-order features on top. A common misconception is that "first-order" means a logic with a single quantifier or a weak one: it means quantification over individuals only, and the expressive loss is real, since second-order logic can pin down the natural numbers but loses completeness. Another pitfall is believing undecidability means a prover can never succeed; it means no prover can succeed on every input, and in practice powerful provers settle many hard problems.
Read predicate logic as propositional logic given objects and the words every and some: expressive enough to hold nearly all of formal mathematics, complete enough that valid reasoning can be found by machine, and undecidable enough that no program can promise to answer every question put to it.