数理逻辑思维导图
本思维导图使用
Markmap
制作
异或词
∀
\forall
∀
或非词
f
(
p
,
q
)
=
p
↓
q
=
¬
(
p
∨
q
)
f(p,q)=p\downarrow q = \neg(p\vee q)
f
(
p
,
q
)
=
p
↓
q
=
¬
(
p
∨
q
)
与非词
f
(
p
,
q
)
=
p
↑
q
=
¬
(
p
∧
q
)
f(p,q)=p\uparrow q = \neg(p\land q)
f
(
p
,
q
)
=
p
↑
q
=
¬
(
p
∧
q
)
∃
\exists
∃
消除：
Γ
⊢
∃
v
A
;
Γ
;
A
t
v
⊢
B
Γ
⊢
B
\frac {\Gamma\vdash\exists v A;\Gamma;A_t^v\vdash B} {\Gamma\vdash B}
Γ
⊢
B
Γ
⊢
∃
v
A
;
Γ
;
A
t
v
⊢
B
，即
F
C
FC
FC
的存在消除定理
∃
\exists
∃
引入：
Γ
⊢
A
t
v
Γ
⊢
∃
v
A
\frac {\Gamma\vdash A_t^v} {\Gamma\vdash \exists v A}
Γ
⊢
∃
v
A
Γ
⊢
A
t
v
(
t
t
t
对
v
v
v
可代入)，即
F
C
FC
FC
定理
A
t
v
→
∃
v
A
A_t^v\rightarrow \exists v A
A
t
v
→
∃
v
A
(
t
t
t
对
v
v
v
可代入)
∀
\forall
∀
消除：
Γ
⊢
∀
v
A
Γ
⊢
A
t
v
\frac {\Gamma\vdash\forall v A} {\Gamma\vdash A_t^v}
Γ
⊢
A
t
v
Γ
⊢
∀
v
A
，其中
t
t
t
对变元
v
v
v
可代入。即
F
C
FC
FC
定理
∀
v
A
→
A
t
v
\forall v A\rightarrow A_t^v
∀
v
A
→
A
t
v
∀
\forall
∀
引入：
Γ
⊢
A
Γ
⊢
(
∀
v
A
)
\frac {\Gamma\vdash A} {\Gamma\vdash(\forall v A)}
Γ
⊢
(
∀
v
A
)
Γ
⊢
A
，即对应
F
C
FC
FC
全称引入定理
仅扩充
N
D
ND
N
D
规则，主要为有关量词的规则
在
N
D
ND
N
D
基础上进行扩充
仅为
r
m
p
r_{mp}
r
m
p
看我干什么？看书！
相应地增加公理
对
F
C
FC
FC
进行扩充，变为5个逻辑联结词、2个量词
A
X
1.3
:
(
¬
A
→
¬
B
)
→
(
B
→
A
)
AX1.3:(\neg A\rightarrow\neg B)\rightarrow(B\rightarrow A)
A
X
1.3
:
(
¬
A
→
¬
B
)
→
(
B
→
A
)
A
X
1.2
:
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
AX1.2:(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))
A
X
1.2
:
(
A
→
(
B
→
C
))
→
((
A
→
B
)
→
(
A
→
C
))
A
X
1.1
:
A
→
(
B
→
A
)
AX1.1:A\rightarrow(B\rightarrow A)
A
X
1.1
:
A
→
(
B
→
A
)
不受量词约束
受量词约束
个体常元
α
\alpha
α
：张三
函词
f
(
x
)
f(x)
f
(
x
)
：x的父亲
谓词P:……是工程师
对于含n个个体变元的函词，常记为
f
(
n
)
f^{(n)}
f
(
n
)
含n个个体变元的谓词
反之为个体变元
字母表靠前的一般为个体常元
个体变元
个体常元
谓语（谓+宾）表示对象性质或对象间关系
主语为研究对象或其群体
或为
Γ
j
1
⊢
A
j
1
,
⋯
,
Γ
j
k
⊢
A
j
k
\Gamma_{j_1}\vdash A_{j_1},\cdots,\Gamma_{j_k}\vdash A_{j_k}
Γ
j
1
⊢
A
j
1
,
⋯
,
Γ
j
k
⊢
A
j
k
由推理规则导出公式
或为
Γ
j
⊢
A
j
(
j
<
i
)
\Gamma_j\vdash A_j(j< i)
Γ
j
⊢
A
j
(
j
<
i
)
或为ND公理
联结词的完备集
联结词的可表示性
二元联结词
一元联结词
n元联结词：
f
:
{
T
,
F
}
n
→
{
T
,
F
}
f:\left\{T,F\right\}^n \rightarrow \left\{T,F\right\}
f
:
{
T
,
F
}
n
→
{
T
,
F
}
添加的规则：
说明
推理规则
7组公理及其全称化
说明
更一般地，
∀
B
∈
Γ
,
(
Γ
⊨
T
B
)
⇒
(
Γ
⊢
F
C
B
\forall B\in\Gamma,(\Gamma\models_T B)\Rightarrow(\Gamma\vdash_{FC}B
∀
B
∈
Γ
,
(
Γ
⊨
T
B
)
⇒
(
Γ
⊢
FC
B
看我干什么？看书！
Γ
\Gamma
Γ
为
F
C
FC
FC
公式集
则公理/定理均必为重言式
F
C
FC
FC
之定理、证明、演绎、演绎结果的定义全同于
P
C
PC
PC
故对于
P
C
PC
PC
中已证公式，均可直接调用
因此
P
C
PC
PC
为
F
C
FC
FC
之子系统
由上可见，
P
C
PC
PC
的语言和公式均为
F
C
FC
FC
的子集
内容：
A
,
A
→
B
B
\frac {A,A\rightarrow B} {B}
B
A
,
A
→
B
使用的是
F
C
FC
FC
中公式而非
P
C
PC
PC
，此为区别
全同于
P
C
PC
PC
，仅有
r
m
p
r_{mp}
r
m
p
A
X
1
AX1
A
X
1
除命题变元为一阶语言
L
(
F
C
)
L(FC)
L
(
FC
)
中任意公式外，其形式全同于
P
C
PC
PC
系统三大公理
A
X
4
:
A
→
∀
v
A
AX4:A\rightarrow \forall v A
A
X
4
:
A
→
∀
v
A
(
v
v
v
在
A
A
A
中无自由出现)
A
X
3
:
∀
v
(
A
→
B
)
→
(
(
∀
v
A
)
→
(
∀
v
B
)
)
AX3:\forall v(A\rightarrow B)\rightarrow((\forall v A) \rightarrow(\forall v B))
A
X
3
:
∀
v
(
A
→
B
)
→
((
∀
v
A
)
→
(
∀
v
B
))
A
X
2
:
∀
v
A
→
A
t
v
AX2:\forall v A\rightarrow A_t^v
A
X
2
:
∀
v
A
→
A
t
v
(项
t
t
t
对
v
v
v
可代入)
A
X
1
AX1
A
X
1
说明：下列公式及其全称化均为FC公理
其中
∀
j
=
1
,
⋯
,
r
,
1
≤
i
j
≤
n
\forall j=1,\cdots,r,1\leq i_j\leq n
∀
j
=
1
,
⋯
,
r
,
1
≤
i
j
≤
n
公式
∀
v
i
1
⋯
∀
v
i
r
A
\forall v_{i_1}\cdots\forall v_{i_r} A
∀
v
i
1
⋯
∀
v
i
r
A
称为
A
A
A
的全称化
设
v
1
,
⋯
,
v
n
v_1,\cdots,v_n
v
1
,
⋯
,
v
n
为谓词公式
A
A
A
之自由变元
说明：是以项
t
t
t
代谓词公式
A
A
A
中之
v
v
v
，不要搞反
则称
t
t
t
对
v
v
v
是可代入的
项
t
t
t
中不含
A
A
A
的约束变元符（有则易名）
v
v
v
为谓词公式
A
A
A
中自由变元
例：
∀
x
P
(
x
)
\forall x P(x)
∀
x
P
(
x
)
的改名式
∀
y
P
(
y
)
\forall y P(y)
∀
y
P
(
y
)
，或记为
∀
y
P
(
x
)
y
x
\forall y P(x)_y^x
∀
y
P
(
x
)
y
x
改名后公式称原式的改名式
量词辖域中某一约束变元改为另一个在该辖域未出现的变元
辖域
自由变元
约束边缘
以上条件有限次复合，仍为合式公式
A
A
A
为合式公式，x在
A
A
A
为自由变元，则
∀
x
P
(
x
)
,
∃
x
P
(
x
)
\forall x P(x),\exists x P(x)
∀
x
P
(
x
)
,
∃
x
P
(
x
)
均为合式公式
A
,
B
A,B
A
,
B
为合式公式，且无x在A/B中一个是约束的而另一个是自由的，则
A
∧
B
,
A
∨
B
,
A
→
B
,
A
↔
B
A\land B,A\vee B,A\rightarrow B,A\leftrightarrow B
A
∧
B
,
A
∨
B
,
A
→
B
,
A
↔
B
均为合式公式
若
A
A
A
为合式公式，则
¬
A
\neg A
¬
A
亦为合式公式
不含联结词的单个谓词（原子谓词）是合取公式
注意：没有n元谓词，因谓词产生的是命题
由上述规则有限次复合产生的结果为项
f
(
n
)
f^{(n)}
f
(
n
)
为n元函词，
t
1
,
⋯
,
t
n
t_1,\cdots,t_n
t
1
,
⋯
,
t
n
为项，则
f
(
n
)
(
t
1
,
⋯
,
t
n
)
f^{(n)}(t_1,\cdots,t_n)
f
(
n
)
(
t
1
,
⋯
,
t
n
)
为项
个体常元/变元是项
特称量词
∃
\exists
∃
全称量词
∀
\forall
∀
例：原子命题“张三的父亲是工程师”表示为
P
(
f
(
α
)
)
P(f(\alpha))
P
(
f
(
α
))
以小写字母/小写单词表示
一个个体域到另一个体域的映射
常以大写D表示
个体变元的取值范围
n元谓词
一般以大写字母表示，如
P
(
α
)
P(\alpha)
P
(
α
)
表示研究对象性质或其关系的词
一般用小写字母表示
表示研究对象的词
原子命题为陈述句，陈述句分主谓
其中，
∀
i
=
1
,
⋯
,
m
−
1
,
Γ
i
⊢
A
i
\forall i=1,\cdots,m-1,\Gamma_i\vdash A_i
∀
i
=
1
,
⋯
,
m
−
1
,
Γ
i
⊢
A
i
则存在序列
Γ
1
⊢
A
1
,
⋯
,
Γ
m
⊢
A
m
(
=
A
)
\Gamma_1\vdash A_1,\cdots,\Gamma_m\vdash A_m(=A)
Γ
1
⊢
A
1
,
⋯
,
Γ
m
⊢
A
m
(
=
A
)
在ND中，若
Γ
⊢
N
D
A
\Gamma\vdash_{ND}A
Γ
⊢
N
D
A
由上可见，ND的规则及其直观逻辑含义比较明显，为逻辑推理带来较大方便
↔
\leftrightarrow
↔
消除：
Γ
⊢
A
↔
B
Γ
⊢
A
→
B
,
Γ
⊢
A
↔
B
Γ
⊢
B
→
A
\frac {\Gamma\vdash A\leftrightarrow B} {\Gamma\vdash A\rightarrow B},\frac {\Gamma\vdash A\leftrightarrow B} {\Gamma\vdash B\rightarrow A}
Γ
⊢
A
→
B
Γ
⊢
A
↔
B
,
Γ
⊢
B
→
A
Γ
⊢
A
↔
B
，以上源于重言式
(
A
→
B
)
↔
(
A
→
B
)
∧
(
B
→
A
)
(A\rightarrow B)\leftrightarrow (A\rightarrow B)\land(B\rightarrow A)
(
A
→
B
)
↔
(
A
→
B
)
∧
(
B
→
A
)
↔
\leftrightarrow
↔
引入：
Γ
⊢
A
→
B
;
Γ
⊢
B
→
A
Γ
⊢
A
↔
B
\frac {\Gamma\vdash A\rightarrow B;\Gamma\vdash B\rightarrow A} {\Gamma\vdash A\leftrightarrow B}
Γ
⊢
A
↔
B
Γ
⊢
A
→
B
;
Γ
⊢
B
→
A
¬
¬
\neg\neg
¬¬
消除：
Γ
⊢
¬
¬
A
Γ
⊢
A
\frac {\Gamma\vdash\neg\neg A} {\Gamma\vdash A}
Γ
⊢
A
Γ
⊢
¬¬
A
，以上源于重言式
A
↔
¬
¬
A
A\leftrightarrow\neg\neg A
A
↔
¬¬
A
¬
¬
\neg\neg
¬¬
引入：
Γ
⊢
A
Γ
⊢
¬
¬
A
\frac {\Gamma\vdash A} {\Gamma\vdash\neg\neg A}
Γ
⊢
¬¬
A
Γ
⊢
A
¬
\neg
¬
消除：
Γ
⊢
A
;
Γ
⊢
¬
A
Γ
⊢
B
\frac {\Gamma\vdash A;\Gamma\vdash\neg A} {\Gamma\vdash B}
Γ
⊢
B
Γ
⊢
A
;
Γ
⊢
¬
A
，即重言式
¬
A
→
(
A
→
B
)
\neg A\rightarrow(A\rightarrow B)
¬
A
→
(
A
→
B
)
¬
\neg
¬
引入：
Γ
;
A
⊢
B
;
Γ
;
A
⊢
¬
B
Γ
⊢
¬
A
\frac {\Gamma;A\vdash B;\Gamma;A\vdash\neg B} {\Gamma\vdash \neg A}
Γ
⊢
¬
A
Γ
;
A
⊢
B
;
Γ
;
A
⊢
¬
B
，反证法是也
→
\rightarrow
→
消除：
Γ
⊢
A
;
Γ
;
A
⊢
B
Γ
⊢
B
\frac {\Gamma\vdash A;\Gamma;A\vdash B} {\Gamma\vdash B}
Γ
⊢
B
Γ
⊢
A
;
Γ
;
A
⊢
B
，即PC中分离规则
→
\rightarrow
→
引入：
Γ
;
A
⊢
B
Γ
⊢
A
→
B
\frac {\Gamma;A\vdash B} {\Gamma\vdash A\rightarrow B}
Γ
⊢
A
→
B
Γ
;
A
⊢
B
，即PC中演绎定理
∧
\land
∧
消除：
Γ
⊢
A
∧
B
Γ
⊢
A
,
Γ
⊢
A
∧
B
Γ
⊢
B
\frac {\Gamma\vdash A\land B} {\Gamma\vdash A},\frac {\Gamma\vdash A\land B} {\Gamma\vdash B}
Γ
⊢
A
Γ
⊢
A
∧
B
,
Γ
⊢
B
Γ
⊢
A
∧
B
，源于重言式
A
∧
B
→
A
,
A
∧
B
→
B
A\land B\rightarrow A,A\land B\rightarrow B
A
∧
B
→
A
,
A
∧
B
→
B
∧
\land
∧
引入：
Γ
⊢
A
;
Γ
⊢
B
Γ
⊢
A
∧
B
\frac {\Gamma\vdash A;\Gamma\vdash B} {\Gamma\vdash A\land B}
Γ
⊢
A
∧
B
Γ
⊢
A
;
Γ
⊢
B
，源于重言式
A
→
B
→
(
A
∧
B
)
A\rightarrow B\rightarrow(A\land B)
A
→
B
→
(
A
∧
B
)
∨
\vee
∨
消除：
Γ
;
A
⊢
C
;
Γ
;
B
⊢
C
;
Γ
⊢
A
∨
B
Γ
⊢
C
\frac {\Gamma;A\vdash C;\Gamma;B\vdash C;\Gamma\vdash A\vee B} {\Gamma\vdash C}
Γ
⊢
C
Γ
;
A
⊢
C
;
Γ
;
B
⊢
C
;
Γ
⊢
A
∨
B
，源于重言式
(
A
→
C
)
∧
(
B
→
C
)
∧
(
A
∨
B
→
C
)
(A\rightarrow C)\land(B\rightarrow C)\land(A\vee B\rightarrow C)
(
A
→
C
)
∧
(
B
→
C
)
∧
(
A
∨
B
→
C
)
∨
\vee
∨
引入：
Γ
⊢
A
Γ
⊢
A
∨
B
,
Γ
⊢
A
Γ
⊢
B
∨
A
\frac {\Gamma\vdash A} {\Gamma\vdash A\vee B},\frac {\Gamma\vdash A} {\Gamma\vdash B\vee A}
Γ
⊢
A
∨
B
Γ
⊢
A
,
Γ
⊢
B
∨
A
Γ
⊢
A
，源于重言式
A
→
A
∨
B
,
A
→
B
∨
A
A\rightarrow A\vee B,A\rightarrow B\vee A
A
→
A
∨
B
,
A
→
B
∨
A
假设消除：
Γ
;
A
⊢
B
;
Γ
;
¬
A
⊢
B
Γ
⊢
B
\frac {\Gamma;A\vdash B ; \Gamma;\neg A\vdash B}{\Gamma\vdash B}
Γ
⊢
B
Γ
;
A
⊢
B
;
Γ
;
¬
A
⊢
B
假设引入：
Γ
⊢
B
Γ
;
A
⊢
B
\frac {\Gamma\vdash B} {\Gamma;A\vdash B}
Γ
;
A
⊢
B
Γ
⊢
B
，源于重言式
A
→
(
B
→
A
)
A\rightarrow(B\rightarrow A)
A
→
(
B
→
A
)
ND的推理规则围绕5个联结词展开，共14个
A
⊢
B
A\vdash B
A
⊢
B
且
B
⊢
A
B\vdash A
B
⊢
A
，记作
A
⊢
⊣
B
A\vdash\dashv B
A
⊢⊣
B
，称A和B演绎等价
若
Γ
=
{
B
}
\Gamma=\left\{B\right\}
Γ
=
{
B
}
，
Γ
⊢
A
\Gamma\vdash A
Γ
⊢
A
简记为
B
⊢
A
B \vdash A
B
⊢
A
记为
Γ
⊢
A
\Gamma\vdash A
Γ
⊢
A
，称
A
A
A
为
Γ
\Gamma
Γ
的演绎结果
∀
i
=
1
,
⋯
,
m
−
1
\forall i=1,\cdots,m-1
∀
i
=
1
,
⋯
,
m
−
1
，
A
i
A_i
A
i
为
Γ
\Gamma
Γ
中公式或PC中公理或
A
j
,
A
k
A_j,A_k
A
j
,
A
k
使用
r
m
p
r_{mp}
r
m
p
导出公式
称
A
1
,
⋯
,
A
m
(
=
A
)
A_1,\cdots,A_m(=A)
A
1
,
⋯
,
A
m
(
=
A
)
为
A
A
A
以
Γ
\Gamma
Γ
为前提的演绎
Γ
\Gamma
Γ
为PC中部分公式之集
Σ
=
{
(
,
)
,
¬
,
→
,
p
1
,
⋯
,
p
n
}
\Sigma=\left\{(,),\neg,\rightarrow,p_1,\cdots,p_n\right\}
Σ
=
{
(
,
)
,
¬
,
→
,
p
1
,
⋯
,
p
n
}
辅助符号：圆括号()
联结词完备集
{
→
,
¬
}
\left\{ \rightarrow,\neg\right\}
{
→
,
¬
}
原子变元符
p
1
,
⋯
,
p
n
,
⋯
p_1,\cdots,p_n,\cdots
p
1
,
⋯
,
p
n
,
⋯
用分配律展开，化简
对仅有部分变元的项进行补齐（合取项添加永假式，析取项添加永真式）
合并相同的合取/析取项或变元
除去其中所有永真/永假的项
求解命题公式
A
(
p
1
,
⋯
,
p
n
)
A(p_1,\cdots,p_n)
A
(
p
1
,
⋯
,
p
n
)
的合取/析取范式
∨
i
=
1
2
n
m
i
=
T
\vee_{i=1}^{2^n} m_i = T
∨
i
=
1
2
n
m
i
=
T
任两不相同的极小项不同时为真
每个极小项有
2
n
2^n
2
n
种真值指派，其中为真的仅一种
命题公式
A
(
p
1
,
⋯
,
p
n
)
A(p_1,\cdots,p_n)
A
(
p
1
,
⋯
,
p
n
)
有
2
n
2^n
2
n
个极小项
A
j
=
Q
1
∨
Q
2
∨
⋯
∨
Q
n
A_j = Q_1\vee Q_2\vee\cdots\vee Q_n
A
j
=
Q
1
∨
Q
2
∨
⋯
∨
Q
n
称极小项
∀
1
⩽
i
⩽
n
,
Q
i
=
p
i
\forall 1\leqslant i\leqslant n,Q_i=p_i
∀1
⩽
i
⩽
n
,
Q
i
=
p
i
或
¬
p
i
\neg p_i
¬
p
i
∀
1
⩽
j
⩽
k
,
A
j
=
Q
1
∨
Q
2
∨
⋯
∨
Q
n
\forall 1\leqslant j \leqslant k,A_j = Q_1\vee Q_2\vee\cdots\vee Q_n
∀1
⩽
j
⩽
k
,
A
j
=
Q
1
∨
Q
2
∨
⋯
∨
Q
n
A
(
p
1
,
⋯
,
p
n
)
=
A
1
∧
A
2
∧
⋯
∧
A
k
(
k
⩾
1
)
A(p_1,\cdots,p_n)=A_1 \land A_2 \land \cdots \land A_k (k\geqslant 1)
A
(
p
1
,
⋯
,
p
n
)
=
A
1
∧
A
2
∧
⋯
∧
A
k
(
k
⩾
1
)
析取项
合取项
任一命题A都存在与之等价的合取范式/析取范式
析取范式
合取范式
内否式
对偶式
可满足式
矛盾式（永假式）
重言式（永真式）
定义：对公式
A
(
p
1
,
⋯
,
p
n
)
A(p_1,\cdots,p_n)
A
(
p
1
,
⋯
,
p
n
)
的任一种真值赋值
复合命题
单个命题变元
单个命题常元
有限次使用上述过程，均为命题公式
两命题公式经任一逻辑联结词形成的也是命题公式
原子命题是命题公式
归约
扩充
等价
↔
\leftrightarrow
↔
蕴涵
→
\rightarrow
→
否定
¬
\neg
¬
析取
∨
\vee
∨
合取
∧
\land
∧
FND
FCM
完备性：
∀
B
∈
Γ
,
(
⊨
T
B
)
⇒
(
Γ
⊢
F
C
B
)
\forall B\in\Gamma,(\models_T B)\Rightarrow(\Gamma\vdash_{FC}B)
∀
B
∈
Γ
,
(
⊨
T
B
)
⇒
(
Γ
⊢
FC
B
)
不一致扩充必定完全
不完全性：
∃
A
∈
Γ
,
(
⊢
A
)
∨
(
⊢
¬
A
)
=
0
\exists A\in\Gamma,(\vdash A)\vee(\vdash\neg A)=0
∃
A
∈
Γ
,
(
⊢
A
)
∨
(
⊢
¬
A
)
=
0
一致性：
∀
A
∈
Γ
,
(
⊢
A
)
∧
(
⊢
¬
A
)
=
0
\forall A\in\Gamma,(\vdash A)\land(\vdash\neg A)=0
∀
A
∈
Γ
,
(
⊢
A
)
∧
(
⊢
¬
A
)
=
0
A
A
A
为
F
C
FC
FC
公式，
(
Γ
⊢
F
C
A
)
⇒
(
Γ
⊨
T
A
)
(\Gamma\vdash_{FC}A)\Rightarrow(\Gamma\models_T A)
(
Γ
⊢
FC
A
)
⇒
(
Γ
⊨
T
A
)
.
合理性：
∀
A
∈
Γ
\forall A\in\Gamma
∀
A
∈
Γ
，若
⊢
F
C
A
\vdash_{FC}A
⊢
FC
A
，则
⊨
T
A
\models_TA
⊨
T
A
.
说明：
看我干什么？看书！
最终目的：通过对演算系统的研究，给出正确的逻辑推理形式及其规律
一阶语言中的个体词、谓词、函词、项等，均完全基于形式考虑，仅为字符串处理，未考虑语义
看我干什么？看书！
补充
补充/记忆
内容
个体变元、个体常元、n元函词、n元谓词、真值联结词
(
¬
,
→
)
(\neg,\rightarrow)
(
¬
,
→
)
、量词、技术性括号等，分别如上所规定
最终构成合式公式
使用量词、函词、逻辑联结词
谓词分解为原子谓词，规定谓词符号
全称化
代入
可代入
易名规则
变元
合式公式
项（递归定义）
量词
函词
个体域
谓词
个体词
原理
无法体现研究对象特性及研究对象间逻辑关系
对原子命题内部结构不进行分析
命题逻辑把原子命题看作不可再分的基本单位
推理能力不足，如无法推理三段论内容
含有变元的判断难以处理
抽象性问题，知识表达能力不足
演绎
特点
规则内容
说明
Γ
;
A
⊢
A
\Gamma;A\vdash A
Γ
;
A
⊢
A
T
h
(
P
C
⋃
Γ
)
=
{
A
∣
Γ
⊢
P
C
A
}
Th(PC\bigcup\Gamma)=\left\{A|\Gamma\vdash_{PC}A\right\}
T
h
(
PC
⋃
Γ
)
=
{
A
∣Γ
⊢
PC
A
}
T
h
(
P
C
)
=
{
A
∣
⊢
P
C
A
}
Th(PC)=\left\{A|\vdash_{PC} A\right\}
T
h
(
PC
)
=
{
A
∣
⊢
PC
A
}
∃
A
(
(
⊢
A
=
0
)
∧
(
⊢
¬
A
=
0
)
)
\exists A((\vdash A=0)\land(\vdash \neg A=0))
∃
A
((
⊢
A
=
0
)
∧
(
⊢
¬
A
=
0
))
∀
A
(
(
⊢
A
)
∧
(
⊢
(
¬
A
)
)
=
0
)
\forall A((\vdash A)\land(\vdash(\neg A))=0)
∀
A
((
⊢
A
)
∧
(
⊢
(
¬
A
))
=
0
)
∀
⊢
A
\forall \vdash A
∀
⊢
A
，
A
A
A
永真
补充
定义
A为PC中定理，记为
⊢
p
c
A
\vdash_{pc}A
⊢
p
c
A
A
i
(
i
=
1
,
⋯
,
m
−
1
)
A_i(i=1,\cdots,m-1)
A
i
(
i
=
1
,
⋯
,
m
−
1
)
或为公理，或为
A
j
(
j
<
i
)
A_j(j<i)
A
j
(
j
<
i
)
，或为
A
j
,
A
k
(
j
,
k
<
i
)
A_j,A_k(j,k< i)
A
j
,
A
k
(
j
,
k
<
i
)
使用
r
m
p
r_{mp}
r
m
p
导出公式
称
A
1
,
⋯
,
A
m
(
=
A
)
A_1,\cdots,A_m(=A)
A
1
,
⋯
,
A
m
(
=
A
)
为公式A在PC中的一个证明
推理序列：
A
,
A
→
B
,
B
A,A\rightarrow B,B
A
,
A
→
B
,
B
若
A
A
A
及
A
→
B
A\rightarrow B
A
→
B
均成立，则B成立
A
3
:
(
¬
A
→
¬
B
)
→
(
B
→
A
)
A_3:(\neg A\rightarrow\neg B)\rightarrow(B\rightarrow A)
A
3
:
(
¬
A
→
¬
B
)
→
(
B
→
A
)
A
2
:
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
A_2:(A\rightarrow (B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))
A
2
:
(
A
→
(
B
→
C
))
→
((
A
→
B
)
→
(
A
→
C
))
A
1
:
A
→
(
B
→
A
)
A_1:A\rightarrow(B\rightarrow A)
A
1
:
A
→
(
B
→
A
)
命题公式
用符号表示
构成元素
求解过程
极小项
主析取范式
主合取范式
范式定理
原理：替换原理
替换原理
代入原理
定义：若
A
⇒
B
A \Rightarrow B
A
⇒
B
且
B
⇒
A
B \Rightarrow A
B
⇒
A
，则
A
⇔
B
A\Leftrightarrow B
A
⇔
B
定义：若任一弄真公式A的指派亦必弄真公式B，称A逻辑蕴涵B，记作
A
⇒
B
A \Rightarrow B
A
⇒
B
特殊命题公式
指派
类型
递归定义
联结词的扩充与归约
常见
命题变元
复合命题
原子命题
定义：具有唯一真值的陈述句
其他形式FC
FC性质定理
语义
定理
推理规则
公理
组成
自然语句的形式化
基本概念
根源
缺陷
基本定理
推理规则
公理
PC基于
Γ
\Gamma
Γ
的扩充
PC的理论
不完全性
一致性
合理性
看我干什么？看书！
演绎
定理
证明（证明序列）
推理:分离规则(
r
m
p
r_{mp}
r
m
p
)
公理
形成规则
字符集
主范式
类型
原理
逻辑等价
逻辑蕴涵
命题公式
真值表
联结词
命题种类
一阶谓词演算形式系统(FC)
一阶谓词演算
命题逻辑的不足
组成
其他
PC的性质定理
PC定理
PC基本定理
PC组成
范式
逻辑关系
命题
一阶谓词演算(FC)
自然演绎推理系统(ND)
命题演算形式系统(PC)
命题逻辑
数理逻辑
2022.12
一起来讨论吧！
留下邮箱，接收后续评论喔~
