Sheffer竖线
维库,知识与思想的自由文库
NAND逻辑门
Sheffer竖线,写为“|”或“↑”,指示等价于合取运算的否定的逻辑运算,普通语言表达为“不全是即真”。在布尔代数和数字电子中它叫做NAND(与非)运算。它是可用来表达与命题逻辑有关的所有布尔函数的自足算子之一。 它得名于Henry M. Sheffer,他证明了(Sheffer 1913)命题逻辑的所有常用算子(非、与、或、蕴涵等等)都可以用它来表达。查尔斯·皮尔士(1880)在30多年前就发现了这个事实。皮尔士还发现所有布尔算子都可以用NOR算子来表达。
[编辑] Sheffer竖线Sheffer竖线"|"等价于合取的否定: 下列真值表在语义上定义了"|":
其他逻辑算子可以依据"|"来定义,比如: [编辑] 基于Sheffer竖线的形式系统下面是完全基于Sheffer竖线的形式系统的一个例子,它有着命题逻辑的表达能力。 [编辑] 1. 符号A B C D E F G ' Sheffer 竖线符合交换律不符合结合律。所以包括Sheffer竖线的所有形式系统必须也包含某种表示组合的方式。我们将为此采用 '(' 和 ')'。 [编辑] 2. 文法字母 A,B,C,D,E,F和G是原子。 任何字母加撇(prime)一次或多次还是一个原子(比如 A', B′′, C′′′, D′′′′ 都是原子)。 构造规则I:原子是合式公式(wff)。 构造规则II:如果X和Y是wff,则(X|Y)是wff。 闭包规则:不能使用前两个构造规则构造的任何公式都不是wff。 字母U,V,X和Y是表示wff的元变量。 确定一个公式是否是合式公式的一个判定过程如下: 反向应用构造规则"解构"这个公式,把这个公式分解为更小的子公式。接着对每个子公式重复这个递归的解构过程。最终这个公式被简约到它的原子,如果某个子公式不能被简约,则这个公式不是 wff。 [编辑] 3. 公理下列wff是公理模式,即在把所有元变量替代为wff后变为公理。 THEN-1:(U|(U|(V|(U|U)))) [编辑] 4. 推理规则等价代换。设wff X包含子公式U的一个或多个实例。如果U=V,则把X中U的一个或多个实例替换为V不改变X的真值。特别是,如果X=Y是个定理,则在V对U的任何代换之后仍是这种情况。 交换律: (X|Y) = (Y|X) 对偶律: 如果形如 X 和 (X|X) 的字符串都出现在一个定理中,则如果对换这两个字符串在这个定理中的所有出现,则结果也是个定理。 双重否定律: ((X|X)|(X|X)) = X 模仿律: (U|(X|X)) = (U|(U|X)) THEN-3: (U|(U|(V|(V|X)))) = (V|(V|(U|(U|X)))) MP-1: U, (U|(V|X)) MP-2: U, (U|(V|X)) 注意。公式 (U|(V|X)) 有释义U→V∧X。肯定前件是MP-1和MP-2在V和X同一的时候的特殊情况。 [编辑] 简化因为这个逻辑的唯一连结词是"|",符号"|"可以一起都丢弃,只留下圆括号用来组合字母。一对圆括号必须总是包含一对 wff。使用这种简单表示法的例子有
明显类似于LISP的语法。 表示法可以进一步简化,通过让
对于任何 U。这种简化导致了需要改变某些规则: (1) 多于两个字母允许在圆括号内。(2) 在圆括号内的字母或 wff 允许交换。(3) 在同一组圆括号内的重复字母或 wff 可以除去。这个结果是 Peirce 的存在图的相应版本。 [编辑] 引用
[编辑] 参见 |







V
U
