一阶逻辑 是使用于数学 、哲学 、语言学 及计算机科学 中的一种形式系统 ,也可以称为:一阶断言演算 、低端断言演算 、量化理论 或谓词逻辑 。一阶逻辑和命题逻辑 的不同之处在于,一阶逻辑包含量词 。
高阶逻辑 和一阶逻辑不同之处在于,高阶逻辑的断言符号可以有断言符号或函数符号当做引数 ,且容许断言量词或函数量词[ 1] 。在一阶逻辑的语义 中,断言被解释为关系 。而高阶逻辑的语义里,断言则会被解释为集合的集合。
在通常的语义下,一阶逻辑是可靠 (所有可证的叙述皆为真)且完备 (所有为真的叙述皆可证)的。虽然一阶逻辑的逻辑归结只是半可判定性 的,但还是有许多用于一阶逻辑上的自动定理证明 。一阶逻辑也符合一些使其能通过证明论 分析的元逻辑 定理,如勒文海姆–斯科伦定理 及紧致性定理 。
一阶逻辑是数学基础 中很重要的一部分。许多常见的公理系统,如一阶皮亚诺公理 、冯诺依曼-博内斯-哥德尔集合论 和策梅洛-弗兰克尔集合论 都是一阶理论。然而一阶逻辑不能控制其无穷模型的基数 大小,因根据勒文海姆–斯科伦定理和康托尔定理 ,可以构造出一种“病态”集合论模型,使整个模型可数,但模型内却会觉得自己有“不可数集”。类似地,可以证明实数系的普通一阶理论既有可数模型又有不可数模型。这类的悖论被称为斯科伦悖论 。但一阶的直觉主义逻辑 里,勒文海姆–斯科伦定理不可证明[ 2] ,故不会有以上之现象。
命题逻辑顾名思义,会将“苏格拉底是哲学家”、“帕雷托是哲学家”之类直观上有真有假 的叙述简记为
p
{\displaystyle p}
及
q
{\displaystyle q}
(也就是有真有假的命题 ),然后讨论
¬
p
{\displaystyle \neg p}
(非p)、
p
⇒
q
{\displaystyle p\Rightarrow q}
(若p则q)、
p
∧
q
{\displaystyle p\wedge q}
(p且q)与
p
∨
q
{\displaystyle p\vee q}
(p或q)之间的推理关系。
但一阶逻辑尝试从一些比较基础的词汇去建构“句子”,比如说,可用符号
Phil
(
x
)
{\displaystyle {\text{Phil}}(x)}
代表 “ x 是哲学家”,也就是赋予断言符号 “
Phil
(
x
)
{\displaystyle {\text{Phil}}(x)}
”语义的解释。 这个解释默认一个“所有人类的群体”(也就是下面标准语义 一节会说到的论域 ),并将变量
x
{\displaystyle x}
对应为自群体中取出来的某人。
以此类推,断言符号可以包含一个以上的变量。例如:可以将
Cp
(
x
,
y
)
{\displaystyle {\text{Cp}}(x,\,y)}
解释为“ x 与 y 是夫妻”。
一阶逻辑类似于命题逻辑,可以将断言符号与
¬
{\displaystyle \neg }
(非)、
⇒
{\displaystyle \Rightarrow }
(则)、
∧
{\displaystyle \wedge }
(且)和
∨
{\displaystyle \vee }
(或)组成更复杂的叙述,例如:把断言符号
Schol
(
x
)
{\displaystyle {\text{Schol}}(x)}
解释成“
x
{\displaystyle x}
是学者”,那“若 x 为哲学家,则 x 为学者”可表示为:
Phil
(
x
)
⇒
Schol
(
x
)
{\displaystyle {\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)\,}
但相较之下,一阶逻辑又加入了描述“所有”与“存在”的量词,比如说“对所有 x ,若 x 为哲学家,则 x 为学者”可记为:
∀
x
[
Phil
(
x
)
⇒
Schol
(
x
)
]
{\displaystyle \forall x[{\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)]}
也就是自左方开始阅读,将
∀
x
{\displaystyle \forall x}
解释成“对所有 x 有…”。
∀
{\displaystyle \forall }
这个符号被称为全称量词 。
而对于“有 x 是哲学家”这一叙述,一阶逻辑则引入另一种量词:
∃
x
[
Phil
(
x
)
]
{\displaystyle \exists x[{\text{Phil}}(x)]}
也就是自左方开始阅读,将
∃
x
{\displaystyle \exists x}
解释成“存在
x
{\displaystyle x}
使…”。
∃
{\displaystyle \exists }
这个符号被称为存在量词 。
顺带一提“并非所有 x 不是哲学家”等价于“有 x 是哲学家”;且“不存在 x 不是学者”也等价于“所有的 x 是学者”。所以可以用“否定”和“全称量词”来组合出“存在量词”。换句话说,可作以下的符号定义(
A
{\displaystyle {\mathcal {A}}}
代表一段“叙述”):
∃
x
A
:=
¬
[
∀
x
(
¬
A
)
]
{\displaystyle \exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]}
一阶逻辑也考虑到“相等”这个概念在叙述中的重要性,例如想表达“若所有
x
{\displaystyle x}
是哲学家,那
x
{\displaystyle x}
的长子也会是哲学家”,可先把
Son
(
x
)
{\displaystyle {\text{Son}}(x)}
解释为 “ x 的长子”,那么这段叙述可记为:
∀
x
Phil
(
x
)
⇒
Phil
[
Son
(
x
)
]
{\displaystyle \forall x{\text{Phil}}(x)\Rightarrow {\text{Phil}}[{\text{Son}}(x)]}
换句话说,
Son
(
x
)
{\displaystyle {\text{Son}}(x)}
被解释成“与
x
{\displaystyle x}
有特定且唯一对应关系”的某对象(被称为函数符号 )。换句话话说,只要“
x
{\displaystyle x}
就是
y
{\displaystyle y}
”,那“
x
{\displaystyle x}
的长子也会是
y
{\displaystyle y}
的长子”。换句话说:
(
x
=
y
)
⇒
[
Son
(
x
)
=
Son
(
y
)
]
{\displaystyle (x=y)\Rightarrow [{\text{Son}}(x)={\text{Son}}(y)]}
这些性质被一阶逻辑视为“理所当然”。
类似地,叙述中也有一些“不变的实体”,如苏格拉底 ,表示这些“实体”的符号被称为常数符号。例如将
s
{\displaystyle s}
解释为苏格拉底 ,那“苏格拉底 为哲学家”就可以写成:
Phil
(
s
)
{\displaystyle {\text{Phil}}(s)}
所谓的“不变”隐含的代表:
“苏格拉底就是苏格拉底”
“对所有x,对所有y,如果x就是苏格拉底,且y就是苏格拉底,那x就是y”
换句话说
(
s
=
s
)
{\displaystyle (s=s)}
∀
x
∀
y
{
[
(
x
=
s
)
∧
(
y
=
s
)
]
⇒
(
x
=
y
)
}
{\displaystyle \forall x\forall y\{[(x=s)\wedge (y=s)]\Rightarrow (x=y)\}}
这两个性质也被一阶逻辑视为“理所当然”。
一阶逻辑的形式理论 可分成几个部分:
语法 :决定哪些符号组合是合式公式 。(直观上的“文法无误的叙述”)
推理规则:由合式公式符号组合出新合式公式的规则(直观上的“推理”)
公理:一套合式公式(直观上的基本假设)
一套理论能容许多少符号,取决于人类能运用物理定律 来塑造多少符号,但目前无法确知宇宙是不是有限,或是以可无限制地分割。虽然所有的公理化集合论 都以量词的形式隐晦的承认跟自然数 一样多的无穷(如ZF集合论的无穷公理 ),甚至以这样的可数无穷为基础,去建构出不可数 的实数,但将抽象的理论对应到现实时,还是需要回答物理上有没有可数或不可数的无穷。所以谨慎起见,如果没有特别申明的话,以下各种类符号的数目上限都是有限的。
一阶逻辑通常拥有以下的符号:
量化符号
∀
{\displaystyle \forall }
及
∃
{\displaystyle \exists }
某些作者[ 3] 会把
∃
{\displaystyle \exists }
符号定义为
∃
x
A
:=
¬
[
∀
x
(
¬
A
)
]
{\displaystyle \exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]}
,如此便只需要
∀
{\displaystyle \forall }
做为基础符号。
逻辑联结词 :以下为可能的表示符号(关于波兰表示法下的逻辑连接词,请参见逻辑运算的波兰记法 ):
否定 :
¬
{\displaystyle \neg }
或
∼
{\displaystyle \sim }
或-
条件 :
⇒
{\displaystyle \Rightarrow }
或
→
{\displaystyle \rightarrow }
或
⊃
{\displaystyle \supset }
且 :
∧
{\displaystyle \land }
或
&
{\displaystyle \&}
或 :
∨
{\displaystyle \lor }
或 ||
双条件 :
⇔
{\displaystyle \Leftrightarrow }
或
↔
{\displaystyle \leftrightarrow }
某些作者[ 4] 会作如下的符号定义:
A
∧
B
:=
¬
(
A
⇒
(
¬
B
)
)
,
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}:=\neg ({\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})),}
A
∨
B
:=
(
¬
A
)
⇒
B
,
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}}:=(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}},}
A
⇔
B
:=
(
A
⇒
B
)
∧
(
B
⇒
A
)
,
{\displaystyle {\mathcal {A}}\Leftrightarrow {\mathcal {B}}:=({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}}),}
如此一来只需要否定 和条件 做为基础符号。
标点符号:括号、逗号及其他,依作者的喜好有所不同。
为了更有效的将括号做配对,通常还会采用大括号{ } 跟中括号[ ] 。
至多跟自然数 一样多的变量 ,通常标记为英文字母末端的小写字母x 、y 、z 、…,也常会使用下标(或上标、上下标兼有)来区别不同的变量:x 0 、x 1 、x 2 、…(特别注意c有时候会被当成常数符号而引起混淆)。
等式符号:
=
{\displaystyle =}
有作者会因为语义上对“相等”的不同解释,而将等式符号视为双元断言符号、甚至是某种合式公式 的简写。
符号相等:
≍
{\displaystyle \asymp }
某些作者[ 5] 会额外采用这个符号来表示符号识别上的等同 以便与等式符号作区别。
并非所有的符号都不可或缺的,像谢费尔竖线 “
|
{\displaystyle |}
”(或异或 )可以用来定义量词以外的所有逻辑符号,换句话说:
符号定义 —
(
¬
A
)
:=
(
A
|
A
)
{\displaystyle (\neg {\mathcal {A}}):=({\mathcal {A}}|{\mathcal {A}})}
(
A
⇒
B
)
:=
A
|
(
B
|
B
)
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}}):={\mathcal {A}}|({\mathcal {B}}|{\mathcal {B}})}
(
A
∧
B
)
:=
[
(
A
|
B
)
|
(
A
|
B
)
]
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {B}})|({\mathcal {A}}|{\mathcal {B}})\,]}
(
A
∨
B
)
:=
[
(
A
|
A
)
|
(
B
|
B
)
]
{\displaystyle ({\mathcal {A}}\vee {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {A}})|({\mathcal {B}}|{\mathcal {B}})\,]}
另外,一些作者不区分语义解释 和形式理论 ,所以会将表示真值的符号纳入形式理论里,也就是说,用 T 、Vpq 或
⊤
{\displaystyle \top }
来表示“真”,并用 F 、 Opq 或
⊥
{\displaystyle \bot }
来表示“假”。
“他们两人是夫妻”,是一个关于两个“对象”的断言,而“他是人”、“三点共线”则表明断言容许一个或者多个对象。所以对于自然数
n
{\displaystyle n}
、
j
{\displaystyle j}
约定:
A
j
n
(
x
1
,
x
2
,
.
.
.
,
x
n
)
{\displaystyle A_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})}
为一阶逻辑的合法词汇。它在直观上表示一个有
n
{\displaystyle n}
个“对象”的断言,称为
n
{\displaystyle n}
元断言符号 。下标的自然数
j
{\displaystyle j}
只是拿来和其他同为
n
{\displaystyle n}
元的断言符号作区别。
实用上只要有申明,不至于和其他词汇引起混淆的话,可以用任意的形式简写一个断言符号。如:公理化集合论 里的双元断言符号
A
1
2
(
x
,
y
)
{\displaystyle A_{1}^{2}(x,\,y)}
也可以表示为
x
∈
y
{\displaystyle x\in y}
。
“物体的颜色”、“夫妻的长子”这种断言说明了一组对象所唯一 对应的对象。但不同的夫妻有不同的长子;不同的物体有不同的颜色。据此,形式上对于自然数
n
{\displaystyle n}
、
j
{\displaystyle j}
约定:
f
j
n
(
x
1
,
x
2
,
.
.
.
,
x
n
)
{\displaystyle f_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})}
为一阶逻辑的合法词汇,直观上表示
n
{\displaystyle n}
个“对象”所对应到的东西,称它为
n
{\displaystyle n}
元函数符号 。需要特别注意 ,这种“唯一对应”的直观想法,必须配上关于“等式”的性质(详见下面的等式定理 章节),才能在形式理论中被实现。
与断言符号一样,只要不引起混淆,就可以用任何的形式简写函数符号。如:公理化集合论 里的
x
∪
y
{\displaystyle x\cup y}
是依据并集公理 而定义的新函数符号(请参见下面函数符号与唯一性 章节),也可以冗长的表记为
f
j
2
(
x
,
y
)
{\displaystyle f_{j}^{2}(x,\,y)}
。
“刻度0”、“原点”、“苏格拉底 ”是直观上"唯一不变"的对象。据此,对自然数
j
{\displaystyle j}
约定
c
j
{\displaystyle c_{j}}
为一阶逻辑的合法词汇,直观上表示一个“唯一不变”的对象,称为常数符号 。同样的。“常数的不变性”需配上等式的性质(详见下面等式定理 )才能被实现。
为了不和变量的表记混淆,常数符号一样可以用任何的形式简写,如公理化集合论 里的
∅
{\displaystyle \varnothing }
是根据空集公理 和函数符号与唯一性 ,而定义的新常数符号。亦可冗长的表示为
c
j
{\displaystyle c_{j}}
。
和自然语言(如英语 )不同,一阶逻辑的语言以明确的递归 定义判断一个给定的词汇是否合法。大致上来说,一阶逻辑以“项”代表讨论的对象,而对“项”的断言组成了最基本的原子(合式)公式 ;而原子公式和逻辑符号组成了更复杂的合式公式 (也就是“叙述”)。
“那对夫妻的长子的职业”、“
(
x
+
y
)
×
z
{\displaystyle (x+y)\times z}
”、“
x
∪
∅
{\displaystyle x\cup \varnothing }
”代表变量可以与函数符号组成更一般的对象。据此形式,递归地规定一类合法词汇——项 为:
递归定义 —
变量 和常数 是项。
若
T
1
,
.
.
.
.
,
T
n
{\displaystyle T_{1},\,....,\,T_{n}}
全都是项,那么
f
j
n
(
T
1
,
.
.
.
.
,
T
n
)
{\displaystyle f_{j}^{n}(T_{1},\,....,\,T_{n})}
也是项。
项只能通过以上两点,于有限步骤内置构出来。
习惯上以大写的西方字母(如英文 字母、希伯来 字母、希腊字母 )代表项,如果变量不得不采用大写字母,而可能跟项引起混淆的话,需额外规定分辨的办法。
为了比较简洁地规定什么是合式公式 ,先规定原子公式 为:(若
T
1
,
.
.
.
.
,
T
n
{\displaystyle T_{1},\,....,\,T_{n}}
是项)
A
j
n
(
T
1
,
.
.
.
.
,
T
n
)
{\displaystyle A_{j}^{n}(T_{1},\,....,\,T_{n})}
这样的形式。
一阶逻辑的合式公式 (简称公式或
w
f
{\displaystyle wf}
)以下面的规则递归地定义:
另外成对的中括弧跟大括弧,符号识别上视为成对的小括弧,而草书的大写西方字母 为公式的代号。
举例来说,
{
(
∀
y
)
A
1
2
[
x
,
f
1
1
(
y
)
]
}
{\displaystyle \{(\forall y)A_{1}^{2}[x,\,f_{1}^{1}(y)]\}}
是公式而
∀
x
x
⇒
{\displaystyle \forall x\,x\Rightarrow }
则不是公式。
而接下来只要对任意公式
A
{\displaystyle {\mathcal {A}}}
、
B
{\displaystyle {\mathcal {B}}}
与变量
x
{\displaystyle x}
,做以下符号定义
符号定义 —
(
A
∧
B
)
:=
{
¬
[
A
⇒
(
¬
B
)
]
}
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}}):=\{\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]\}}
(
A
∨
B
)
:=
[
(
¬
A
)
⇒
B
]
{\displaystyle ({\mathcal {A}}\vee {\mathcal {B}}):=[(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]}
(
A
⇔
B
)
:=
[
(
A
⇒
B
)
∧
(
B
⇒
A
)
]
{\displaystyle ({\mathcal {A}}\Leftrightarrow {\mathcal {B}}):=[({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}})]}
(
∃
x
A
)
:=
{
¬
[
∀
x
(
¬
A
)
]
}
{\displaystyle (\exists x{\mathcal {A}}):=\{\neg [\forall x(\neg {\mathcal {A}})]\}}
(同样美观起见
(
∃
x
)
A
:=
∃
x
A
{\displaystyle (\exists x){\mathcal {A}}:=\exists x{\mathcal {A}}}
)
这样所有的逻辑连接词与量词就纳入了合式公式的规范。
所谓的施用 /作用 ,是以下公式形式的口语说法:(其中
A
{\displaystyle {\mathcal {A}}}
与
B
{\displaystyle {\mathcal {B}}}
都是公式)
(
¬
A
)
{\displaystyle (\neg {\mathcal {A}})}
称为
¬
{\displaystyle \neg }
施用于
A
{\displaystyle {\mathcal {A}}}
上。
(
A
⇒
B
)
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
称为
⇒
{\displaystyle \Rightarrow }
施用于
A
{\displaystyle {\mathcal {A}}}
和
B
{\displaystyle {\mathcal {B}}}
上。
(
A
∧
B
)
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}})}
称为
∧
{\displaystyle \wedge }
施用于
A
{\displaystyle {\mathcal {A}}}
和
B
{\displaystyle {\mathcal {B}}}
上。
(
A
∨
B
)
{\displaystyle ({\mathcal {A}}\vee {\mathcal {B}})}
称为
∨
{\displaystyle \vee }
施用于
A
{\displaystyle {\mathcal {A}}}
和
B
{\displaystyle {\mathcal {B}}}
上。
(
A
⇔
B
)
{\displaystyle ({\mathcal {A}}\Leftrightarrow {\mathcal {B}})}
称为
⇔
{\displaystyle \Leftrightarrow }
施用于
A
{\displaystyle {\mathcal {A}}}
和
B
{\displaystyle {\mathcal {B}}}
上。
(
∀
x
A
)
{\displaystyle (\forall x{\mathcal {A}})}
称为
∀
x
{\displaystyle \forall x}
施用于
A
{\displaystyle {\mathcal {A}}}
上。
(
∃
x
A
)
{\displaystyle (\exists x{\mathcal {A}})}
称为
∃
x
{\displaystyle \exists x}
施用于
A
{\displaystyle {\mathcal {A}}}
上。
就类似于运算符作用在它们身上。
量词所施用的公式被称为量词的范围 (scope)。同一个变量在公式一般来说不只出现一次,若变量
x
{\displaystyle x}
出现在
∀
x
{\displaystyle \forall x}
的范围内,称这样出现的
x
{\displaystyle x}
为不自由 /被约束的
x
{\displaystyle x}
(not free/bounded);反过来说,不出现在
∀
x
{\displaystyle \forall x}
的范围内的某个
x
{\displaystyle x}
被称为自由的
x
{\displaystyle x}
。
例如,对于公式:
{
(
∀
x
)
[
A
1
1
(
x
)
⇒
A
2
1
(
y
)
]
}
{\displaystyle \{(\forall x)[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]\}}
[
A
1
1
(
x
)
⇒
A
2
1
(
y
)
]
{\displaystyle [A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]}
就是量词
∀
x
{\displaystyle \forall x}
的范围;而
A
1
1
(
x
)
{\displaystyle A_{1}^{1}(x)}
里的
x
{\displaystyle x}
就是不自由的;反之
A
2
1
(
y
)
{\displaystyle A_{2}^{1}(y)}
里的
y
{\displaystyle y}
就是自由的。
说
x
{\displaystyle x}
于公式
A
{\displaystyle {\mathcal {A}}}
完全自由,意为于
A
{\displaystyle {\mathcal {A}}}
出现的
x
{\displaystyle x}
都是自由的;反之,说
x
{\displaystyle x}
于公式
A
{\displaystyle {\mathcal {A}}}
完全不自由/完全被约束,意为
A
{\displaystyle {\mathcal {A}}}
内根本没有
x
{\displaystyle x}
,或是
A
{\displaystyle {\mathcal {A}}}
内没有自由的
x
{\displaystyle x}
。若
A
{\displaystyle {\mathcal {A}}}
内所有的变量都完全不自由,
A
{\displaystyle {\mathcal {A}}}
特称为封闭公式/句子 (closed formula/sentence)。
括弧是为了保证语义解释符合预期,但太多的括弧书写不易,为此规定以下的“重构法”(反过来就是“简写法”),从表面上不合法的一串符号找出作者原来想表达的公式:
若整串符号的括弧不成对,直接视为无法重构 。
以
¬
,
∧
,
∨
,
∀
,
∃
,
⇒
,
⇔
{\displaystyle \lnot ,\,\land ,\,\lor ,\,\forall ,\,\exists ,\,\Rightarrow ,\,\Leftrightarrow }
(左至右)的施用顺序重构括弧。
相邻的逻辑连接词或量词无法决定施用顺序的话,以右边为先。
重构施用的顺序,以被成对括弧包住的部分为优先施用,其次才是落单的断言符号。
举例来说
¬
[
∀
x
A
1
1
(
x
)
]
⇒
∃
x
¬
A
2
1
(
x
)
{\displaystyle \lnot [\forall xA_{1}^{1}(x)]\Rightarrow \exists x\lnot A_{2}^{1}(x)}
的重构过程如下
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
∃
x
[
¬
A
2
1
(
x
)
]
{\displaystyle \{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \exists x[\lnot A_{2}^{1}(x)]}
(优先施用
¬
{\displaystyle \lnot }
)
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
{
∃
x
[
¬
A
2
1
(
x
)
]
}
{\displaystyle \{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}}
(施用
∃
{\displaystyle \exists }
)
{
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
{
∃
x
[
¬
A
2
1
(
x
)
]
}
}
{\displaystyle \{\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}\}}
(最后施用
⇒
{\displaystyle \Rightarrow }
)
可以被重构为公式的一串符号则宽松的认定为“合式公式”。(最明显的例子就是合式公式最外层的括弧可以省略)
波兰表示法 将逻辑连接词前置于被施用的公式 而非传统的中间。如果沿用以上的"施用顺序",这个表示法允许舍弃所有括弧。如公式
∀
x
∀
y
{
A
1
1
[
f
1
1
(
x
)
]
⇒
¬
{
A
1
1
(
x
)
⇒
A
1
3
[
f
1
1
(
y
)
,
x
,
z
]
}
}
{\displaystyle \forall x\forall y\{A_{1}^{1}[f_{1}^{1}(x)]\Rightarrow \neg \{A_{1}^{1}(x)\Rightarrow A_{1}^{3}[f_{1}^{1}(y),x,z]\}\}}
转成波兰表示法的过程如下
∀
x
∀
y
⇒
A
1
1
f
1
1
x
¬
⇒
A
1
1
x
A
1
3
f
1
1
y
x
z
{\displaystyle \forall x\forall y\Rightarrow A_{1}^{1}f_{1}^{1}x\neg \Rightarrow A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz}
(转成波兰表示法的顺序)
Π
x
Π
y
C
A
1
1
f
1
1
x
N
C
A
1
1
x
A
1
3
f
1
1
y
x
z
{\displaystyle \Pi x\Pi y{\text{C}}A_{1}^{1}f_{1}^{1}x{\text{N}}{\text{C}}A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz}
(逻辑链接词的符号变换)
一阶逻辑通常只有以下的推理规则(因为将普遍化 视为推理规则会有不直观的限制)
直观意义非常明显,就是p =>q 且p 可以推出q 。
在只以谢费尔竖线 “
|
{\displaystyle |}
”为基础逻辑连接词的公理系统 里,MP律 会被改写成
它们实际上是公理模式 ,代表着“跟自然数一样多”条的公理。
在有(A1)与(A2)的前提下,(A3)等价于以下的公理模式:(证明请参见下面否定 一节。)
(T1) —
[
(
¬
B
)
⇒
(
¬
C
)
]
⇒
(
B
⇒
C
)
{\displaystyle [\,(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})\,]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})}
另外,在只以谢费尔竖线 “
|
{\displaystyle |}
”为基础逻辑连接词的公理系统 里,上面三条公理模式等价于下面这条公理模式[ 3] :
公理 — 如果
B
{\displaystyle {\mathcal {B}}}
、
C
{\displaystyle {\mathcal {C}}}
、
D
{\displaystyle {\mathcal {D}}}
、
E
{\displaystyle {\mathcal {E}}}
和
F
{\displaystyle {\mathcal {F}}}
都是公式,则:
[
B
|
(
C
|
D
)
]
|
{
[
E
|
(
E
|
E
)
]
|
{
(
F
|
C
)
|
[
(
B
|
F
)
|
(
B
|
F
)
]
}
}
{\displaystyle [\,{\mathcal {B}}|({\mathcal {C}}|{\mathcal {D}})\,]|{\big \{}\,[\,{\mathcal {E}}|({\mathcal {E}}|{\mathcal {E}})\,]|\{\,({\mathcal {F}}|{\mathcal {C}})|[\,({\mathcal {B}}|{\mathcal {F}})|({\mathcal {B}}|{\mathcal {F}})\,]\,\}\,{\big \}}}
都是公理。
它们实际上也是公理模式 。
根据不同作者的看法,甚至是理论本身的需求,“等式”在形式理论里可能是断言符号或是一段公式(如 a 等于 b 可定义为对所有的 x , x 属于 a 等价于 x 属于 b )。而如何刻划直观上“等式的性质”,有一开始就将“等式的性质”视为公理(模式),但也有视为元定理 的另一套处理方法,以下暂且以公理模式 的方式处理。以元定理处理的方法会在等式定理 详述。
事实上这两个公理模式也确保了函数符号“唯一对应”和常数符号的“唯一性”,但证明这些性质需要一些元定理 ,简便起见合并于下面的等式定理 一节讲述。
一阶逻辑的标准语义 源于波兰逻辑学家阿尔弗雷德·塔斯基 所著《On the Concept of Truth in Formal Languages》 。根据上面语法 一节,公式是由原子公式递归地添加逻辑链接词而来的,而原子公式是由断言符号与项所构成的。所以要检验一条公式在特定的论域下正不正确,就要规定项的取值 ,然后检验这样的取值会不会落在断言符号所对应的关系 里。由此延伸出所有公式的“真假值“。
也就是一套一阶逻辑的语义解释,要包含
变量取值的论域
如何解释函数符号(为论域中的某个函数)与常数符号(为论域中的某特定元素),以便从特定的变量取值得出项的取值。
如何将断言符号与论域里的某关系做对应。
通常一套解释方法(简称为解释 )会以代号
M
{\displaystyle M}
表示。
量词的解释 需要指明变量取值范围的论域 ——也就是一个集合
D
{\displaystyle D}
。而变量可能跟自然数一样多,换句话说,所有变量在论域
D
{\displaystyle D}
取的值可以依序以自然数标下标——也就是一个在
D
{\displaystyle D}
取值的数列 。如果以
x
1
,
x
2
,
x
3
,
⋯
{\displaystyle x_{1},\,x_{2},\,x_{3},\,\cdots }
的代号(不一定是变量本身的表示符号)来枚举变量,那么从
D
{\displaystyle D}
的某套变量取值就以
⟨
a
k
⟩
k
∈
N
{\displaystyle \left\langle a_{k}\right\rangle _{k\in \mathbb {N} }}
或较直观的符号
⟨
a
1
,
a
2
,
a
3
,
⋯
⟩
{\displaystyle \left\langle a_{1},\,a_{2},\,a_{3},\,\cdots \right\rangle }
来表示。
一套解释
M
{\displaystyle M}
会将
n
{\displaystyle n}
元函数符号
f
i
n
{\displaystyle f_{i}^{n}}
解释成某个
(
f
i
n
)
M
:
D
n
→
D
{\displaystyle {(f_{i}^{n})}^{M}:D^{n}\to D}
的
n
{\displaystyle n}
元函数 ;而常数符号
c
l
{\displaystyle c_{l}}
解释成特定的
c
l
M
∈
D
{\displaystyle {c_{l}}^{M}\in D}
(亦称为
c
l
{\displaystyle c_{l}}
的取值为
c
l
M
{\displaystyle {c_{l}}^{M}}
),这样就可以用上面语法 一节定义项的方式,递归地规定项的取值 :
元定义 — 在解释
M
{\displaystyle M}
下的某套变量取值下,一列项
T
1
,
⋯
,
T
n
{\displaystyle T_{1},\,\cdots ,\,T_{n}}
的取值分别为
T
1
M
,
⋯
,
T
n
M
{\displaystyle {T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M}}
,则这套变量取值下,项
f
i
n
(
T
1
,
⋯
,
T
n
)
{\displaystyle f_{i}^{n}(T_{1},\,\cdots ,\,T_{n})}
的取值规定为
(
f
i
n
)
M
(
T
1
M
,
⋯
,
T
n
M
)
{\displaystyle {(f_{i}^{n})}^{M}({T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M})}
直观上要解释关系最直接的方法,就是枚举所有符合关系的对象;例如如果想说明夫妻关系 ,可以枚举所有(老公, 老婆)的双元有序对 ,但并非所有的人类有序对都会在这个关系中。
以此为基础,若以
D
m
{\displaystyle D^{m}}
代表所有以
m
{\displaystyle m}
个
D
{\displaystyle D}
中的元素构成的
m
{\displaystyle m}
元有序对的集合(也就是
m
{\displaystyle m}
元笛卡尔积 ) ,那一套解释
M
{\displaystyle M}
会将
m
{\displaystyle m}
元断言符号
A
j
m
{\displaystyle A_{j}^{m}}
解释为一个
(
A
j
m
)
M
⊆
D
m
{\displaystyle {(A_{j}^{m})}^{M}\subseteq D^{m}}
的
m
{\displaystyle m}
元有序对 子集合。
这样就可以依据语法的递归定义,以下面的规则对每条公式赋予真值。(这种赋值方式称为T-模式 ,取名于逻辑学家阿尔弗雷德·塔斯基)
元定义 — 在一套解释
M
{\displaystyle M}
下:
在一套特定的变量取值下,一列项
T
1
,
⋯
,
T
m
{\displaystyle T_{1},\,\cdots ,\,T_{m}}
的取值为
T
1
M
,
⋯
,
T
m
M
{\displaystyle {T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M}}
,那
A
j
m
(
T
1
,
⋯
,
T
m
)
{\displaystyle A_{j}^{m}(T_{1},\,\cdots ,\,T_{m})}
为真定义为
(
T
1
M
,
⋯
,
T
m
M
)
∈
(
A
j
m
)
M
{\displaystyle ({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\in {(A_{j}^{m})}^{M}}
反之
(
T
1
M
,
⋯
,
T
m
M
)
∉
(
A
j
m
)
M
{\displaystyle ({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\notin {(A_{j}^{m})}^{M}}
则定义为假。
在一套特定的变量取值下,“
(
¬
B
)
{\displaystyle (\neg {\mathcal {B}})}
为真” 等价于 “
B
{\displaystyle {\mathcal {B}}}
为假”。
在一套特定的变量取值下,
(
B
⇒
C
)
{\displaystyle ({\mathcal {B}}\Rightarrow {\mathcal {C}})}
为真,意为“
B
{\displaystyle {\mathcal {B}}}
为假或是
C
{\displaystyle {\mathcal {C}}}
为真。” (p =>q 为假只有p 为真且q 为假的状况)
在变量取值
⟨
a
k
⟩
k
∈
N
{\displaystyle \left\langle a_{k}\right\rangle _{k\in \mathbb {N} }}
下,
(
∀
x
i
B
)
{\displaystyle (\forall x_{i}{\mathcal {B}})}
为真,意为“对所有的
d
∈
D
{\displaystyle d\in D}
,
B
{\displaystyle {\mathcal {B}}}
于变量取值
⟨
a
1
,
⋯
,
a
i
−
1
,
d
,
a
i
+
1
,
⋯
⟩
{\displaystyle \left\langle a_{1},\,\cdots ,\,a_{i-1},\,d,\,a_{i+1},\,\cdots \right\rangle }
下为真”。(也就是把变量
x
i
{\displaystyle x_{i}}
的取值换为论域的任意元素仍然为真)
更进一步的来说
另一种一阶逻辑语义的方法可经由命题逻辑的林登鲍姆-塔斯基代数 扩展而成。有如下几种类型:
这些代数 都是纯粹扩展两元素布尔代数 而成的格 。
塔斯基和葛范德于1987年证明,没有超过包在三个以上的量化内的原子句子 的部分一阶逻辑,其表示力和关系代数 相同。上述部分一阶逻辑令人十分地感到有兴趣,因为它已足够表示皮亚诺算术 和公理化集合论 ,包括典型的ZFC 。他们亦证明了,具有简单有序对的一阶逻辑和具有两个有序的投影函数 的关系代数等价。
上述的语义解释都要求论域为非空集合。但在如自由逻辑 之中,设置空论域是被允许的。甚至代数结构的类包含一个空结构(如空偏序集 ),当允许空论域时,这个类只能是一阶逻辑中的一个基本类,不然就要将空结构由类中移除。
不过,空论域存在着一些难点:
许多常见的推理规则只在论域被要求是非空时才为有效的。一个例子为,当x 不是
ϕ
{\displaystyle \phi \,}
内的自由变量时,
ϕ
∨
∃
x
ψ
{\displaystyle \phi \lor \exists x\psi }
会蕰涵
∃
x
(
ϕ
∨
ψ
)
{\displaystyle \exists x(\phi \lor \psi )}
。这个用来将公式写成前束范型 的规则在非空论域中是可靠的,但在允许空论域时则是不可靠的。
在使用变量赋值函数的解释中,真值的定义不能和空论域一起运作,因为不存在范围为空的变量赋值函数。(相似地,也无法将解释赋予上常数符号。)在甚至是原子公式的真值可被定义之前,都必须选定一个变量赋值函数。然后一个句子的真值即可在任一个变量赋值之下定义出其真值,且可证明其真值不依选定的赋值而变。这个做法在赋值函数不存在时不能运作;除非将其改成配上空论域。
因此,若空论域是被允许的,通常也必须被视成特例。不过,大多数的作家会简单地将空论域由定义中排除。
以下介绍一些基本用语和符号
口语上会称公式
A
{\displaystyle {\mathcal {A}}}
(或
⊢
L
A
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {A}}}
) 为
L
{\displaystyle {\mathcal {L}}}
下的定理 (theorem)。而这列
C
i
(
1
≤
i
≤
n
)
{\displaystyle {\mathcal {C}}_{i}\,\,(1\leq i\leq n)}
会称为
⊢
L
A
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {A}}}
的证明 。
例如定理
(
I
)
{\displaystyle (I)}
⊢
L
B
⇒
B
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {B}}}
的证明:
以上其实是蕴含了无限多定理的元定理 的证明(因为没有给出合式公式的明确形式)。方便起见,这种元定理 还是会称为定理并以同样的形式来表达。
直观上的证明,总是会有一些“前提假设”,对此,若以
Γ
{\displaystyle \Gamma }
代表一列有限数目的公式,那
这样称
C
i
(
1
≤
i
≤
n
)
{\displaystyle {\mathcal {C}}_{i}\,\,(1\leq i\leq n)}
为在前提
Γ
{\displaystyle \Gamma }
下,
A
{\displaystyle {\mathcal {A}}}
的证明 ;或是说
A
{\displaystyle {\mathcal {A}}}
是
Γ
{\displaystyle \Gamma }
的推论结果 。
若要特别凸显
Γ
{\displaystyle \Gamma }
里的一条"前提条件"
B
{\displaystyle {\mathcal {B}}}
对"证明过程"的重要性,可以用
Γ
,
B
⊢
L
A
{\displaystyle \Gamma ,\,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {A}}}
的符号去特别凸显。若
Γ
{\displaystyle \Gamma }
里的公式枚举出来有
B
1
,
.
.
.
,
B
n
{\displaystyle {\mathcal {B}}_{1},...,{\mathcal {B}}_{n}}
,那亦可表示为
B
1
,
.
.
.
,
B
n
⊢
L
A
{\displaystyle {\mathcal {B}}_{1},...,{\mathcal {B}}_{n}\vdash _{\mathcal {L}}{\mathcal {A}}}
证明过程没有被引用的公式尽可能不写出来。另一方面从以上对于证明定义可以发现,依怎样的顺序枚举前提条件,对于证明本身是不会有任何影响的。
本节所介绍的符号,在引用哪个理论很显然的情况下,
⊢
L
{\displaystyle \vdash _{\mathcal {L}}}
的下标
L
{\displaystyle {\mathcal {L}}}
可以省略。
实际的证明常常会"引用"别的(元)定理,严格来说,就是照抄(元)定理的证明过程,然后作一些修改使符号一致。为了节省证明的篇幅,引用时只会单单列出配合引用(元)定理所得出的公式(形式),并在后面注明引用的(元)定理代号。
从公理(A1)和(A2)会得出不但直观且实用的演绎元定理 :
因为
Γ
{\displaystyle \Gamma }
代表的是有限条公式,所以透过演绎元定理可以将证明过程必要的前提条件递归地移到
⊢
{\displaystyle \vdash }
后,直到不需要任何前提为止;然后由MP律可以知道,若有
Γ
⊢
L
B
⇒
C
{\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}}
,则有
Γ
,
B
⊢
L
C
{\displaystyle \Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}}
,如此一来透过演绎元定理搬到推论结果的合式公式,也可以任意的搬回来。所以
Γ
⊢
L
B
{\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}}
等价于某定理
⊢
L
C
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {C}}}
。因此也会将
Γ
⊢
L
B
{\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}}
称为一个定理 。
而从演绎元定理和MP律,会有以下直观且实用的元定理
元定理 —
(D1)
D
1
⇒
D
2
,
D
2
⇒
D
3
⊢
D
1
⇒
D
3
{\displaystyle {\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{2},\,{\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}}
(D2)
D
1
⇒
(
D
2
⇒
D
3
)
,
D
2
⊢
D
1
⇒
D
3
{\displaystyle {\mathcal {D}}_{1}\Rightarrow ({\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}),\,{\mathcal {D}}_{2}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}}
以下如果需要将引用的定理以演绎元定理进行"搬移",会省略掉搬移的过程并在搬移后得到的结果后标注(D)。如果引用以上的(D1)和(D2)也会省略过程,单有结果和代号标注。
以下的证明会分成使用(A3)的部分跟将公理(A3)取代为(T1)的部分,用以证明两者的等价性。
(DNe) Double negation, elimination —
⊢
¬
¬
A
⇒
A
{\displaystyle \vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
证明(使用A3)
(1)
(
¬
A
⇒
¬
¬
A
)
⇒
[
(
¬
A
⇒
¬
A
)
⇒
A
]
{\displaystyle (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}]}
(A3)
(2)
¬
A
⇒
¬
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}}
(I)
(3)
(
¬
A
⇒
¬
¬
A
)
⇒
A
{\displaystyle (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}}
(D2 with 1, 2)
(4)
¬
¬
A
⇒
(
¬
A
⇒
¬
¬
A
)
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})}
(A1)
(5)
¬
¬
A
⇒
A
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
(D1 with 3, 4)
证明(使用T1)
(1)
¬
¬
A
⇒
(
¬
¬
¬
¬
A
⇒
¬
¬
A
)
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow (\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})}
(A1)
(2)
¬
¬
A
{\displaystyle \neg \neg {\mathcal {A}}}
(Hyp)
(3)
¬
¬
¬
¬
A
⇒
¬
¬
A
{\displaystyle \neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(MP with 2, 1)
(4)
¬
A
⇒
¬
¬
¬
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg \neg \neg {\mathcal {A}}}
(MP with 3, T1)
(5)
¬
¬
A
⇒
A
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
(MP with 4, T1)
(6)
A
{\displaystyle {\mathcal {A}}}
(MP with 2, 5)
(DNi) Double negation, introduction —
⊢
A
⇒
¬
¬
A
{\displaystyle \vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
证明(使用A3)
(1)
(
¬
¬
¬
A
⇒
¬
A
)
⇒
[
(
¬
¬
¬
A
⇒
A
)
⇒
¬
¬
A
]
{\displaystyle (\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}]}
(A3)
(2)
(
¬
¬
¬
A
⇒
A
)
⇒
¬
¬
A
{\displaystyle (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}}
(MP with DNe, 1)
(3)
A
⇒
(
¬
¬
¬
A
⇒
A
)
{\displaystyle {\mathcal {A}}\Rightarrow (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})}
(A1)
(4)
A
⇒
¬
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(D1 with 2,3)
证明(使用T1)
(1)
¬
¬
¬
A
⇒
¬
A
{\displaystyle \neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}}
(DNe)
(2)
A
⇒
¬
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(MP with 1, T1)
上面两定理表达了双否定推理上等价于于原公式,引用两者任一会都以(DN)简写。
(T1) Transposition-1 —
¬
A
⇒
¬
B
⊢
B
⇒
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}}
证明(使用A3)
(1)
(
¬
A
⇒
¬
B
)
⇒
[
(
¬
A
⇒
B
)
⇒
A
]
{\displaystyle (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}]}
(A3)
(2)
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(Hyp)
(3)
(
¬
A
⇒
B
)
⇒
A
{\displaystyle (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}}
(MP with 1, 2)
(4)
B
⇒
(
¬
A
⇒
B
)
{\displaystyle {\mathcal {B}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})}
(A1)
(5)
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(D1 with 3, 4)
(T2) Transposition-2 —
B
⇒
A
⊢
¬
A
⇒
¬
B
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}\vdash \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
证明(使用T1)
(1)
¬
¬
B
⇒
B
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}}
(DN)
(2)
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(Hyp)
(3)
¬
¬
B
⇒
A
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(D with 1, 2)
(4)
A
⇒
¬
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(DN)
(5)
¬
¬
B
⇒
¬
¬
A
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}}
(D1 with 3,4)
(6)
(
¬
¬
B
⇒
¬
¬
A
)
⇒
(
¬
A
⇒
¬
B
)
{\displaystyle (\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})}
(T1, D)
(7)
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(MP with 5, 6)
注意到(T2)的证明引用了(T1)+(DN),但之前已经证明了(A1)+(A2)+(A3)可以推出(T1);还有(A1)+(A2)+(T1)也可以推出(DN),所以注明使用(T1)即可。
以上二定理说明
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
推理上等价于
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
,引用这两个定理中任一都以(T)表示。
至此,已经可以证明(A1)+(A2)+(T1)可以推出(A3):
(T1)可推出(A3)的证明
由MP律 显然有
¬
B
,
(
¬
B
⇒
B
)
⊢
B
{\displaystyle \neg {\mathcal {B}},\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {B}}}
(1)
¬
B
⇒
[
(
¬
B
⇒
B
)
⇒
B
]
{\displaystyle \neg {\mathcal {B}}\Rightarrow [\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}\,]}
(对上面的定理使用两次演绎元定理)
(2)
¬
B
⇒
[
¬
B
⇒
¬
(
¬
B
⇒
B
)
]
{\displaystyle \neg {\mathcal {B}}\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]}
(D1 with 1, T2)
(3)
(
¬
B
⇒
¬
B
)
⇒
[
¬
B
⇒
¬
(
¬
B
⇒
B
)
]
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]}
(MP with A2, 2)
(4)
¬
B
⇒
¬
(
¬
B
⇒
B
)
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})}
(MP with I, 3)
(5)
(
¬
B
⇒
B
)
⇒
B
{\displaystyle (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}}
(MP with T1, 4)
(6)
(
¬
B
)
⇒
(
¬
C
)
{\displaystyle (\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})}
(Hyp)
(7)
¬
B
⇒
C
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(Hyp)
(8)
¬
C
⇒
¬
¬
B
{\displaystyle \neg {\mathcal {C}}\Rightarrow \neg \neg {\mathcal {B}}}
(MP with T2, 7)
(9)
¬
B
⇒
¬
¬
B
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {B}}}
(D1 with 6, 8)
(10)
¬
B
⇒
B
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}}
(D1 with DN, 9)
(11)
B
{\displaystyle {\mathcal {B}}}
(MP with 5, 10)
所以综合以上所述,在有(A1)+(A2)的前提下,公理(T1)等价于公理(A3)。
由(T)可以得到类似于公理(A3)的定理
(A3') —
A
⇒
B
,
¬
A
⇒
B
⊢
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}}
证明
(1)
(
¬
B
⇒
¬
¬
A
)
⇒
[
(
¬
B
⇒
¬
A
)
⇒
B
]
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]}
(A3)
(2)
(
¬
A
⇒
B
)
⇒
(
¬
B
⇒
¬
¬
A
)
{\displaystyle (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})}
(T, D)
(3)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(Hyp)
(4)
¬
B
⇒
¬
¬
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}}
(MP with 2, 3)
(5)
(
¬
B
⇒
¬
A
)
⇒
B
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}}
(MP with 1, 4)
(6)
(
A
⇒
B
)
⇒
(
¬
B
⇒
¬
A
)
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})}
(T, D)
(7)
A
⇒
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(Hyp)
(8)
¬
B
⇒
¬
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with 6, 7)
(9)
B
{\displaystyle {\mathcal {B}}}
(MP with 5, 8)
以下的定理重现了实质条件 的直观理解。
(M0)material condition —
¬
A
,
A
⊢
B
{\displaystyle \neg {\mathcal {A}},{\mathcal {A}}\vdash {\mathcal {B}}}
(也就是
¬
A
⊢
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}}
)
证明
(1)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(Hyp)
(2)
A
{\displaystyle {\mathcal {A}}}
(Hyp)
(3)
(
¬
B
⇒
¬
A
)
⇒
[
(
¬
B
⇒
A
)
⇒
B
]
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}]}
(A3)
(4)
¬
A
⇒
(
¬
B
⇒
¬
A
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})}
(A1)
(5)
¬
B
⇒
¬
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with 4, 1)
(6)
A
⇒
(
¬
B
⇒
A
)
{\displaystyle {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})}
(A1)
(7)
¬
B
⇒
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(MP with 6, 2)
(8)
(
¬
B
⇒
A
)
⇒
B
{\displaystyle (\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}}
(MP with 3,5)
(9)
B
{\displaystyle {\mathcal {B}}}
(MP with 8,7)
(M1)material condition —
A
,
¬
B
⊢
¬
(
A
⇒
B
)
{\displaystyle {\mathcal {A}},\neg {\mathcal {B}}\vdash \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
证明
首先注意到
A
,
A
⇒
B
⊢
B
{\displaystyle {\mathcal {A}},{\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}}
(MP)
(1)
A
⇒
[
(
A
⇒
B
)
⇒
B
]
{\displaystyle {\mathcal {A}}\Rightarrow [({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]}
(0, D)
(2)
[
(
A
⇒
B
)
⇒
B
]
⇒
{
¬
B
⇒
[
¬
(
A
⇒
B
)
]
}
{\displaystyle [({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]\Rightarrow \{\neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\}}
(T)
(3)
A
{\displaystyle {\mathcal {A}}}
(Hyp)
(4)
(
A
⇒
B
)
⇒
B
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}}
(MP with 1, 3)
(5)
¬
B
⇒
[
¬
(
A
⇒
B
)
]
{\displaystyle \neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]}
(MP with 2, 4)
(6)
¬
B
{\displaystyle \neg {\mathcal {B}}}
(Hyp)
(7)
¬
(
A
⇒
B
)
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(MP 5, 6)
(M2)material condition —
¬
(
A
⇒
B
)
⊢
¬
B
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash \neg {\mathcal {B}}}
证明
(1)
B
⇒
(
A
⇒
B
)
{\displaystyle {\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(A1)
(2)
[
B
⇒
(
A
⇒
B
)
]
⇒
{
[
¬
(
A
⇒
B
)
]
⇒
(
¬
B
)
}
{\displaystyle [{\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})\}}
(T)
(3)
[
¬
(
A
⇒
B
)
]
⇒
(
¬
B
)
{\displaystyle [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})}
(MP with 1, 2)
(4)
¬
(
A
⇒
B
)
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(Hyp)
(5)
¬
B
{\displaystyle \neg {\mathcal {B}}}
(MP with 3, 4)
(M3)material condition —
¬
(
A
⇒
B
)
⊢
A
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {A}}}
证明
(1)
¬
A
⇒
(
A
⇒
B
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(M0, D)
(2)
[
¬
A
⇒
(
A
⇒
B
)
]
⇒
{
[
¬
(
A
⇒
B
)
]
⇒
(
¬
¬
A
)
}
{\displaystyle [\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})\}}
(T)
(3)
[
¬
(
A
⇒
B
)
]
⇒
(
¬
¬
A
)
{\displaystyle [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})}
(MP with 1, 2)
(4)
¬
(
A
⇒
B
)
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(Hyp)
(5)
¬
¬
A
{\displaystyle \neg \neg {\mathcal {A}}}
(MP with 3,4)
(6)
A
{\displaystyle {\mathcal {A}}}
(MP with 5, DN)
(C1)Proof by Contradiction —
A
⇒
¬
B
,
B
⊢
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}},{\mathcal {B}}\vdash \neg {\mathcal {A}}}
证明
(1)
(
A
⇒
¬
B
)
⇒
(
¬
¬
B
⇒
¬
A
)
{\displaystyle ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow (\neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})}
(T, D)
(2)
A
⇒
¬
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(Hyp)
(3)
¬
¬
B
⇒
¬
A
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with 1, 2)
(4)
B
{\displaystyle {\mathcal {B}}}
(Hyp)
(5)
¬
¬
B
{\displaystyle \neg \neg {\mathcal {B}}}
(MP with DN, 4)
(6)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(MP with 3, 5)
(C2)Proof by Contradiction —
¬
A
⇒
B
,
¬
B
⊢
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}}
以下为逻辑与 的交换性
元定理 —
⊢
(
A
∧
B
)
⇒
(
B
∧
A
)
{\displaystyle \vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow ({\mathcal {B}}\wedge {\mathcal {A}})}
证明
(1)
(
B
⇒
¬
A
)
⇒
(
A
⇒
¬
B
)
{\displaystyle ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})}
(C1, D)
(2)
[
(
B
⇒
¬
A
)
⇒
(
A
⇒
¬
B
)
]
⇒
{
[
¬
(
A
⇒
¬
B
)
]
⇒
[
¬
(
B
⇒
¬
A
)
]
}
{\displaystyle [({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]\}}
(T, D)
(3)
[
¬
(
A
⇒
¬
B
)
]
⇒
[
¬
(
B
⇒
¬
A
)
]
{\displaystyle [\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]}
(MP with 1,2)
类似的,(C2)正是逻辑或 的交换性:
元定理 —
A
∨
B
⊢
B
∨
A
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {B}}\vee {\mathcal {A}}}
(C2, D)
"且"的直观意义是实质条件元定理的直接结果
(AND)Intuitive meaning of And —
A
,
B
⊢
A
∧
B
{\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}}
(M1)
A
∧
B
⊢
A
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}}
(M3)
A
∧
B
⊢
B
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}}
(M2)
从(AND)和
⇔
{\displaystyle \Leftrightarrow }
的符号定义可知,
⊢
B
⇔
C
{\displaystyle \vdash {\mathcal {B}}\Leftrightarrow {\mathcal {C}}}
的证明可以拆成两部分;习惯上会以“(
⇒
{\displaystyle \Rightarrow }
) ”标示
⊢
B
⇒
C
{\displaystyle \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}}
部分的证明,而“(
⇐
{\displaystyle \Leftarrow }
) ”标示
⊢
C
⇒
B
{\displaystyle \vdash {\mathcal {C}}\Rightarrow {\mathcal {B}}}
部分的证明。
类似的,"或"的直观意义是(M0)跟(D)的直截结果
(OR)Intuitive meaning of OR —
A
⊢
A
∨
B
{\displaystyle {\mathcal {A}}\vdash {\mathcal {A}}\vee {\mathcal {B}}}
(M0, DN)
B
⊢
A
∨
B
{\displaystyle {\mathcal {B}}\vdash {\mathcal {A}}\vee {\mathcal {B}}}
(A1, D)
A
∨
B
,
¬
A
⊢
B
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {A}}\vdash {\mathcal {B}}}
(D)
A
∨
B
,
¬
B
⊢
A
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}}
(交换性, D)
以下的定理则是(A3')的直截结果
(DisJ)Disjunction —
A
⇒
C
,
B
⇒
C
,
A
∨
B
⊢
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}},{\mathcal {B}}\Rightarrow {\mathcal {C}},{\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {C}}}
证明
(1)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(Hyp)
(2)
B
⇒
C
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(Hyp)
(3)
¬
A
⇒
C
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(D1 with 1, 2)
(4)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(Hyp)
(5)
C
{\displaystyle {\mathcal {C}}}
(A3' with 3, 4)
对于"且",展开符号定义后,可以从直观意义轻松地得到
(ASO-AND)Associativity of AND —
⊢
A
∧
(
B
∧
C
)
⇔
(
A
∧
B
)
∧
C
{\displaystyle \vdash {\mathcal {A}}\wedge ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\wedge {\mathcal {C}}}
"或"也有类似的性质
(ASO-OR)Associativity of OR —
⊢
A
∨
(
B
∨
C
)
⇔
(
A
∨
B
)
∨
C
{\displaystyle \vdash {\mathcal {A}}\vee ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\vee {\mathcal {C}}}
"且"和"或"之间还有分配律
(DIS-1)Distribution —
⊢
A
∧
(
B
∨
C
)
⇔
(
A
∧
B
)
∨
(
A
∧
C
)
{\displaystyle \vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})}
证明
(
⇒
{\displaystyle \Rightarrow }
)
(1)
A
∧
(
B
∨
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})}
(Hyp)
(2)
A
{\displaystyle {\mathcal {A}}}
(MP with 1, AND)
(3)
¬
B
⇒
C
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(MP with 1, AND)
(4)
¬
¬
(
A
⇒
¬
B
)
{\displaystyle \neg \neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})}
(Hyp)
(5)
A
⇒
¬
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(MP with 4, DN)
(6)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(D1 with 3, 5)
(7)
C
{\displaystyle {\mathcal {C}}}
(MP with 2, 5)
(8)
A
∧
C
{\displaystyle {\mathcal {A}}\wedge {\mathcal {C}}}
(MP twice with 2, 7, AND)
也就是
A
∧
(
B
∨
C
)
,
¬
(
A
∧
B
)
⊢
A
∧
C
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg ({\mathcal {A}}\wedge {\mathcal {B}})\vdash {\mathcal {A}}\wedge {\mathcal {C}}}
再套用(D)就会得到
A
∧
(
B
∨
C
)
⊢
(
A
∧
B
)
∨
(
A
∧
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})}
(
⇐
{\displaystyle \Leftarrow }
)
(1)
¬
(
A
∧
B
)
⇒
A
∧
C
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}\wedge {\mathcal {C}}}
(Hyp)
(2)
¬
(
A
∧
B
)
⇒
A
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}}
(D1 with 1, AND)
(3)
¬
(
A
∧
B
)
⇒
C
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}}
(D1 with 1, AND)
(4)
¬
A
⇒
(
A
∧
B
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})}
(MP with 2, C2)
(5)
¬
C
⇒
(
A
∧
B
)
{\displaystyle \neg {\mathcal {C}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})}
(MP with 3, C2)
(6)
¬
A
⇒
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
(D1 with 4, AND)
(7)
¬
C
⇒
B
{\displaystyle \neg {\mathcal {C}}\Rightarrow {\mathcal {B}}}
(D1 with 4, AND)
(8)
A
{\displaystyle {\mathcal {A}}}
(A3' with 6, I)
(9)
A
∧
(
B
∨
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})}
(MP twice with 7, 8, AND)
也就是
(
A
∧
B
)
∨
(
A
∧
C
)
⊢
A
∧
(
B
∨
C
)
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})}
(DIS-2)Distribution —
⊢
A
∨
(
B
∧
C
)
⇔
(
A
∨
B
)
∧
(
A
∨
C
)
{\displaystyle \vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})}
证明
(
⇒
{\displaystyle \Rightarrow }
)
(1)
¬
A
⇒
(
B
∧
C
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow ({\mathcal {B}}\wedge {\mathcal {C}})}
(Hyp)
(2)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(D1 with 1, AND)
(3)
¬
A
⇒
C
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(D1 with 1, AND)
(4)
(
A
∨
B
)
∧
(
A
∨
C
)
{\displaystyle ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})}
(MP twice with 2, 3,AND)
也就是
A
∨
(
B
∧
C
)
⊢
(
A
∨
B
)
∧
(
A
∨
C
)
{\displaystyle {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\vdash ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})}
(
⇐
{\displaystyle \Leftarrow }
)
(1)
(
¬
A
⇒
B
)
∧
(
¬
A
⇒
C
)
{\displaystyle (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge (\neg {\mathcal {A}}\Rightarrow {\mathcal {C}})}
(Hyp)
(2)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(MP with 1, AND)
(3)
¬
A
⇒
C
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(MP with 1, AND)
(4)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(Hyp)
(5)
B
{\displaystyle {\mathcal {B}}}
(MP with 2,4)
(6)
C
{\displaystyle {\mathcal {C}}}
(MP with 3,4)
(7)
B
∧
C
{\displaystyle {\mathcal {B}}\wedge {\mathcal {C}}}
(MP twice with 5, 6, AND)
也就是
A
∧
(
B
∨
C
)
,
¬
A
⊢
B
∧
C
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg {\mathcal {A}}\vdash {\mathcal {B}}\wedge {\mathcal {C}}}
再使用一次推论元定理会得到
A
∧
(
B
∨
C
)
⊢
A
∨
(
B
∧
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})}
以下的元定理的名字来自于英国逻辑学家奥古斯塔斯·德摩根 。
De Morgan I —
⊢
[
¬
(
A
∧
B
)
]
⇔
[
(
¬
A
)
∨
(
¬
B
)
]
{\displaystyle \vdash [\neg ({\mathcal {A}}\wedge {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\vee (\neg {\mathcal {B}})]}
De Morgan II —
⊢
[
¬
(
A
∨
B
)
]
⇔
[
(
¬
A
)
∧
(
¬
B
)
]
{\displaystyle \vdash [\neg ({\mathcal {A}}\vee {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})]}
公理模式 (A7)可以稍加延伸成以下的元定理
定理的普遍化 —
对任意变量
x
{\displaystyle x}
,若
⊢
B
{\displaystyle \vdash {\mathcal {B}}}
则有
⊢
(
∀
x
)
B
{\displaystyle \vdash (\forall x){\mathcal {B}}}
。
更进一步,有以下元定里
(GEN) —
在
A
1
,
A
2
,
.
.
.
.
,
A
n
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}}
里变量
x
{\displaystyle x}
都完全被约束,若
A
1
,
A
2
,
.
.
.
.
,
A
n
⊢
B
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash {\mathcal {B}}}
则有
A
1
,
A
2
,
.
.
.
.
,
A
n
⊢
(
∀
x
)
B
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash (\forall x){\mathcal {B}}}
证明
以下对前提条件的数量
n
{\displaystyle n}
做归纳。
若
n
=
1
{\displaystyle n=1}
,根据前提有
A
1
⊢
B
{\displaystyle {\mathcal {A}}_{1}\vdash {\mathcal {B}}}
以(D)将
A
1
{\displaystyle {\mathcal {A}}_{1}}
往前搬,再套用定理的普遍化,会得到
⊢
(
∀
x
)
(
A
1
⇒
B
)
{\displaystyle \vdash (\forall x)({\mathcal {A}}_{1}\Rightarrow {\mathcal {B}})}
再根据(A5)和MP律,就可以得到
⊢
A
1
⇒
(
∀
x
)
B
{\displaystyle \vdash {\mathcal {A}}_{1}\Rightarrow (\forall x){\mathcal {B}}}
也就是本元定理要求的结果。
现在假设
n
<
k
{\displaystyle n<k}
的情况下元定理会成立。元定理的前提条件根据(D)可以写为
A
1
,
A
2
,
.
.
.
.
,
A
k
−
1
⊢
A
k
⇒
B
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash {\mathcal {A}}_{k}\Rightarrow {\mathcal {B}}}
则根据归纳法的假设
A
1
,
A
2
,
.
.
.
.
,
A
k
−
1
⊢
(
∀
x
)
(
A
k
⇒
B
)
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash (\forall x)({\mathcal {A}}_{k}\Rightarrow {\mathcal {B}})}
上式配上(A5),本元定理在
n
=
k
{\displaystyle n=k}
的情况就可以得到证明,故本元定理得证。
◻
{\displaystyle \Box }
(GEN)可以稍加修饰,以套用在含有存在量词的公式上
以下的定理,说明两条“等价”的公式可以互相代换
证明
以下的证明都会用到这三条公式:
(a)
A
⇔
B
{\displaystyle {\mathcal {A}}\Leftrightarrow {\mathcal {B}}}
(from
Γ
{\displaystyle \Gamma }
)
(b)
A
⇒
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(MP with AND , a)
(c)
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(MP with AND , a)
1.
(1)
(
¬
B
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})}
(MP with T , b)
(2)
(
¬
A
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})}
(MP with T , c)
(3)
(
¬
A
)
⇔
(
¬
B
)
{\displaystyle (\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})}
(AND with 3, 5)
2.
(
⇒
{\displaystyle \Rightarrow }
)
(1)
C
⇒
A
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {A}}}
(Hyp)
(2)
C
⇒
B
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {B}}}
(D1 with 1, b)
(
⇐
{\displaystyle \Leftarrow }
)
(1)
C
⇒
B
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {B}}}
(Hyp)
(2)
C
⇒
A
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {A}}}
(D1 with 1, c)
3.
(
⇒
{\displaystyle \Rightarrow }
)
(1)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(Hyp)
(2)
(
¬
C
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})}
(MP with T , 1)
(3)
(
¬
A
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})}
(MP with T , c)
(4)
(
¬
C
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})}
(D1 with 2, 3)
(5)
B
⇒
C
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(MP with T , 4)
(
⇐
{\displaystyle \Leftarrow }
)
(1)
B
⇒
C
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(Hyp)
(2)
(
¬
C
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})}
(MP with T , 1)
(3)
(
¬
B
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})}
(MP with T , b)
(4)
(
¬
C
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})}
(D1 with 2, 3)
(5)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(MP with T , 4)
4.
(
⇒
{\displaystyle \Rightarrow }
)
(1)
(
∀
x
)
(
A
⇒
B
)
{\displaystyle (\forall x)({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(GEN with
x
{\displaystyle x}
, a)
(2)
(
∀
x
)
A
⇒
(
∀
x
)
B
{\displaystyle (\forall x){\mathcal {A}}\Rightarrow (\forall x){\mathcal {B}}}
(MP with A6 , 1)
(
⇐
{\displaystyle \Leftarrow }
)
(1)
(
∀
x
)
(
B
⇒
A
)
{\displaystyle (\forall x)({\mathcal {B}}\Rightarrow {\mathcal {A}})}
(GEN with
x
{\displaystyle x}
, c)
(2)
(
∀
x
)
B
⇒
(
∀
x
)
A
{\displaystyle (\forall x){\mathcal {B}}\Rightarrow (\forall x){\mathcal {A}}}
(MP with A6 , 1)
这些定理通常是混合使用,以达到“等价代换”的结果,例如,考虑到“逻辑与”是以下的符号定义:
(
A
∧
C
)
:=
¬
[
A
⇒
(
¬
C
)
]
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {C}}):=\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]}
那如果假设
⊢
A
⇔
B
{\displaystyle \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}}
,就有:
⊢
[
A
⇒
(
¬
C
)
]
⇔
[
B
⇒
(
¬
C
)
]
{\displaystyle \vdash [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]}