Logic

Logic studies formal languages, proof, models, semantics, consistency, and the foundations of mathematical reasoning.

Modal logic is the largest field, with more than a third of the subject's articles. The systems K, T, S4 and S5 are sound and strongly complete for Kripke models whose accessibility relation is arbitrary, reflexive, reflexive and transitive, or an equivalence relation, and filtration gives each of them the finite model property. The field also has the modal μ-calculus, with least and greatest fixed points, and its model-checking game, a parity game between Verifier and Refuter.

Propositional logic covers natural deduction and its completeness, Craig interpolation and satisfiability, from the Tseitin transformation and resolution to the DPLL procedure and binary decision diagrams. First-order logic centers on Gödel's completeness theorem in its strong form, built from Henkin witnesses, and in temporal logic every formula of linear temporal logic has a Büchi automaton accepting exactly the words that satisfy it, the basis of LTL model checking.

Proof theory has cut elimination for classical linear logic and abstract forms of Gödel's incompleteness theorems, and model theory has Tarski's quantifier elimination for the real field, Morley's categoricity theorem and Wilkie's conjecture for \(\mathbb{R}_{\exp}\), which bounds the number of algebraic points of degree at most \(g\) and height at most \(H\) on the transcendental part of a definable set by a polynomial in \(g\) and \(\log H\).

• Propositional logic and satisfiability
• First-order logic
• Proof theory
• Modal logic
• Temporal logic and model checking
• Model theory

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.