1 定义与特征
形式科学（Formal Sciences）是研究抽象符号系统、逻辑结构与形式化推理的学科分支，与依赖经验观察的自然科学和社会科学相区别。其核心在于通过公理、定义和推理规则，构建自洽的理论体系，并探讨其内部一致性、完备性与可计算性。包括数学、逻辑学、计算机科学、信息论、统计学等学科，强调演绎推理与形式证明，为其他科学提供方法论基础与分析工具。
1.1 学科边界
1.1.1 与经验科学的区别
形式科学与经验科学（如物理学、生物学）的根本区别在于其研究对象的性质与验证方式。经验科学依赖观察、实验和归纳来获取知识，其结论必须接受现实世界的检验；而形式科学则基于公理、定义和逻辑推理，其有效性完全取决于内部一致性而非与外部事实的对应。例如，数学定理不因实验结果的改变而失效，牛顿力学被相对论修正，但欧几里得几何并未因此“错误”——它只是在一个不同的公理体系中依然成立。
1.1.2 与形式逻辑的关系
形式逻辑是形式科学的基础工具，但不等同于形式科学本身。形式逻辑研究有效推理的形式结构，而形式科学则将这种形式化方法扩展至更广泛的领域。形式逻辑为数学证明、计算机程序验证、语言学分析等提供底层规则，因此常被视作形式科学的“语法”。同时，形式科学的发展也反过来推动了逻辑学理论的演进，如数理逻辑就是数学与逻辑学交叉的产物。
1.2 主要特征
1.2.1 抽象性
形式科学的研究对象是脱离具体物理实体的抽象概念。例如，数学中的数字“1”不是指任何一个具体的苹果或物体，而是表示单一性的抽象符号。这种抽象性使得形式科学的结论可以跨越不同领域应用——同样的代数方程可以描述物理运动、经济活动或信息传输。
1.2.2 演绎推理
形式科学依赖演绎推理而非归纳。其典型模式是：从一组给定的公理出发，通过严格的逻辑规则推导出结论。如果前提为真且推理规则正确，则结论必然为真。这与经验科学中基于有限观测的归纳概括形成鲜明对比——即便所有观察到的天鹅都是白的，归纳也不能保证“所有天鹅都是白的”永远成立。
1.2.3 公理化方法
公理化方法是形式科学的核心组织方式。其步骤包括：选取一组初始概念（不加定义的元概念）和一组公理（被认为不证自明的基本命题），然后在此基础上通过定义和定理推导构建整体理论。欧几里得的《几何原本》是这一方法的经典范例，后世数学与逻辑学的多数分支均沿袭此范式。
2 主要分支
2.1 数学
数学是形式科学中历史最悠久、体系最庞大的分支。它研究数量、结构、空间和变化等抽象概念。
2.1.1 基础数学
基础数学为整个数学体系提供底层逻辑和本体论基础。
2.1.1.1 集合论与数理逻辑
集合论是几乎所有现代数学的共同语言，将数学对象定义为集合并研究其性质。数理逻辑则用数学方法研究逻辑问题，包括命题逻辑、谓词逻辑等。两者共同确保了数学推理的严格性和一致性，但也揭示了某些内在局限（如哥德尔不完备定理）。
2.1.2 结构数学
结构数学研究不同形式的抽象结构及其相互关系。
2.1.2.1 代数、几何与拓扑
代数研究运算规则和代数结构（群、环、域等），几何研究形状、大小和空间性质，拓扑则关注在连续变形下保持不变的性质。这三者互为支撑：代数提供描述结构的语言，几何提供直观的模型，拓扑则揭示更深层的空间关系。
2.1.3 应用数学
应用数学将数学工具应用于解决现实问题，领域包括数值分析、微分方程、概率论、运筹学等。尽管其动机常来自实际需求，但结论仍以形式证明为基础，而非依赖实验验证。
2.2 逻辑学
逻辑学研究有效推理的形式和规律。
2.2.1 经典逻辑
经典逻辑包括命题逻辑和谓词逻辑，建立在排中律、不矛盾律和同一律等基本原则之上。它是现代形式科学中最基础的逻辑系统，大多数数学理论以经典逻辑为框架。
2.2.2 非经典逻辑
非经典逻辑尝试修正或扩展经典逻辑的某些假设。
2.2.2.1 模态逻辑与直觉主义逻辑
模态逻辑引入了“必然”、“可能”等模态算子，用于分析推理的模态性质。直觉主义逻辑则拒绝了排中律，认为一个命题只有被构造性证明时才是真的。这些变体在计算机科学（程序验证）和哲学（语言分析）中有重要应用。
2.3 计算机科学
计算机科学不仅是一门工程学科，也包含大量形式科学的内容。
2.3.1 理论计算机科学
理论计算机科学探讨计算的本质与边界。
2.3.1.1 可计算性理论
可计算性理论研究哪些问题可以被算法解决。图灵机模型和可判定性问题（如停机问题）是核心议题，揭示了计算能力的理论极限。
2.3.1.2 形式语言与自动机
形式语言研究符号串的集合及其生成规则，自动机理论则研究处理这些语言的抽象机器模型。两者是编译器设计、自然语言处理和人工智能的基础。
2.3.2 算法与复杂性
算法研究解决问题的步骤和方法，复杂性理论则分析解决问题所需的资源（时间、空间），界定问题的难易程度（P与NP问题等）。该方向在密码学、数据科学等领域具有实际意义。
2.4 统计学与概率论
统计学与概率论处理不确定性和随机现象的形式化描述。
2.4.1 概率公理体系
概率论以柯尔莫哥洛夫公理为基础，将概率定义为满足非负性、归一性和可列可加性的测度。这一形式化框架消除了古典概率定义中的模糊性，使概率论成为严格的数学分支。
2.4.2 统计推断
统计推断研究如何从样本数据推断总体性质。
2.4.2.1 假设检验与置信区间
假设检验通过比较观测数据与零假设的概率来做出判断，置信区间则在给定置信水平下估计参数范围。两者都基于概率论的形式化推导，为科学研究提供了量化标准。
2.5 信息论
信息论由克劳德·香农在20世纪中叶创立，研究信息的量化、存储和传输。
2.5.1 熵与信息度量
信息熵衡量一个随机变量的不确定性：不确定性越高，信息量越大。这一概念为通信系统、数据压缩和密码学提供了理论基础。
2.5.2 编码理论
编码理论研究如何将信息转换为有效且可靠的符号序列。包括信源编码（压缩）和信道编码（纠错），后者确保数据在噪声信道中的正确传输，如硬盘纠错码和微信二维码中的纠错机制。
3 研究方法
3.1 公理化方法
公理化方法是形式科学最基本的研究方法。研究者选择一组初始概念和公理，然后通过精确定义和逻辑推导建立整个理论。公理的选择通常追求简洁性、独立性和一致性，但有时也因启发式考虑（如欧几里得第五公设的修正产生了非欧几何）。
3.2 形式系统
形式系统是公理化方法的现代实现形式，是一个由符号、公式、公理和推理规则组成的严格框架。
3.2.1 语法与语义
语法定义了什么符号序列是系统内合法的公式（合式公式），语义则赋予这些公式以意义（真值或模型）。一个形式系统可以被视为一个纯语法游戏，但语义为其提供解释和应用依据。
3.2.2 一致性与完备性
一致性指系统中不存在推导出矛盾（即同时证明A和非A）的可能性。完备性则指所有语义上真实的公式都能在系统内被证明。希尔伯特曾期望算术系统同时满足一致性和完备性，但哥德尔的不完备定理打破了这一愿景。
3.3 模型论
模型论研究形式语言与数学结构之间的关系。一个模型就是使一组形式语句为真的具体数学结构。通过构造不同的模型，可以探索公理系统的语义多样性——例如，非欧几何就是欧几里得几何公理（除第五公设外）的不同模型。
3.4 证明论
证明论将数学证明本身作为形式研究对象。它关注证明的结构、长度和复杂度，并试图通过刻画证明的形式特征来论证整个系统的一致性。证明论与可计算性理论密切相关，例如自动定理证明系统就依赖证明论的算法化成果。
4 历史与发展
4.1 古代起源
4.1.1 欧几里得几何
古希腊数学家欧几里得在《几何原本》中系统化地应用了公理化方法：从五条公设和五条公理出发，推导出500余个定理。这部著作成为形式科学的第一个完整体系，其严谨性和方法论影响深远，直到19世纪才被非欧几何的诞生所挑战。
4.1.2 亚里士多德逻辑
亚里士多德创立了形式逻辑的早期体系，主要包括三段论理论。他研究了命题形式和推理的有效性，将逻辑从具体的论证内容中抽象出来。尽管与现代数理逻辑相比其表达力有限，但亚里士多德逻辑为后来所有的形式化研究提供了概念基础。
4.2 近代突破
4.2.1 希尔伯特纲领
20世纪初，大卫·希尔伯特提出将全部数学形式化在一个一致且完备的系统中的宏伟计划（希尔伯特纲领）。他希望通过有限的方法证明系统的一致性，从而一劳永逸地解决数学基础危机。这一纲领直接推动了数理逻辑和证明论的快速发展。
4.2.2 哥德尔不完备定理
1931年，库尔特·哥德尔证明，任何包含算术的一致形式系统必然是不完备的：系统中存在既不能被证明、也不能被否证的命题。同时，系统的一致性不能在自身内部被证明。这两个定理对希尔伯特纲领造成致命打击，但也开启了更深刻的形式科学研究——关于形式系统内在局限性的研究。
4.3 现代演变
4.3.1 计算机科学的形式化
20世纪中叶起，计算机科学成为形式科学最活跃的领域。丘奇的λ演算、图灵机模型、形式语言层级（乔姆斯基层级）等成果，将计算现象形式化，催生了人工智能、程序验证等子领域。形式方法（如模型检测和Hoare逻辑）被用于保证软件硬件的可靠性。
4.3.2 离散数学的兴起
传统数学以连续量（实数、函数）为核心，但计算机科学和其他离散系统（网络、组合优化）的需求催生了离散数学的独立成长。图论、组合数学、代数结构等分支不仅自身发展为成熟学科，也成为算法设计和密码学的理论基础。
5 与其他科学的关系
5.1 在自然科学中的应用
5.1.1 物理学中的数学模型
物理学几乎全盘依赖数学模型：牛顿力学用微积分描述运动，量子力学用希尔伯特空间和算子代数表示状态，广义相对论使用黎曼几何。这些模型不仅用于描述现有现象，还通过纯数学演绎来预测未知现象（如反物质和黑洞的数学预测）。
5.2 在社会科学中的应用
5.2.1 博弈论与经济学
博弈论作为数学的一个分支，通过形式化模型分析策略互动和利益分配。其在经济学中的应用尤为突出，从纳什均衡到拍卖理论，形式科学的工具被用来模拟市场行为、设计机制并解释社会现象——尽管后者与理想化模型之间常存在显著偏差。
5.3 在工程与技术中的作用
5.3.1 软件工程的规范方法
在关键系统中（航天、医疗、金融），形式化规范方法被用来避免软件错误。通过将系统需求转化为逻辑公式（如Z语言或VDM规格说明），开发者可以在编码前通过形式验证发现设计缺陷，从而提升软件的可靠性。
6 批判与局限
6.1 形式主义的困境
形式主义的极端立场认为数学只是一套符号游戏，无需与任何现实对应。这种观点面临两个问题：一是难以解释数学在经验科学中惊人的有效性；二是若完全脱离意义，则数学研究可能沦为无目的的机械操作，丧失其启发价值。
6.2 可计算性的边界
可计算性理论揭示了计算的固有极限：停机问题不可判定，许多自然问题（如判定丢番图方程是否有整数解）在算法上是不可解的。这意味着存在大量我们无法通过形式化方法自动求解的问题，只能退而求其次寻求近似或启发式方案。
6.3 与现实世界的脱节争议
过度形式化可能导致理论脱离实际。例如，经济学中完全理性的博弈论模型经常在现实市场中被打破；物理学的数学优雅性可能与实验数据不完全匹配。批评者认为形式科学应警惕“高雅却无用”的倾向，保持与世界对话的开放性。不过，支持者认为，理论脱节本身就是推进知识边界的代价——许多曾被视作“无用”的纯数学，最终意外地找到了应用（如数论在加密技术中的应用）。