查看“︁谢费尔竖线”︁的源代码

{{noteTA
|1=zh-tw:數位;zh-cn:数字;
}}
[[File:Venn1110.svg|thumb|[[文氏图]]<math>A | B</math>]]
{{Otheruses|other=数字电路中的与非门|与非门}}
'''谢费尔竖线'''（{{lang-en|Sheffer stroke}}），得名于{{link-en|亨利·莫里斯·谢费尔|Henry M. Sheffer}}<ref>[[张申府]]《所思》：“自余后起数理名家数美人蛇斐（Dr.H.M. Sheffer）最有成就，也久不见其新著。……友人[[俞大维]]博士，昔在美学于蛇斐。前岁在德著名的《数学纪录》杂志，曾一见其新著，精进不息，必是足为中国光的。</ref>，写为“| ”（見[[豎線]]）或“↑”，指示等价于[[逻辑合取|合取]]运算的[[否定]]的[[逻辑连结词|逻辑运算]]。普通语言表达为“'''不全是'''即真”（Not AND，因此也常縮寫為'''NAND'''），也就是说，A | B假，当且仅当A与B都真时才成立。它是可用来表达与[[命题逻辑]]有关的所有[[布尔函数]]的[[自足算子]]之一。在[[布尔代数]]和[[数字电子]]中有叫做「NAND」的等价运算。

==定义==
谢费尔竖线“|”等价于[[逻辑与]]的否定：
:<math> A | B = \neg(A \wedge B) = \overline{AB} </math>

下列真值表在语义上定义了“|”：

{| class="wikitable" style="font-family:Arial;text-align:center;"
|+
! style="width:35px;background:#aaa;" | <big>A</big>
! style="width:35px;background:#aaa;" | <big>B</big>
!style="width:70px;background:#aaa;" | <big>A | B</big>
|-
| T  || T  || F
|-
| T  || F  || T
|-
| F  || T  || T
|-
| F  || F  || T
|}

其他逻辑算子可以依据"|"来定义，比如：
:<math> \neg A = A | A, </math>
:<math> A \wedge B =(A | B) |(A | B), </math>
:<math> A \vee B =(A | A) |(B | B), </math>
:<math> A \rightarrow B = A |(B | B) = A |(A | B)</math>。

==历史==
亨利·莫里斯·谢费尔证明了[[命题逻辑]]的所有常用算子（[[否定|非]]、[[逻辑合取|与]]、[[逻辑析取|或]]、[[逻辑条件|蕴涵]]等等）都可以用它来表达（Sheffer 1913）。[[查尔斯·桑德斯·皮尔士|查尔斯·皮尔士]]在30多年前（1880年）就发现了这个事实。皮尔士还发现所有布尔算子都可以用[[逻辑或非|NOR]]算子来表达。

==基于谢费尔竖线的形式系统==
下面是完全基于谢费尔竖线的形式系统的一个例子，它有着[[命题逻辑]]的表达能力。

===符号===
A B C D E F G ' <br>
( | )

谢费尔竖线符合交换律不符合结合律。所以包括谢费尔竖线的所有形式系统必须也包含某种表示组合的方式。我们将为此采用'('和')'。

===文法===
字母A,B,C,D,E,F和G是原子。

任何字母加[[角分符號]]（Prime,  ′ ）一次或多次还是一个原子（比如A<nowiki>'</nowiki>, B<nowiki>''</nowiki>, C<nowiki>'''</nowiki>, D<nowiki>''''</nowiki>都是原子）。

构造规则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)) <br> 

'''[[弗雷格命题演算|THEN-3]]：'''(U|(U|(V|(V|X)))) =(V|(V|(U|(U|X))))

'''MP-1：''' U,(U|(V|X)) <math>\vdash</math> V 

'''MP-2：''' U,(U|(V|X)) <math>\vdash</math> 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)) <math>\equiv</math> 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.
{{reflist}}

==参见==
* [[逻辑与非]]
* [[与非门]]
* [[自足算子]]
* [[真值表]]
* [[存在图]]
* [[逻辑哲学论]]
* [[零阶逻辑]]
{{逻辑联结词}}
[[Category:布尔代数]]
[[Category:數理邏輯|X]]
[[Category:邏輯聯結詞]]