Logic and Its Major Schools逻辑学与主要流派
Formal reasoning / foundations形式推理 / 数学基础Proof / Model / Set / Computability / TypeMathJax formulasMathJax 公式
What Logic Studies
Logic studies valid inference, formal consequence, truth, proof, meaning, computation, and the structure of theories. It asks what follows from what, which forms of reasoning preserve truth, how languages can be interpreted, and what can or cannot be proved or computed inside a formal system.
Modern logic comprises a cluster of linked traditions: philosophical logic analyzes concepts of truth and consequence; mathematical logic studies formal systems with mathematical tools; computational logic turns proof and semantics into algorithms; linguistic logic studies meaning and quantification in natural language; non-classical logics revise or extend classical assumptions.
Validity
An argument is valid when no interpretation makes all premises true and the conclusion false.
Proof
A proof is a finite, rule-governed derivation. Proof theory studies proofs as mathematical objects.
Model
A model interprets a formal language in a domain, assigning meanings to constants, functions, and predicates.
Historical Timeline
Ancient Greece
Aristotle developed syllogistic logic, analyzing categorical propositions and valid argument forms. Stoic logicians explored propositional reasoning, conditionals, and inference patterns.
Indian and Chinese traditions
Nyaya logic studied inference, debate, and epistemic warrants. Mohist texts in China developed analyses of names, distinctions, and argument patterns.
Medieval scholastic logic
Medieval thinkers developed supposition theory, obligationes, modal reasoning, insolubles, and sophisticated semantic distinctions.
Leibniz to Boole
Leibniz imagined a calculus of reasoning. Boole and De Morgan algebraized logic, making formal manipulation central.
Frege and Peano
Frege's Begriffsschrift created modern quantificational logic; Peano's notation helped formalize arithmetic.
Russell, Hilbert, Gödel
Logicism, formalism, completeness, incompleteness, and proof theory became central to foundations of mathematics.
Tarski, Church, Turing
Truth definitions, computability, lambda calculus, and Turing machines connected logic with semantics and computation.
Late 20th century to now
Model theory, set theory, type theory, modal logic, category-theoretic logic, automated theorem proving, proof assistants, and AI reasoning systems expand the field.
Core Formal Principles
Semantic consequence
\( \Gamma \vDash \varphi \iff \forall \mathcal{M}\,(\mathcal{M}\vDash\Gamma \Rightarrow \mathcal{M}\vDash\varphi) \)
Truth preservation across every model. This is the semantic notion of validity.
Syntactic derivability
\( \Gamma \vdash \varphi \)
There exists a formal derivation of \(\varphi\) from assumptions \(\Gamma\) by specified inference rules.
Soundness
\( \Gamma \vdash \varphi \Rightarrow \Gamma \vDash \varphi \)
Everything provable by the system is semantically valid.
Completeness
\( \Gamma \vDash \varphi \Rightarrow \Gamma \vdash \varphi \)
Everything semantically valid is derivable. First-order logic has this theorem; stronger systems may not.
Compactness
\( \Gamma \text{ satisfiable } \iff \text{ every finite } \Delta\subseteq\Gamma \text{ is satisfiable} \)
A first-order theory has a model if every finite fragment has a model.
Incompleteness
\( T \supseteq Q,\ T \text{ consistent and r.e.} \Rightarrow \exists G_T\,(T\nvdash G_T \land T\nvdash \neg G_T) \)
Any sufficiently strong consistent recursively enumerable theory cannot prove every arithmetical truth.
Computability
\( A \leq_T B \iff A \text{ is computable with oracle } B \)
Reducibility compares the informational difficulty of decision problems.
Curry-Howard
\( \text{propositions} \simeq \text{types},\quad \text{proofs} \simeq \text{programs} \)
Logical proof and typed computation share one structural language.
A complete theory overview must distinguish object language from metalanguage, syntax from semantics, proof from truth, and formal calculi from intended mathematical interpretation.
Major Schools and Tasks
| School | Main task | Core questions | Detailed role |
|---|---|---|---|
| Classical propositional logic | Analyze truth-functional reasoning. | How do connectives preserve truth? | Studies formulas built from \(\neg,\land,\lor,\to\); gives truth tables, normal forms, SAT, tautology, and proof systems. |
| First-order logic | Formalize quantification over individuals. | What follows from predicates, variables, equality, and quantifiers? | Standard language of modern mathematics; supports theories of groups, orders, fields, arithmetic fragments, and formal semantics. |
| Proof theory | Study proofs as formal objects. | Can proofs be normalized, eliminated, bounded, or transformed? | Includes sequent calculus, natural deduction, cut elimination, ordinal analysis, constructive proof, and consistency programs. |
| Model theory | Study structures satisfying theories. | What do formal theories say about possible models? | Analyzes elementary equivalence, definability, compactness, Löwenheim-Skolem, stability, categoricity, and applications to algebra and geometry. |
| Set theory | Provide a universe for mathematics. | Which axioms govern collections, infinity, choice, and continuum? | Studies ZFC, large cardinals, forcing, independence, inner models, determinacy, and foundations of mathematical objects. |
| Computability / recursion theory | Classify effective procedures and undecidability. | What can be computed, decided, or reduced? | Studies Turing machines, partial recursive functions, degrees, halting problem, arithmetical hierarchy, and algorithmic limits. |
| Type theory | Connect logic, computation, and foundations. | How can propositions be represented as types? | Includes simply typed lambda calculus, dependent type theory, Martin-Löf type theory, homotopy type theory, proof assistants. |
| Modal logic | Formalize necessity, possibility, knowledge, time, obligation. | How do truth conditions vary across worlds or states? | Uses Kripke frames; supports epistemic, temporal, deontic, dynamic, provability, and description logics. |
| Non-classical logics | Revise classical assumptions. | What changes if excluded middle, explosion, bivalence, or monotonicity fails? | Includes intuitionistic, paraconsistent, relevant, many-valued, fuzzy, substructural, linear, and default logics. |
| Philosophical and linguistic logic | Analyze meaning, truth, reference, conditionals, and language. | How do formal tools clarify natural reasoning? | Studies formal semantics, pragmatics, vagueness, counterfactuals, truth theories, quantifier scope, and logical consequence. |
Famous Logicians and Core Views
Logic develops through a long chain of thinkers. The following selection marks the main turning points from syllogistic reasoning to mathematical logic, model theory, computability, and type-theoretic foundations; it does not claim to be exhaustive.
Aristotle 384-322 BCE
Greek philosopher who systematized syllogistic reasoning in the Organon. His logic analyzed categorical propositions and valid inference forms.
Core view: validity depends on form, not on the empirical content of the terms.
Gottfried W. Leibniz 1646-1716
Imagined a universal symbolic language and a calculus of reasoning in which disputes could be settled by calculation.
Core view: reasoning can be formalized as symbolic calculation.
George Boole 1815-1864
Created an algebra of logic, treating logical operations with mathematical symbols and equations.
Core view: logic can be represented as an algebra of classes and truth operations.
Gottlob Frege 1848-1925
Founded modern predicate logic with quantifiers and variables, and argued that arithmetic could be grounded in logic.
Core view: the structure of propositions is function-argument, and quantification is central to formal reasoning.
Bertrand Russell 1872-1970
With Whitehead, developed logicism in Principia Mathematica and exposed Russell's paradox in naive set theory.
Core view: mathematical foundations require type restrictions or other safeguards against self-reference.
David Hilbert 1862-1943
Proposed Hilbert's program: formalize mathematics and prove its consistency by finitary means.
Core view: axiomatic systems should be complete, consistent, and formally controlled.
Kurt Gödel 1906-1978
Proved first-order completeness and the incompleteness theorems for arithmetic-strength formal systems.
Core view: formal proof has exact limits; truth in arithmetic outruns any sufficiently strong consistent computable proof system.
Alfred Tarski 1901-1983
Developed model-theoretic semantics and a rigorous definition of truth for formal languages.
Core view: truth must be defined in a metalanguage, and logical consequence is semantic preservation across models.
Alonzo Church 1903-1995
Created lambda calculus and helped define effective calculability; his work shaped computability and functional programming.
Core view: computable functions can be captured by formal calculi such as lambda calculus.
Alan Turing 1912-1954
Defined Turing machines and proved limits of decision procedures, including the unsolvability of the halting problem.
Core view: computation can be modeled by mechanical symbol manipulation, revealing precise undecidable boundaries.
Gerhard Gentzen 1909-1945
Developed natural deduction and sequent calculus, proving cut elimination and advancing proof-theoretic consistency methods.
Core view: the structure of proofs can be normalized and studied directly.
Saul Kripke 1940-2022
Transformed modal logic with possible-world semantics and influenced philosophy of language, necessity, and naming.
Core view: modal truth depends on accessibility relations among possible worlds.
Dana Scott 1932-
Advanced model theory, modal logic, and domain theory, connecting logic with denotational semantics of programs.
Core view: meanings of programs and logical systems can be given by structured mathematical domains.
Per Martin-Löf 1942-
Developed intuitionistic dependent type theory, a foundation for constructive mathematics and modern proof assistants.
Core view: propositions are types, and knowing a proposition means possessing a construction of it.
逻辑学研究什么
逻辑学研究有效推理、形式后承、真、证明、意义、计算，以及理论的结构条件。除了“如何推理”，它还会追问：什么可以从什么推出，哪些推理形式能够稳定保持真，语言如何被解释，以及在一个形式系统内部，究竟有什么能够被证明、被计算，又有什么注定不能。
现代逻辑学是一组彼此连通的传统，并非一个单一主题。哲学逻辑分析真、后承、指称与条件句等概念；数理逻辑用数学工具研究形式系统；计算逻辑把证明与语义转化为算法问题；语言逻辑关注自然语言中的意义、量化与结构；非经典逻辑则通过修订或扩展经典假设，探索不同推理制度的边界。
有效性
如果不存在任何一种解释，能够让所有前提为真而结论为假，那么这项论证就是有效的。
证明
证明是有限且受规则约束的推导过程。证明论则把证明本身当作数学对象来研究。
模型
模型是在某个论域中对形式语言进行解释的结构，它为常元、函数与谓词赋予确定意义。
发展历史 Timeline
古希腊
亚里士多德系统发展三段论，分析范畴命题与有效论证形式；斯多亚逻辑学家则进一步研究命题推理、条件句与推理模式。
印度与中国传统
印度正理派围绕推理、辩论与知识根据展开系统分析；中国墨家文本也发展了关于名、辩、类与论证结构的独特讨论。
中世纪经院逻辑
中世纪思想家推进了指代理论、义务辩论、模态推理、悖论处理与精细语义区分，使逻辑分析更趋复杂。
莱布尼茨到布尔
莱布尼茨设想“理性演算”，希望争论能像计算一样被处理；布尔与德摩根则把逻辑代数化，使形式操作成为核心方法。
弗雷格与皮亚诺
弗雷格以《概念文字》建立现代量词逻辑的基本框架，皮亚诺记号则推动了算术与形式语言的标准化。
罗素、希尔伯特、哥德尔
逻辑主义、形式主义、完备性、不完备性与证明论，在这一时期集中进入数学基础研究。
塔斯基、丘奇、图灵
真定义、可计算性、λ 演算与图灵机模型，把逻辑与语义理论、算法思想和计算科学紧密连接起来。
20 世纪后期至今
模型论、集合论、类型论、模态逻辑、范畴逻辑、自动定理证明、证明助手以及 AI 推理系统，持续扩展着逻辑学的边界。
核心形式原理
语义后承
\( \Gamma \vDash \varphi \iff \forall \mathcal{M}\,(\mathcal{M}\vDash\Gamma \Rightarrow \mathcal{M}\vDash\varphi) \)
如果一个结论在所有满足前提的模型中都为真，那么它就在语义上由这些前提出发成立。这是有效性的标准语义定义。
句法可推导
\( \Gamma \vdash \varphi \)
这表示存在一条按照指定推理规则展开的形式推导，可以从假设 \(\Gamma\) 得到 \(\varphi\)。
可靠性
\( \Gamma \vdash \varphi \Rightarrow \Gamma \vDash \varphi \)
一个系统如果可靠，就意味着它所证明出来的东西，在语义上都确实有效。
完备性
\( \Gamma \vDash \varphi \Rightarrow \Gamma \vdash \varphi \)
如果某个结论在语义上总是成立，那么系统也应当能够把它形式化地推导出来。一阶逻辑满足这一定理，但更强的系统未必如此。
紧致性
\( \Gamma \text{ 可满足 } \iff \Gamma \text{ 的每个有限子集 } \Delta \text{ 可满足} \)
对于一阶理论来说，只要每一个有限片段都有模型，整个理论也就有模型。
不完备性
\( T \supseteq Q,\ T \text{ consistent and r.e.} \Rightarrow \exists G_T\,(T\nvdash G_T \land T\nvdash \neg G_T) \)
哥德尔不完备性定理说明：任何足够强且一致的递归可枚举理论，都无法囊括全部算术真理。
可计算性
\( A \leq_T B \iff A \text{ is computable with oracle } B \)
图灵归约用于比较不同判定问题之间的信息难度，判断一个问题是否能借助另一个问题的能力被计算出来。
Curry-Howard 对应
\( \text{命题} \simeq \text{类型},\quad \text{证明} \simeq \text{程序} \)
这一对应揭示了逻辑证明与带类型计算之间的深层同构关系，说明命题、证明与程序可以共享同一种结构语言。
要真正理解这些原理，必须始终区分对象语言与元语言、句法与语义、证明与真，以及形式演算与其预期数学解释之间的层次差异。
主要流派、任务与详细介绍
如果把现代逻辑学想成一座城市，那么不同流派更像彼此连通的功能区，而不是互相隔绝的小王国。有的传统更关心“什么算有效证明”，有的更关心“一个理论有哪些模型”，有的追问“什么能够被算法判定”，也有的尝试解释自然语言、知识状态和可能世界中的推理变化。这些传统分工不同，却经常共享形式工具，也会互相借用成果。
因此，下表不应被读成死板分类，而应被看成一张导航图。它帮助读者先把主要问题域分开，再理解这些问题如何在数学基础、计算机科学、语言分析和哲学讨论之间来回流动。
| 流派 | 主要任务 | 核心问题 | 详细作用 |
|---|---|---|---|
| 经典命题逻辑 | 分析真值函数推理。 | 联结词如何保持真？ | 研究由 \(\neg,\land,\lor,\to\) 构成的公式；包含真值表、范式、SAT、重言式和证明系统。 |
| 一阶逻辑 | 形式化个体量化。 | 谓词、变量、等词和量词能推出什么？ | 现代数学的标准语言；支持群、序、域、算术片段和形式语义学等理论。 |
| 证明论 | 把证明作为形式对象研究。 | 证明能否规范化、消去、界定或变换？ | 包括相继式演算、自然演绎、切消、序数分析、构造性证明和一致性纲领。 |
| 模型论 | 研究满足理论的结构。 | 形式理论如何约束可能模型？ | 分析初等等价、可定义性、紧致性、Löwenheim-Skolem、稳定性、范畴性，以及代数和几何应用。 |
| 集合论 | 为数学提供宇宙。 | 哪些公理支配集合、无穷、选择和连续统？ | 研究 ZFC、大基数、强迫法、独立性、内模型、决定性和数学对象基础。 |
| 可计算性 / 递归论 | 分类有效过程和不可判定性。 | 什么能够被计算、判定或归约？ | 研究图灵机、部分递归函数、度、停机问题、算术层级和算法极限。 |
| 类型论 | 连接逻辑、计算和基础。 | 命题如何表示为类型？ | 包括简单类型 λ 演算、依值类型论、Martin-Löf 类型论、同伦类型论和证明助手。 |
| 模态逻辑 | 形式化必然、可能、知识、时间、义务。 | 真值如何随可能世界或状态变化？ | 使用 Kripke 框架；支持认知、时序、道义、动态、可证明性和描述逻辑。 |
| 非经典逻辑 | 修改经典假设。 | 如果排中律、爆炸律、二值性或单调性失效会怎样？ | 包括直觉主义、次协调、相干、多值、模糊、子结构、线性和默认逻辑。 |
| 哲学逻辑与语言逻辑 | 分析意义、真、指称、条件句和语言。 | 形式工具如何澄清自然推理？ | 研究形式语义、语用、模糊性、反事实、真理论、量词辖域和逻辑后承。 |
真正进入这些分支之后，最重要的是学会辨认每个分支究竟在处理哪一种“限制条件”：真值限制、证明限制、模型限制、计算限制，还是语言解释的限制，并非死记名称。
著名逻辑学家与主要观点
逻辑学的发展是一条很长的思想链。下面这些人物不是完整名录，但他们分别处在三段论、代数逻辑、数理逻辑、模型论、可计算性和类型论发展的若干转折处。
亚里士多德 384-322 BCE
古希腊哲学家，在《工具论》中系统化三段论，分析范畴命题和有效推理形式。
主要观点：有效性取决于推理形式，而不是词项的经验内容。
莱布尼茨 1646-1716
设想一种普遍符号语言和理性演算，希望争论可以通过计算来解决。
主要观点：推理可以被形式化为符号计算。
乔治·布尔 1815-1864
创立逻辑代数，用数学符号和方程处理逻辑运算。
主要观点：逻辑可以表示为类与真值运算的代数。
戈特洛布·弗雷格 1848-1925
以量词和变量建立现代谓词逻辑，并主张算术可以奠基于逻辑。
主要观点：命题结构是函数-论元结构，量化是形式推理的核心。
伯特兰·罗素 1872-1970
与怀特海发展《数学原理》的逻辑主义，同时揭示朴素集合论中的罗素悖论。
主要观点：数学基础必须通过类型限制或其他机制避免自指悖论。
大卫·希尔伯特 1862-1943
提出希尔伯特纲领：把数学形式化，并用有限主义方法证明其一致性。
主要观点：公理系统应追求完备、一致，并接受严格的形式控制。
库尔特·哥德尔 1906-1978
证明一阶逻辑完备性定理，以及关于足够强形式系统的两个不完备性定理。
主要观点：形式证明有精确边界；算术真理会超出任何足够强且一致的可计算证明系统。
阿尔弗雷德·塔斯基 1901-1983
发展模型论语义，并为形式语言给出严格的真定义。
主要观点：真必须在元语言中定义，逻辑后承是在模型间保持真。
阿隆佐·丘奇 1903-1995
创立 λ 演算，参与定义有效可计算性，深刻影响可计算性理论和函数式编程。
主要观点：可计算函数可以由 λ 演算等形式演算刻画。
艾伦·图灵 1912-1954
定义图灵机，证明判定程序的限制，包括停机问题不可解。
主要观点：计算可以被机械符号操作建模，并由此显出不可判定的精确边界。
格哈德·根岑 1909-1945
发展自然演绎和相继式演算，证明切消定理，并推进证明论一致性方法。
主要观点：证明结构本身可以规范化，并作为对象被直接研究。
索尔·克里普克 1940-2022
以可能世界语义重塑模态逻辑，并影响语言哲学、必然性和命名理论。
主要观点：模态真值依赖可能世界之间的可达关系。
达纳·斯科特 1932-
推进模型论、模态逻辑和域理论，把逻辑与程序指称语义连接起来。
主要观点：程序和逻辑系统的意义可以由结构化的数学域给出。
佩尔·马丁-洛夫 1942-
发展直觉主义依值类型论，成为构造性数学和现代证明助手的重要基础。
主要观点：命题即类型，知道一个命题意味着拥有它的构造。