在逻辑与数学中，形式系统（Formal system）是由形式语言与推理规则组成，指根据推理规则从公理推出定理的抽象结构。1921年，希尔伯特提出用形式系统作为数学知识的基础。

命题逻辑是最简单的形式系统。

一，背景介绍

推理和蕴含（Inference and entailment）

逻辑基础上的蕴含性（entailment）是区分形式系统与其他抽象模型系统的因素。

形式语言

形式语言通常有两个方面：

语法：指语言中的话语是什么。

语义：指语言中的话语是什么意思。

演绎系统

演绎系统，由公理（或公理模式）和推理规则组成，可用于推导系统的定理。

这种演绎系统在系统中表达的公式中保留了演绎的品质，通常指公式的真值。

为了维持其演绎的完整性，一个演绎工具必须是可定义的，而不需要参考语言的任何预期解释。其目的是确保推导的每一行仅仅是其前面几行的句法结果。对语言的任何解释都不应该涉及到系统的演绎性质。

逻辑系统

逻辑系统是演绎系统加上公理。根据模型理论，一个逻辑系统可以被赋予一个或多个语义或解释，这些语义或解释描述一个形式良好的公式是否被一个给定的结构所满足。一个满足形式系统所有公理的结构被称为逻辑系统的一个模型。如果可以从公理推断出的每个形式良好的公式都被逻辑系统的每个模型所满足，那么这个逻辑系统就是健全的（sound）。反过来说，如果逻辑系统的每个模型所满足的每个形式良好的公式都能从公理中推断出来，那么这个逻辑系统就是（语义上）完备的（complete）。

证明系统

形式证明是合式公式（简称wff）的序列。为了使一个wff有资格成为证明的一部分，它可能是一个公理，或者是对证明序列中的前一个wff应用推理规则的产物。序列中的最后一个wff被认为是一个定理。

大卫-希尔伯特创立了元数学，作为讨论形式系统的学科。人们用来讨论形式系统的任何语言被称为元语言。元语言可能是一种自然语言，也可能是部分形式化的语言本身，但它通常不如所研究的形式系统的形式语言部分完全形式化，后者则被称为对象语言，即有关讨论的对象。

一旦给出一个形式系统，人们就可以定义在形式系统内可以被证明的定理集合。这个集合由所有存在证明的wffs组成。因此，所有公理都被视为定理。与wffs的语法不同，不能保证有一个判定程序来判定一个给定的wffs是否是一个定理。

二，命题逻辑（命题演算）

在逻辑和数学里，命题演算是一个形式系统，有着可以由以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。

命题演算的语言包括：

（1）一套原始符号，被称之为“原子公式”或“命题变量”；

（2）一套运算符号，被称之为“逻辑运算符”。一个“合式公式”是任一原子公式，或任一以运算符号依文法规则由原子公式创建起的公式。

形式描述

命题演算是一个形式系统 L = {A, Ω, Z, I}：

A集合是由“命题变量”所组成的有限集合，“命题变量”是形式语言L最基本的元素，亦被称之为“原子公式”。在接着的例子中，A内的元素一般写作字母p, q, r之类的形式。

Ω是“逻辑运算符”所组成的有限集合。

依据所使用的精确形式文法，可能需要以括号作语法上的辅助，用来完成公式的构造。

L的语言，亦称之为“公式”或“合式公式”的集合，可由如下规则被归纳或递归地定义。

Z集合，指“变换规则”（当作为逻辑解释时则称为“推理规则”）所构成的有限集合。

I是“起始点”（当得到逻辑解释时则称为“公理”）所构成的有限集合。

例子

1. 简单的公理系统

设 L1 = {A, Ω, Z, I}：

A = {p,q,r,s,t,u, …}

Ω = {¬，→}

Z：

p → (q →p)

(p → (q →r)) → ((p → q) →(p → r))

(¬p → ¬q) → (p → q)

肯定前件：p和(p → q)导出q

I：各个公理都是由下列的公理模式作代换所得。

2. 自然演绎系统

L2 = {A, Ω, Z, I}：

A = {p,q,r,s,t,u}

Ω = {¬, ∧, ∨, →, ↔}

Z：10个推理规则

I：起始点的集合是空的

参考文献：

https://zh.wikipedia.org/zh-sg/%E5%91%BD%E9%A2%98%E9%80%BB%E8%BE%91

https://en.wikipedia.org/wiki/Formal_system