--- id: FOUND-011 title: "Logic and Formal Systems" alternative_names: - "Mathematical Logic for AI" - "Automated Reasoning Foundations" category: "Foundations → Mathematics" volume: I chapter: 3 entry_type: "Standard Article" level: 3 status: "Draft" last_reviewed: 2026-10-15 version: "0.1.0" prerequisites: - "FOUND-003" related_entries: - "FOUND-004" - "FOUND-007" - "HIST-003" - "TECH-REASON-001" - "BIO-TURING-001" --- # Logic and Formal Systems ## 1. Concise Definition **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. ## 2. Overview & Significance Logic was the first major formalism for AI. The early programs of the 1950s and 1960s (see [[HIST-003] Symbolic AI and the Perceptron](../vol02_history/HIST-003_symbolic_ai_perceptron.md)) 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](FOUND-003_knowledge_representation.md)). 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](FOUND-004_computational_complexity.md)) 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). ## 3. Historical Development Modern formal logic dates from the late nineteenth century and the construction of quantificational logic as a formal language (Frege's *Begriffsschrift*, 1879) [VERIFICATION NEEDED: Frege primary source not checked]. In 1931 Gödel proved that any consistent, effectively axiomatized formal system capable of expressing elementary arithmetic is incomplete: there are true statements it cannot prove (Gödel, 1931). In 1936 Church and Turing independently showed that the *Entscheidungsproblem*, the problem of deciding validity of first-order formulas, has no algorithmic solution (Church, 1936; Turing, 1936-37). Turing's paper also introduced the abstract machine now called the Turing machine ([[BIO-TURING-001] Alan Turing](../vol10_people_organizations/BIO-TURING-001_alan_turing.md)). 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. Technical / Conceptual Explanation ### 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 $$\forall x\,\bigl(\mathrm{Human}(x) \rightarrow \mathrm{Mortal}(x)\bigr).$$ ### 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, so valid formulas are semi-decidable: a procedure exists that halts with a proof for every valid formula, but none can halt on every invalid one (Church, 1936; Turing, 1936-37; Robinson, 1965). ### 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: $$\frac{(A \vee \ell) \quad (B \vee \neg \ell)}{(A \vee B)}.$$ 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 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 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](FOUND-005_philosophy_of_mind.md)). ### 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](FOUND-008_probability_statistics_and_bayesian_inference.md)). ### 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). ## 5. Types, Components & Classifications - **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). ## 6. Applications & Concrete Examples - **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](FOUND-003_knowledge_representation.md)). - **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. ## 7. Advantages, Limitations & Unresolved Questions **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, 1936; 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. ## 8. Current State 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](../vol03_technical/TECH-REASON-001_reasoning_models_and_test_time_compute.md) 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). ## 9. Future Trajectory & Strategic Outlook 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. ## 10. Related Entries & Knowledge Graph - **Foundational Concepts**: - [[FOUND-003] Knowledge Representation](FOUND-003_knowledge_representation.md): logic as a representation language. - [[FOUND-004] Computational Complexity in AI](FOUND-004_computational_complexity.md): complexity limits on reasoning. - **Related Methods & Technologies**: - [[FOUND-007] Learning, Reasoning and Generalization](FOUND-007_learning_reasoning_and_generalization.md): deduction versus induction. - [[HIST-003] Symbolic AI and the Perceptron](../vol02_history/HIST-003_symbolic_ai_perceptron.md): early logic-based AI. - [[BIO-TURING-001] Alan Turing](../vol10_people_organizations/BIO-TURING-001_alan_turing.md): computability. - **Advanced Implications & Future Trajectories**: - [[TECH-REASON-001] Reasoning Models and Test-Time Compute](../vol03_technical/TECH-REASON-001_reasoning_models_and_test_time_compute.md): learned reasoning in language models. - [[CAP-REASON-001] Reasoning, Planning and Long-Horizon Capability](../vol04_capabilities/CAP-REASON-001_reasoning_planning_and_long_horizon_capability.md): measured reasoning capability. ## 11. References & Foundational Literature 1. Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. *Monatshefte für Mathematik und Physik*, 38, 173-198. https://doi.org/10.1007/BF01700692. [Incompleteness theorems. Checked against Crossref; the statement of the theorem is the standard textbook formulation.] 2. Church, A. (1936). An unsolvable problem of elementary number theory. *American Journal of Mathematics*, 58(2), 345. https://doi.org/10.2307/2371045. [Early result on unsolvability bearing on the Entscheidungsproblem. Checked against Crossref (Crossref lists the start page only).] 3. Turing, A. M. (1936-37). On computable numbers, with an application to the Entscheidungsproblem. *Proceedings of the London Mathematical Society*, s2-42(1), 230-265. https://doi.org/10.1112/plms/s2-42.1.230. [Introduces the Turing machine and shows the Entscheidungsproblem is unsolvable. Checked against Crossref, which dates the issue 1937.] 4. Newell, A., & Simon, H. A. (1956). The logic theory machine: A complex information processing system. *IRE Transactions on Information Theory*, 2(3), 61-79. https://doi.org/10.1109/TIT.1956.1056797. [Early theorem-proving program. Checked against Crossref.] 5. Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. *Communications of the ACM*, 5(7), 394-397. https://doi.org/10.1145/368273.368557. [Propositional proof search procedure underlying SAT solving. Checked against Crossref.] 6. Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. *Journal of the ACM*, 12(1), 23-41. https://doi.org/10.1145/321250.321253. [Resolution principle. Checked against Crossref.] 7. Cook, S. A. (1971). The complexity of theorem-proving procedures. *Proceedings of the Third Annual ACM Symposium on Theory of Computing*, 151-158. https://doi.org/10.1145/800157.805047. [NP-completeness of propositional satisfiability. Checked against Crossref.] 8. Reiter, R. (1980). A logic for default reasoning. *Artificial Intelligence*, 13(1-2), 81-132. https://doi.org/10.1016/0004-3702(80)90014-4. [Default logic as a non-monotonic formalism. Checked against Crossref.] 9. Polu, S., & Sutskever, I. (2020). Generative language modeling for automated theorem proving. arXiv:2009.03393 (preprint). [Language-model proof generation for Metamath. Authors and title checked against arXiv page.] 10. de Moura, L., & Ullrich, S. (2021). The Lean 4 theorem prover and programming language. In *Automated Deduction - CADE 28*, Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-030-79876-5_37. [Describes Lean 4. Checked against Crossref.] 11. Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. *Nature*, 625(7995), 476-482. https://doi.org/10.1038/s41586-023-06747-5. [AlphaGeometry: 25 of 30 test problems solved, versus ten for the prior best, per its abstract. Checked against Crossref abstract; five authors confirmed.] 12. Garcez, A. d'A., & Lamb, L. C. (2023). Neurosymbolic AI: The 3rd wave. *Artificial Intelligence Review*, 56(11), 12387-12406. https://doi.org/10.1007/s10462-023-10448-w. [Argues for combining neural learning and symbolic reasoning. Checked against Crossref.] ## 12. Evidential Classification Matrix | Section / Claim | Evidence Category | Supporting Source | Confidence / Status | | :--- | :--- | :--- | :--- | | Incompleteness of sufficiently rich consistent formal theories | Established | Gödel (1931) | High | | Undecidability of first-order validity | Established | Church (1936); Turing (1936-37) | High | | Resolution is a sound, refutation-complete procedure for first-order logic | Established | Robinson (1965) | High | | Propositional satisfiability is NP-complete | Established | Cook (1971) | High | | Default logic formalizes defeasible reasoning | Established (as a formalism) | Reiter (1980) | High | | LM-guided proof search succeeds on specific formal benchmarks | Well Supported (per benchmark) | Polu & Sutskever (2020); Trinh et al. (2024) | Moderate | | Neurosymbolic integration is necessary for general intelligence | Contested | Garcez & Lamb (2023) | Low | | Gödel's theorem shows machines cannot match human minds | Contested | None cited | Low; requires extra premises | ## 13. Revision History - **v0.1.0** (2026-10-15): Initial draft. Citations checked against arXiv/Crossref/publisher pages where marked; not independently fact-checked.