謝費爾豎線

文氏圖$A|B$

  關於數位電路中的與非門，請見「與非門」。

謝費爾豎線（英語：Sheffer stroke），得名於亨利·莫里斯·謝費爾，寫為「| 」（見豎線）或「↑」，指示等價於合取運算的否定的邏輯運算。普通語言表達為「不全是即真」（Not AND，因此也常縮寫為NAND），也就是說，A | B假，若且唯若A與B都真時才成立。它是可用來表達與命題邏輯有關的所有布爾函數的自足算子之一。在布爾代數和數位電子中有叫做「NAND」的等價運算。

定義

謝費爾豎線「|」等價於邏輯與的否定：

$A|B=\neg (A\wedge B)={\overline {AB}}$

下列真值表在語義上定義了「|」：

A	B	A | B
T	T	F
T	F	T
F	T	T
F	F	T

其他邏輯算子可以依據"|"來定義，比如：

$\neg A=A|A,$

$A\wedge B=(A|B)|(A|B),$

$A\vee B=(A|A)|(B|B),$

$A\rightarrow B=A|(B|B)=A|(A|B)$。

歷史

亨利·莫里斯·謝費爾證明了命題邏輯的所有常用算子（非、與、或、蘊涵等等）都可以用它來表達（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)) $\vdash$ V

MP-2： U,(U|(V|X)) $\vdash$ 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)) $\equiv$ 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.

參見

• 邏輯與非
• 與非門
• 自足算子
• 真值表
• 存在圖
• 邏輯哲學論
• 零階邏輯