| 希尔伯特-贝尔奈斯系统 Hilbert-Bernays system 简称“HB系统”。把关于五个基本联结词的公理同时列出的系统。在希尔伯特与贝尔奈斯合著的《数学基础》中给出。其公理为：
(1) 蕴涵公理：
1. p→(q→p)
2. (p→(p→q))→(p→q)
3. (p→q)→((q→r)→(p→r))
(2) 合取公理：
1. p∧q→p
2. p∧q→q
3. (p→q)→((p→r)→(p→q∧r))
(3) 析取公理：
1. p→p∨q
2. q→p∨q
3. (p→r)→((q→r)→(p∨q→r))
(4) 等值公理：
1. (p↔q)→(p→q)
2. (p↔q)→(q→p)
3. (p→q)→((q→p)→(p↔q))
(5) 否定公理：
1. (p→q)→(q→p)
2. p→p
3. p→p
推演规则只有代入规则和分离规则。这系统可以省去定义。 |