Logic and Formal Systems

Logic is the study of valid inference. A formal system specifies a precise language, a set of axioms and a set of inference rules from which theorems can be derived by purely syntactic steps, so that correctness of a derivation can be checked mechanically. In AI, logic provides representation languages for knowledge, algorithms for deriving consequences, and limits on what any such algorithm can accomplish.

Logic was the first major formalism for AI. The early programs of the 1950s and 1960s (see HIST-003 Symbolic AI and the Perceptron) treated intelligence as symbol manipulation, with logical deduction as a model of reasoning. McCarthy's research program proposed representing common-sense knowledge in logical form, and logic-based representation remains the core of knowledge representation languages, databases, program verification and formal mathematics (FOUND-003 Knowledge Representation).

Logic also delimits what is possible. Results of Gödel, Church and Turing show that sufficiently expressive formal systems cannot be both complete and decidable, and complexity theory (Cook, 1971; see FOUND-004 Computational Complexity in AI) shows that even propositional satisfiability is believed to be intractable in the worst case. These limits explain both the successes (exact, verifiable reasoning in restricted domains) and the difficulties (brittleness, combinatorial explosion) of logic-based AI.

Current interest in logic comes from two directions: the use of proof assistants and automated provers for verified mathematics and software, and attempts to combine neural networks, which learn flexibly but give no guarantees, with symbolic reasoning, which gives guarantees but requires formalization (Garcez & Lamb, 2023).

Modern formal logic dates from the late nineteenth century and the construction of quantificational logic as a formal language (Frege's Begriffsschrift, 1879; Frege, 1879). In 1930 Gödel proved the completeness of first-order logic (Gödel, 1930). In 1931 he proved that any effectively axiomatized formal system capable of expressing elementary arithmetic is incomplete if it is suitably consistent: there are true statements it cannot prove (Gödel, 1931). Gödel's original argument assumed the stronger condition of $\omega$-consistency, and Rosser (1936) extended the result to plain consistency. In 1936 Church and Turing independently showed that the Entscheidungsproblem, the problem of deciding validity of first-order formulas, has no algorithmic solution (Church, 1936a, 1936b; Turing, 1936-37). Turing's paper also introduced the abstract machine now called the Turing machine (BIO-TURING-001 Alan Turing).

In AI, Newell and Simon's Logic Theory Machine (1956) is generally regarded as an early program that proved theorems of propositional logic (Newell & Simon, 1956). Davis, Logemann and Loveland (1962) published a procedure for propositional theorem proving that is the ancestor of modern SAT solvers. Robinson (1965) introduced the resolution principle, a single inference rule suitable for machine implementation in first-order logic. Cook (1971) showed that propositional satisfiability is NP-complete, linking logic with complexity theory.

By the 1970s, researchers noted that classical logic is monotonic (adding premises never removes conclusions), which conflicts with everyday reasoning that retracts conclusions on new information. Reiter (1980) proposed default logic as a formalization of reasoning with defaults, one of several non-monotonic formalisms. Description logics, which restrict first-order logic to obtain decidable fragments, underlie ontology languages used in knowledge representation.

Recent work includes machine-learning systems that interact with formal proof systems. Polu and Sutskever (2020) trained a language model to generate proofs for the Metamath formalization. De Moura and Ullrich (2021) describe the Lean 4 theorem prover and programming language. Trinh et al. (2024) combined a language model with a symbolic deduction engine for Euclidean geometry.

#4.1 Syntax and semantics

A logic has a syntax (which strings are well-formed formulas) and a semantics (what formulas mean, typically via truth in models). Propositional logic has atomic propositions combined by connectives ($\neg, \wedge, \vee, \rightarrow$). First-order logic adds objects, predicates, functions and quantifiers $\forall, \exists$, for example

#4.2 Entailment, soundness and completeness

A set of formulas $\Gamma$ entails $\varphi$, written $\Gamma \models \varphi$, if $\varphi$ is true in every model of $\Gamma$. A proof system derives $\Gamma \vdash \varphi$ by syntactic rules. The system is sound if $\Gamma \vdash \varphi$ implies $\Gamma \models \varphi$, and complete if the converse holds. First-order logic admits sound and complete proof systems (Gödel, 1930), so valid formulas are semi-decidable: a procedure exists that halts with a proof for every valid formula (for example, resolution refutation; Robinson, 1965), but, by the undecidability results of Church (1936b) and Turing (1936-37), none can halt on every invalid one.

#4.3 Resolution and satisfiability

In resolution, formulas are converted to clausal form, and two clauses containing complementary literals are resolved to produce a new clause:

To prove $\Gamma \models \varphi$, one adds $\neg\varphi$ to $\Gamma$ and derives the empty clause (refutation), which signals unsatisfiability (Robinson, 1965). For propositional logic, the DLL procedure performs systematic search with unit propagation and backtracking (Davis et al., 1962), and modern conflict-driven solvers extend it. Satisfiability is NP-complete (Cook, 1971), so worst-case runtime is expected to be exponential even though many practical instances are solved quickly.

#4.4 Incompleteness

Gödel's first incompleteness theorem states that for any suitably consistent, effectively axiomatized theory that includes a sufficient amount of arithmetic, there is a sentence that is true but unprovable in the theory (Gödel, 1931; the consistency-only form is due to Rosser, 1936). The theorem limits what any formal system, including one used by an AI system, can prove about arithmetic. Claims that it limits machine intelligence relative to human intelligence require additional, contested philosophical premises and are not consequences of the theorem alone (FOUND-005 Philosophy of Mind and the Turing Test).

#4.5 Non-monotonic and uncertain reasoning

In default logic, a default rule has the form "if $\alpha$ holds and it is consistent to assume $\beta$, conclude $\gamma$" (Reiter, 1980). Probabilistic formalisms address uncertainty differently, representing degrees of belief rather than defaults (FOUND-008 Probability, Statistics and Bayesian Inference).

#4.6 Machine-checkable proof

Proof assistants such as Lean check every step of a proof against a small trusted kernel, so a verified proof is correct relative to the kernel and the stated definitions (de Moura & Ullrich, 2021). This property allows learned systems to propose proofs while a formal checker rejects invalid ones, as in the proof-search setting of Polu and Sutskever (2020).

• Propositional logic: decidable (satisfiability is NP-complete).
• First-order logic: expressive and semi-decidable.
• Higher-order and type-theoretic logics: used in proof assistants such as Lean.
• Modal and temporal logics: reasoning about necessity, knowledge, time; used in verification.
• Description logics: decidable fragments for ontologies.
• Non-monotonic logics: default logic and related systems (Reiter, 1980).
• Probabilistic and fuzzy logics: handle graded truth or uncertainty.
• Automated reasoning technologies: SAT and SMT solvers, resolution provers, interactive proof assistants.
• Neurosymbolic approaches: combine learned components with symbolic reasoning (Garcez & Lamb, 2023).

• Hardware and software verification. SAT/SMT solving and theorem proving are used to check designs and programs; the deductive core of these tools descends from Davis et al. (1962) and Robinson (1965).
• Knowledge-based systems and ontologies. Description logic reasoners support classification in large ontologies (FOUND-003 Knowledge Representation).
• Formal mathematics. Lean and similar systems are used for large formalization projects (de Moura & Ullrich, 2021).
• Neurosymbolic research demonstrations. AlphaGeometry (Trinh et al., 2024) reported solving 25 of 30 olympiad-level geometry problems in its test set, compared with ten for the previous best method it reported, using a language model to guide a symbolic deduction engine. This is a result for a specific problem set in one domain and a laboratory demonstration.
• Learned proof search. Polu and Sutskever (2020) is a research demonstration of language-model proof generation checked by a formal verifier.

Strengths. Soundness guarantees; transparent, inspectable derivations; precise semantics; the ability to verify results independently of how they were found.

Limitations.

• Undecidability and intractability: first-order validity is undecidable, and propositional satisfiability is NP-complete (Church, 1936b; Turing, 1936-37; Cook, 1971).
• Incompleteness of sufficiently rich theories (Gödel, 1931).
• The knowledge acquisition bottleneck: reasoning requires formalized knowledge, which is costly to write and incomplete.
• Brittleness: classical logic handles exceptions, uncertainty and vagueness poorly without extensions (Reiter, 1980).
• Autoformalization gap: translating informal problems into formal statements is itself a hard problem; systems that work in formal settings do not automatically transfer to informal mathematics.

Open questions. How best to integrate learned and symbolic reasoning; whether neural models can learn reliable deduction without explicit symbolic machinery; and how to scale formalization of knowledge.

As of 2026-10-15:

• The metatheoretic results (completeness of first-order logic, undecidability, incompleteness, NP-completeness of SAT) are Established.
• Practical SAT/SMT solvers and proof assistants are mature, deployed technologies.
• Learned proof search and neurosymbolic systems are active research. The reported results (Polu & Sutskever, 2020; Trinh et al., 2024) are Well Supported as demonstrations on the cited benchmarks, but their generality is Contested. Current performance of language models on formal mathematics changes rapidly and is tracked outside this stable article (see TECH-REASON-001 Reasoning Models and Test-Time Compute and MODEL-001).
• The debate whether symbolic structure is necessary for general intelligence, or whether it can emerge in neural networks, is Contested (Garcez & Lamb, 2023, argue for the neurosymbolic approach).

No registered forecast is made. Observed trends: growth in machine-checked mathematics and in AI systems that propose proofs for formal verification; research on combining language models with solvers and provers; and interest in using formal methods to verify properties of AI-enabled systems. Whether formal verification can provide guarantees about large learned models is an open question rather than a demonstrated capability.

• Foundational Concepts:
  • FOUND-003 Knowledge Representation: logic as a representation language.
  • FOUND-004 Computational Complexity in AI: complexity limits on reasoning.
• Related Methods & Technologies:
  • FOUND-007 Learning, Reasoning and Generalization: deduction versus induction.
  • HIST-003 Symbolic AI and the Perceptron: early logic-based AI.
  • BIO-TURING-001 Alan Turing: computability.
• Advanced Implications & Future Trajectories:
  • TECH-REASON-001 Reasoning Models and Test-Time Compute: learned reasoning in language models.
  • CAP-REASON-001 Reasoning, Planning and Long-Horizon Capability: measured reasoning capability.