谢费尔竖线
谢费尔竖线（英語：Sheffer stroke），得名于亨利·莫里斯·谢费尔[1]，写为“| ”（見豎線）或“↑”，指示等价于合取运算的否定的逻辑运算。普通语言表达为“不全是即真”（Not AND，因此也常縮寫為NAND），也就是说，A | B假，当且仅当A与B都真时才成立。它是可用来表达与命题逻辑有关的所有布尔函数的自足算子之一。在布尔代数和数字电子中有叫做「NAND」的等价运算。
定义
谢费尔竖线“|”等价于逻辑与的否定：
下列真值表在语义上定义了“|”：
| A | B | A | B |
|---|---|---|
| T | T | F |
| T | F | T |
| F | T | T |
| F | F | T |
其他逻辑算子可以依据"|"来定义，比如：
- 。
历史
亨利·莫里斯·谢费尔证明了命题逻辑的所有常用算子（非、与、或、蕴涵等等）都可以用它来表达（Sheffer 1913）。查尔斯·皮尔士在30多年前（1880年）就发现了这个事实。皮尔士还发现所有布尔算子都可以用NOR算子来表达。
基于谢费尔竖线的形式系统
下面是完全基于谢费尔竖线的形式系统的一个例子，它有着命题逻辑的表达能力。
符号
A B C D E F G '
( | )
谢费尔竖线符合交换律不符合结合律。所以包括谢费尔竖线的所有形式系统必须也包含某种表示组合的方式。我们将为此采用'('和')'。
文法
字母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。
公理
下列wff是公理模式，即在把所有元变量替代为wff后变为公理。
THEN-1：(U|(U|(V|(U|U))))
推理规则
等价代换。设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)) V
MP-2： U,(U|(V|X)) X
注意。公式(U|(V|X))有释义U→V∧X。肯定前件是MP-1和MP-2在V和X同一的时候的特殊情况。
简化
因为这个逻辑的唯一连结词是"|"，符号"|"可以一起都丢弃，只留下圆括号用来组合字母。一对圆括号必须总是包含一对wff。使用这种简单表示法的例子有
- (A(A(B(B((AB)(AB)))))),
- (A(A((BB)(AA)))).
明显类似于LISP的语法。
表示法可以进一步简化，通过让
- (U):=(UU)
- ((U)) U
对于任何U。这种简化导致了需要改变某些规则：（1）多于两个字母允许在圆括号内。（2）在圆括号内的字母或wff允许交换。（3）在同一组圆括号内的重复字母或wff可以除去。这个结果是Peirce的存在图的相应版本。
引用
- 查尔斯·桑德斯·皮尔士, 1880. 'A Boolean Algebra with One Constant'. In Hartshorne, C, and Weiss, P., eds.,(1931-35)Collected Papers of Charles Sanders Peirce, Vol. 4: 12-20. Harvard University Press.
- H. M. Sheffer, 1913. "A set of five independent postulates for Boolean algebras, with application to logical constants," Transactions of the American Mathematical Society 14: 481-488.
