一次函数斜率公式布尔代数公理及其他常用逻辑运算

2020年10月11日发(作者：裴汉)
布尔代数公理及其他常用逻辑运算




在 1933 年，美国数学家 Edward Vermilye Huntington (1874-1952)
展示了对布尔代数的如下公理化：
交换律：x + y = y +
x。

结合律：(x + y) + z = x + (y + z)。

Huntington等式：n(n(x) + y) + n(n(x) + n(y)) = x。

一元函数符号 n 可以读做‘补’。

Herbert Robbins 接着摆出下列问题： Huntington等式能否缩短为
下述的等式，并且这个新 等式与结合律和交换律一起成为布尔代数的
基础? 通过一组叫做 Robbins 代数的公理，问题就变成了：是否所
有的 Robbins 代数都是布尔代数?

Robbins 代数的公理化：

交换律： x + y = y + x。

结合律： (x + y) + z = x + (y + z)。

Robbins等式： n(n(x + y’) + n(x + n(y))) = x。

这个问题自从 1930 年代一直是公开的，并成为 Alfred Tarski 和
他的学生最喜好的问题。

在 1996 年，William McCune 在 Argonne 国家实验室，建造在
Larry Wos、Steve Winker 和 Bob Veroff 的工作之上，肯定的回答
了这个长期存在的问题： 所有的 Robbins 代数都是布尔代数。这项
工作是使用 McCune 的自动推理程序 EQP 完成的。