形式证明 是 指对具体推理的形式正确性进行考察，即把具体推理的前提和结论符号化为逻辑公式，运用一定的推理规则，有步骤地从表示前提的公式推出表示结论的公式 。
为了保证形式证明能严谨有序地进行，避免错误和随意性，现代逻辑提出了关于形式证明的两套规则： 建立证明的规则和推理规则 。
一、建立证明的规则
人建立证明的规则 是 关于如何组织形式证明的前提、如何运用推理规则、怎样才可以确认形式证明建立起来的一些规定 。
一般而言，建立一个推理的形式证明可采用如下步骤：
第一步， 把前提的符号表达式即公式按行列出，并在公式左边标明相应的行数；在最后一行前提公式的右边列出推理结论的符号表达式即结*公论**式，用一斜线将其和前提公式分开 。
第二步， 考虑运用某个推理规则于一定的前提公式，将所得结论写在下面一行，并在其右边注明得到的根据 。
第三步， 再考虑运用某个推理规则于已经写出的公式（不包括原推理结*公论**式），并写出得到的结论，在结论右边注明得到的根据 。
第四步， 依此类推，直到得到原推理结*公论**式 。如果 最后得到了原推理结*公论**式 ，则 形式证明就被认为建立起来，原推理的有效性得到证明 。
二、推理规则
在形式证明中，常用的是以下一些推理规则。这些规则大多 对应于一定的重言式 ，体现了人们在思维中经常使用的推理形式。
1.假设引入规则：
在推导过程中，可以根据需要随时引入一个假设 。
2.蕴涵消除规则(分离规则），简记为→_：
从 A→B和A，可以推出B 。
3.合取引入规则，简记为Λ₊：
从A和B，可以推出AΛB 。
4.合取消除规则，简记为A_：
从AΛB，可以推出A。
从AΛB，可以推出B 。
5.析取引人规则，简记为V₊：
从A，可以推出AVB。
从B,可以推出AVB 。
6.析取消除规则，简记为V_：
从AVB和┓A,可以推出B。
从AVB和┓B,可以推出A 。
7.等值引人规则，简记为↔₊：
从A→B和B→A，可以推出A↔B 。
8.等值消除规则，简记为↔_：
从A↔B，可以推出A→B。
从A↔B，可以推出B→A 。
9.否定引入规则（归谬律），简记为┓₊：
在给定前提下，如果引入假设A，由此推出B和-B，那么，由原来的前提可以推出A 。
10.否定消除规则(反证律)，简记为┓_：
在给定前提下，如果引入假设┓A，由此推出B和┓B，那么，由原来的前提可以推出A 。
11.假言易位规则：
从A→B，可以推出┓B→┓A 。
12.否定后件规则：
从A→B和┓B，可以推出┓A 。
除了上面所列规则外， 还允许在需要时将经典命题逻辑中其他的重言式当作推理规则使用 。例如：
13.双重否定消除规则，简记为 ┓┓_：
从┓┓A，可以推出A 。
14.假言三段论规则：
从B→C和A→B，可以推出A→C 。
15.二难推理规则：
从A→B,C→D和AVC,可以推出BVD 。
此外，为了使形式证明简便易行，还需要增加以下两条特殊规则：
16.等值置换规则：
在推导过程中，可以把互相等值的公式彼此替换 。
17.蕴涵引入规则，简记为→₊：
如果在前提公式的集合基础上，再加上一个假设A，进而可以推出B，那么，从这个前提公式的集合可以推出A→B 。
例5-1 分析以下推理是否有效：
如果张明去北京，那么李卫和赵强也去北京。
如果李卫或者王华去北京，那么孙明也去北京。
张明去北京。
所以，孙明和赵强去北京。
该推理可以符号化为：解
p→(qΛr)
(qVs)→t
P
∴tΛr
(p表示“张明去北京”，q表示“李卫去北京”，r表示“赵强去北京”，s表示“王华去北京”，t表示“孙明去北京”。)
对这个推理形式，可以构造如下形式证明：
1 p→(qAr)
2 (qVs)→t
3 p / :tAr
4 q→r 1，3→_
5 q 4 Λ_
6 r 4 Λ_
7 qVs 5 V₊
8 t 2，7 →_
9 tΛr 8，6 Λ₊
上述证明的最后一行即原推理的结*公论**式，所以，原推理有效。
例5-2 分析以下推理形式是否有效：
p→(q→r)Λ(┓q→s)
ㄱrΛㄱS
∴ㄱp
解：对这一推理形式，可以构造如下形式证明：
1 p→(q→r)Λ(┓q→s)
2 ㄱrΛㄱS /∴ㄱp
3 p 假设
4 (q→r)Λ(┓q→s) 1，3 →_
5 q→r 4 Λ_
6 ㄱr 2 Λ_
7 ㄱq 5，6 否定后件规则
8 ㄱq→s 4 Λ_
9 ㄱs 2 Λ_
10 ┓┓q 8，9 否定后件规则
11 ㄱp 7，10 ┓₊
上述证明的最后一行即原推理形式的结论，所以，原推理形式有效。
例5-3 分析以下推理形式是否有效：
p→qΛq
∴ㄱp
解：对于这一推理形式，可以构造如下形式证明：
1 p→qΛ┓q /∴ㄱp
2 p 假设
3 qΛㄱq 1,2 →_
4 q 3 Λ_
5 ┓q 3 Λ_
6 ㄱp 4，5 ┓₊
上述证明的最后一行即原推理形式的结论，所以，原推理形式有效。
例5-4 分析以下推理是否有效：
张华没有上课或者因为有病，或者因为有急事。
如果张华有急事，他就会打电话来。
张华没有打电话来。
所以，张华没有上课是因为有病。
解该推理可符号化为：
pVq
q→r
ㄱr
∴p
(p表示“张华没有上课是因为有病”，q表示“张华没有上课是因为有急事”，r表示“张华打电话来”。)
对于这一推理形式，可以构造如下形式证明：
1 pVq
2 q→r
3 ㄱr/ ∴p
4 ㄱq 2，3 否定后件规则
5 p 1，4 V_
上述证明的最后一行即原推理的结*公论**式，所以，原推理有效。