シェファー・ストローク

Sheffer stroke

1913年、Henry Maurice Shefferが
￢(否定。「～でない」にあたる)、∨(論理和。「～または～」にあたる)、∧(論理積。「～かつ～」にあたる)、→(含意。「～ならば～」にあたる)以外に導入した
古典命題論理の論理結合子|(二者択一否定。￢(A∧B)に同じで、「～であることと～であることは両立しない」にあたる)のこと。

否定、論理和、論理積、含意は次のように、
￢AはA|A
A∨Bは(A|A)|(B|B)
A∧Bは(A|B)|(A|B)
A→BはA|(B|B)
と定義可能でそれぞれSheffer strokeのみで表現することができ、
以下のひとつの公理と

((U|(V|W))|((Y|(Y|Y))|((X|V)|((U|X)|(U|X)))))

下記の推論規則だけからなる

(U|(V|W)), U├W

Hilbert流の古典命題論理の形式システムも知られている。


http://en.wikipedia.org/wiki/...
http://people.cohums.ohio-state.edu/...