Document ID: V_2_07
Section: V_Mathematics_Information
Keywords: logic, formal logic, Aristotle, syllogism, Boolean algebra, Frege, Begriffsschrift, Russell, Whitehead, Principia Mathematica, Gödel, Turing, computability, decidability, predicate logic, propositional logic
Category Tags: mathematics, information
Cross-References: P_3_07 · ZD_1_01 · P_1_05 · S_1_01
Reliability Tier: Tier 1 (mathematical proofs and established historical scholarship)
Last Updated: Mar 07, 2026 | Source Count: 24 | Weighted Score: 44 | Source Confidence: [5/5] | Confidence: High

QUICK SUMMARY

Formal logic — the systematic study of valid inference — spans 2,400 years from Aristotle's syllogistic (c. 350 BCE) to Turing's computation theory (1936). Aristotle's Organon established the syllogism as the fundamental unit of deductive reasoning and dominated Western logic for nearly two millennia. The 19th century saw an explosion of innovation: George Boole (1854) algebraized logic, Gottlob Frege (1879) created modern predicate logic with quantifiers in his Begriffsschrift, and Giuseppe Peano developed symbolic notation for arithmetic. Russell and Whitehead's Principia Mathematica (1910–1913) attempted to derive all of mathematics from logic (logicism), but Gödel's incompleteness theorems (1931) showed that any consistent formal system powerful enough for arithmetic contains truths it cannot prove. Alan Turing (1936) resolved the Entscheidungsproblem (decision problem) by defining the Turing machine and proving that no algorithm can decide the truth of all mathematical statements — simultaneously founding theoretical computer science. The history of formal logic is the story of humanity's attempt to mechanize reasoning, its remarkable successes, and the discovery of its inherent limitations.

1. VERIFIED CLAIMS (Tier 1 — Peer-Reviewed / Established Scholarship)

1.1 Aristotle's syllogistic logic (c. 350 BCE)

• Aristotle (384–322 BCE) developed the syllogism — a deductive argument with two premises and a conclusion — in the Prior Analytics (part of the Organon).
• Example: "All men are mortal; Socrates is a man; therefore Socrates is mortal."
• Classified 256 possible syllogistic forms into 24 valid moods (later refined to 15 unconditionally valid moods in three figures, later four).
• Square of opposition: systematic relationships (contradiction, contrariety, subalternation) between categorical propositions (All S are P / No S are P / Some S are P / Some S are not P).
• Dominance: Aristotelian logic was the core of Western education (the trivium: grammar, logic, rhetoric) for roughly 2,000 years — Kant (1787) declared that logic "has not had to retrace a single step" since Aristotle.
• Limitations: Aristotelian logic cannot handle relations (e.g., "A is taller than B"), multiple quantifiers, or mathematical induction — these required the 19th-century revolution.

1.2 Stoic and medieval contributions

• Stoic logic (Chrysippus, c. 279–206 BCE): developed propositional logic — inference rules governing "if…then," "or," "and" — complementing Aristotle's term logic. Five basic inference schemas (indemonstrables).
• Medieval logicians: Peter Abelard (12th c., modal logic), William of Ockham (14th c., nominalism and supposition theory), Jean Buridan (14th c., consequences and self-reference paradoxes).
• Indian logic: Nyāya school (Gautama's Nyāya Sūtras, c. 2nd c. CE) independently developed a five-membered syllogism and sophisticated theories of inference (anumāna), perception, and debate rules.
• Buddhist logic: Dignāga (5th–6th c. CE) and Dharmakīrti (7th c. CE) developed formal theories of inference remarkably parallel to Western developments.

1.3 Boole, De Morgan, and the algebraization of logic (1847–1854)

• George Boole (1815–1864), The Laws of Thought (1854): reformulated logic as algebra — propositions as variables (0 or 1), conjunction as multiplication, disjunction as addition, negation as complement.
• Boolean algebra became the mathematical foundation of digital circuit design (Shannon's master's thesis, 1938, showed that switching circuits implement Boolean algebra).
• Augustus De Morgan (1806–1871): De Morgan's laws ($\neg(A \wedge B) = \neg A \vee \neg B$), formalized the logic of relations.
• Together, Boole and De Morgan liberated logic from Aristotelian term structure and opened it to mathematical treatment.

1.3b Properties of propositional and first-order logic

Key meta-logical results:

• Soundness: any theorem derivable in the system is logically valid — the proof system never produces false conclusions from true premises.
• Gödel's completeness theorem (1929, not to be confused with the incompleteness theorems): every logically valid first-order sentence is provable in first-order logic. First-order logic is complete — semantic truth and syntactic provability coincide.
• Compactness theorem: a set of first-order sentences has a model if and only if every finite subset has a model — a fundamental tool in model theory, yielding the existence of nonstandard models of arithmetic.
• Decidability: propositional logic is decidable (truth tables, resolution). First-order logic is undecidable (Church and Turing, 1936) — no algorithm can determine validity of all first-order sentences. However, several fragments (monadic FOL, the Bernays-Schönfinkel class) are decidable.
• Löwenheim-Skolem theorem: if a first-order theory has an infinite model, it has models of every infinite cardinality — first-order logic cannot uniquely characterize structures like the natural numbers or the reals.

1.4 Frege's Begriffsschrift and modern predicate logic (1879)

Gottlob Frege (1848–1925):

• Begriffsschrift ("Concept-Script," 1879): invented modern predicate logic with quantifiers (∀, "for all"; ∃, "there exists"), variables, functions, and a formal proof system — the single most important advance in logic since Aristotle.
• Distinguished sense (Sinn) from reference (Bedeutung) — foundational for philosophy of language.
• Die Grundlagen der Arithmetik (1884): attempted to reduce arithmetic to logic (logicism) — defining numbers as equivalence classes of concepts.
• Grundgesetze der Arithmetik (vol. 1, 1893; vol. 2, 1903): the full formal derivation — but just before vol. 2's publication, Bertrand Russell informed Frege that his system was inconsistent (Russell's Paradox: the set of all sets that don't contain themselves).
• Frege's notation was two-dimensional and never adopted, but his logical system — translated into modern notation by Peano and Russell — remains the foundation of mathematical logic.

1.5 Russell, Whitehead, and Principia Mathematica (1910–1913)

• Bertrand Russell (1872–1970) and Alfred North Whitehead (1861–1947): Principia Mathematica (3 volumes, 1910–1913) — the most ambitious attempt to derive all of mathematics from purely logical axioms.
• To avoid Russell's Paradox, they introduced the theory of types — a hierarchy forbidding self-referential set membership.
• The proof that $1 + 1 = 2$ appears on page 379 of Volume I (proposition *54.43), with the note "the above proposition is occasionally useful."
• Logicism — the thesis that mathematics is reducible to logic — was the driving philosophical program. While Principia demonstrated the power of formal systems, Gödel's theorems (1931) showed that the logicist program cannot be fully completed.

1.6 Gödel's incompleteness theorems (1931)

Kurt Gödel (1906–1978):

• First Incompleteness Theorem: any consistent formal system $F$ capable of expressing basic arithmetic contains a statement $G$ that is true but unprovable within $F$. (Gödel constructed $G$ to say, in effect, "this statement is not provable in $F$.")
• Second Incompleteness Theorem: such a system $F$ cannot prove its own consistency (unless it is inconsistent).
• Method: Gödel numbering — encoding logical formulas as natural numbers, allowing the system to "talk about itself."
• Impact: destroyed Hilbert's program to prove mathematics consistent and complete from finitary methods. (See also V_2_06.)
• Gödel's theorems do not imply that mathematics is unreliable — they show that no single formal system can capture all mathematical truth.

1.7 Turing and the Entscheidungsproblem (1936)

Alan Turing (1912–1954):

• Hilbert's Entscheidungsproblem (1928): is there an algorithm that can determine the truth or falsity of any mathematical statement?
• Turing (1936), "On Computable Numbers": defined the Turing machine — a theoretical device with an infinite tape, a read/write head, and a finite set of states — capable of computing anything that is computable by any mechanical process.
• Proved the halting problem is undecidable: no algorithm can determine, for all programs and inputs, whether the program halts or runs forever.
• Consequence: the Entscheidungsproblem has no solution — there are mathematical questions that no algorithm can answer. (Alonzo Church proved this independently using lambda calculus in 1936.)
• The Turing machine became the foundational model of theoretical computer science and the basis for the Church-Turing thesis.

1.8 Proof theory: from Gentzen to proof assistants

• Gerhard Gentzen (1909–1945): invented the sequent calculus and natural deduction (1935) — formal proof systems that mirror how mathematicians actually reason. Proved the consistency of Peano arithmetic using transfinite induction up to ε₀ (just beyond what Peano arithmetic itself can formalize).
• Cut-elimination theorem (Gentzen, 1935): the Hauptsatz — any proof in the sequent calculus can be transformed into a "direct" proof without detours (cuts). A foundational result for proof theory, with applications to decidability and interpolation.
• Curry-Howard correspondence (1958/1969): a deep isomorphism between proofs and programs — propositions are types, proofs are programs. A proof of $A \to B$ corresponds to a function from type $A$ to type $B$. This bridge between logic and computer science underlies modern type theory and functional programming.
• Proof assistants: Coq, Lean, Isabelle/HOL, Agda — software tools for writing machine-checkable proofs. Notable achievements: Gonthier's formal proof of the four-color theorem (2005) and odd-order theorem (2012) in Coq; Hales's Flyspeck project verifying the Kepler conjecture in Isabelle/HOL (2014).
• Constructive mathematics and HoTT: intuitionism (Brouwer, Heyting) rejects the law of excluded middle — a proof of existence must construct a witness. Homotopy Type Theory (HoTT, 2013 "Univalent Foundations" book): merges Martin-Löf type theory with homotopy theory, proposing a new foundation for mathematics where equality has geometric (homotopical) content.

2. CREDIBLE BUT DEBATED CLAIMS (Tier 2 — Academic / Debated)

2.1 The Church-Turing thesis

• Claim: any function computable by any physically realizable device is computable by a Turing machine.
• Status: widely accepted but unprovable (it is a thesis about the physical world, not a mathematical theorem).
• Challenges: quantum computing does not violate the thesis (quantum computers compute the same functions, just faster for some problems), but hypercomputation proposals (super-Turing machines, oracle machines) remain speculative and controversial.

2.2 Whether logic captures all valid reasoning

• Formal logic captures deductive reasoning but may not capture all forms of valid inference — abductive reasoning (inference to the best explanation), analogical reasoning, and practical reasoning are not fully formalized.
• Some philosophers (e.g., Toulmin, 1958) argue that formal logic is too narrow to model real-world argumentation.

3. SPECULATIVE CLAIMS (Tier 3 — Possible but Unverified)

3.1 Ancient precursors to formal logic beyond Greece and India

Claims that ancient Egyptians, Chinese (Mohist logic), or Mesoamericans had formal logical systems comparable to Aristotelian or Nyāya logic are largely unsubstantiated. The Mohist Canons (c. 400 BCE) contain interesting logical insights but do not constitute a formal system. Egyptian wisdom literature contains reasoned argument but not systematic logic.

4. DUBIOUS OR FRINGE CLAIMS (Tier 4 — No Credible Source / Contradicted by Evidence)

4.1 Gödel proved that truth is unknowable

A common misinterpretation: Gödel proved that specific formal systems cannot prove all truths expressible within them — not that mathematical truth is unknowable. The unprovable statement $G$ is known to be true (by the meta-mathematical argument). The theorems concern the limitations of formal proof systems, not of human knowledge.

COUNTER-ARGUMENTS & CRITICISMS

IMAGES

BIBLIOGRAPHY

1. Aristotle | 1989 | ∅ | Prior Analytics | ∅ | ∅ | Translated by Robin Smith | ∅ | doi:10.1017/s0009840x00253420 | ∅ | ∅ | Indianapolis: Hackett
2. Boole, George | 1854 | ∅ | An Investigation of the Laws of Thought | ∅ | ∅ | London: Walton and Maberly | ∅ | isbn:9781019245248 | ∅ | ∅ | ∅
3. Frege, Gottlob | 1879 | ∅ | Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens | ∅ | ∅ | Halle: Louis Nebert | ∅ | doi:10.2307/2271662 | ∅ | ∅ | ∅
4. Russell, Bertrand; Alfred North Whitehead | 1910–1913 | ∅ | Principia Mathematica | ∅ | ∅ | 3 vols | ∅ | doi:10.1126/science.35.890.106 | ∅ | ∅ | Cambridge: Cambridge University Press
5. Gödel, Kurt | 1931 | "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" | Monatshefte für Mathematik und Physik | ∅ | 38::173–198 | ∅ | ∅ | doi:10.1007/bf01700692 | ∅ | ∅ | ∅
6. Turing, Alan M | 1936 | "On Computable Numbers, with an Application to the Entscheidungsproblem" | Proceedings of the London Mathematical Society | ∅ | 42::230–265 | ∅ | ∅ | doi:10.1112/plms/s2-42.1.230 | ∅ | ∅ | ∅
7. Church, Alonzo | 1936 | "An Unsolvable Problem of Elementary Number Theory" | American Journal of Mathematics | ∅ | 58::345–363 | ∅ | ∅ | ∅ | ∅ | ∅ | ∅
8. Kneale, William; Martha Kneale | 1962 | ∅ | The Development of Logic | ∅ | ∅ | Oxford: Clarendon Press | ∅ | ∅ | ∅ | ∅ | ∅
9. van Heijenoort, Jean (ed.) | 1879–1931 | ∅ | From Frege to Gödel: A Source Book in Mathematical Logic | ∅ | ∅ | Cambridge, MA: Harvard University Press, 1967 | ∅ | ∅ | ∅ | ∅ | ∅
10. Hodges, Andrew | 1983 | ∅ | Alan Turing: The Enigma | ∅ | ∅ | London: Burnett Books | ∅ | ∅ | ∅ | ∅ | ∅
11. Matilal, Bimal Krishna | 1998 | ∅ | The Character of Logic in India | ∅ | ∅ | Albany: SUNY Press | ∅ | ∅ | ∅ | ∅ | ∅
12. Shannon, Claude E | 1938 | "A Symbolic Analysis of Relay and Switching Circuits" | Transactions of the AIEE | ∅ | 57::713–723 | ∅ | ∅ | ∅ | ∅ | ∅ | ∅
13. Toulmin, Stephen | 1958 | ∅ | The Uses of Argument | ∅ | ∅ | Cambridge: Cambridge University Press | ∅ | ∅ | ∅ | ∅ | ∅
14. Copeland, B | 2004 | ∅ | The Essential Turing | ∅ | ∅ | Jack, ed | ∅ | ∅ | ∅ | ∅ | Oxford: Oxford University Press
15. Franzén, Torkel | 2005 | ∅ | Gödel's Theorem: An Incomplete Guide to Its Use and Abuse | ∅ | ∅ | Wellesley: A K Peters | ∅ | ∅ | ∅ | ∅ | ∅
16. Stillwell, John | 2010 | ∅ | Roads to Infinity: The Mathematics of Truth and Proof | ∅ | ∅ | Natick: A K Peters | ∅ | ∅ | ∅ | ∅ | ∅
17. Davis, Martin | 2000 | ∅ | The Universal Computer: The Road from Leibniz to Turing | ∅ | ∅ | New York: W.W | ∅ | ∅ | ∅ | ∅ | Norton
18. Ganeri, Jonardon | 2004 | "Indian Logic" | Handbook of the History of Logic | ∅ | ∅ | In , vol | ∅ | ∅ | ∅ | ∅ | 1, edited by Dov M; Gabbay and John Woods, 309 395; Amsterdam: Elsevier
19. Smith, Peter. . | 2013 | ∅ | An Introduction to Gödel's Theorems | ∅ | ∅ | Cambridge: Cambridge University Press | 2nd | ∅ | ∅ | ∅ | ∅
20. Mancosu, Paolo, Richard Zach; Calixto Badesa | 1900–1935 | "The Development of Mathematical Logic from Russell to Tarski, " | The Development of Modern Logic | ∅ | ∅ | In , edited by Leila Haaparanta, 318 470 | ∅ | ∅ | ∅ | ∅ | Oxford: Oxford University Press, 2009
21. Gentzen, Gerhard | 1935 | "Untersuchungen über das logische Schließen" | Mathematische Zeitschrift | ∅ | 39::176–210,405–431 | ∅ | ∅ | ∅ | ∅ | ∅ | ∅
22. Sorensen, Morten Heine; Paweł Urzyczyn | 2006 | ∅ | Lectures on the Curry-Howard Isomorphism | ∅ | ∅ | Amsterdam: Elsevier | ∅ | ∅ | ∅ | ∅ | ∅
23. The Univalent Foundations Program | 2013 | ∅ | Homotopy Type Theory: Univalent Foundations of Mathematics | ∅ | ∅ | Princeton: Institute for Advanced Study | ∅ | ∅ | ∅ | ∅ | ∅
24. Gonthier, Georges | 2008 | "Formal Proof — The Four-Color Theorem" | Notices of the AMS | ∅ | 55::1382–1393 | ∅ | ∅ | ∅ | ∅ | ∅ | ∅

CROSS-REFERENCE INDEX

Document V_2_07 · Created Mar 07, 2026 · TheoriesOfAnything Knowledge Base

<table border="1" cellpadding="12" cellspacing="0" style="border-collapse: collapse; border: 2px solid #888; margin-top: 2em; background: #fafafa;">

<tr><td>

⚠️ AI-Assisted Research Disclaimer

This document was generated and structured with the assistance of AI tools.

While every effort is made to ensure accuracy, AI-assisted content may

contain errors, misattributions, or unintended inaccuracies. **Always

verify claims, dates, and sources independently** before citing or relying

on any information presented here.

• Sources may contain errors. Bibliography entries and cross-references

are checked by automated systems, but mistakes can occur. If something

looks wrong, it may be.

• Speculative and unverified claims are clearly labeled. This project

uses a four-tier evidence system:

• Tier 1 — Verified: Peer-reviewed, established scientific consensus.
• Tier 2 — Credible: Academically supported, debated but grounded.
• Tier 3 — Speculative: Plausible but unverified by mainstream science.
• Tier 4 — Dubious: No credible support or contradicted by evidence.
• This project maps multiple perspectives — not a single truth. Mainstream,

alternative, and skeptical viewpoints are presented side by side for

critical comparison, not endorsement. Inclusion does not imply agreement.

• We are actively improving. Source verification, factuality scoring,

and bibliography enrichment are ongoing. Each revision adds stronger

citations, corrects identified errors, and expands coverage.

📖 For full details on our verification methodology, scoring systems, and

quality metrics, see: Fact-Checking & Verification Systems

Think Openly. Check the sources. Draw your own conclusions.

</td></tr>

</table>