Sheffer stroke: Difference between revisions

Revision as of 20:30, 19 October 2007

Latest revision as of 06:57, 11 July 2025

(395 intermediate revisions by more than 100 users not shown)

Line 1:

{{short description|Logical operation}}

{| class="wikitable" align=right

{{use dmy dates|date=May 2023|cs1-dates=y}}

|- bgcolor="#ddeeff" align="center"

{{use list-defined references|date=May 2023}}

|colspan=2|'''INPUT''' || '''OUTPUT'''

{{Infobox logical connective

|- bgcolor="#ddeeff" align="center"

| title = Sheffer stroke

| A || B || A NAND B

| other titles = NAND

|- bgcolor="#ddffdd" align="center"

| wikifunction = Z10243

|0 || 0 || 1

| Venn diagram = Venn1110.svg

|- bgcolor="#ddffdd" align="center"

| definition = <math>\overline{x \cdot y}</math>

|0 || 1 || 1

| truth table = <math>(0111)</math>

|- bgcolor="#ddffdd" align="center"

| logic gate = NAND_ANSI.svg

|1 || 0 || 1

| DNF = <math>\overline{x} + \overline{y}</math>

|- bgcolor="#ddffdd" align="center"

| CNF = <math>\overline{x} + \overline{y}</math>

|1 || 1 || 0

| Zhegalkin = <math>1 \oplus xy</math>

|}

| 0-preserving = no

| 1-preserving = no

| monotone = no

| affine = no

| self-dual = no

}}

{{Logical connectives sidebar}}

The '''Sheffer stroke''', written "|" or "&uarr;", in the subject matter ofIn [[booleanBoolean function|boolean functions]],s and [[propositional calculus]], [[sententialthe calculus]],'''Sheffer or [[zeroth order logic]]stroke''' denotes a [[logical operation]] that is equivalent to the [[logical negation|negation]] of the [[logical conjunction|conjunction]] operation, expressed in ordinary language as "not both". It is also called the'''non-conjunction''', '''alternative denial''', (since it says in effect that at least one of its operands is false), or '''NAND''' ("not and").<ref name=":13">{{Cite Inbook [[Boolean|last=Howson algebra|first=Colin |title=Logic with trees: an introduction to symbolic (logic) |Booleandate=1997 algebra]]|publisher=Routledge and|isbn=978-0-415-13342-5 |___location=London; New York |pages=43}}</ref> In [[digital electronics]], it corresponds to the [[NAND gate]]. It is knownnamed after [[Henry Maurice Sheffer]] and written as the<math>\mid</math> '''NANDor operation'''as <math>\uparrow</math> or as <math>\overline{\wedge}</math> or as <math>Dpq</math> in [[Polish notation]] by [[Jan Łukasiewicz|Łukasiewicz]] ("but not and"as ||, often used to represent [[logical disjunction|disjunction]]).

Its [[duality (mathematics)|dual]] is the [[logical NOR|NOR operator]] (also known as the [[Peirce arrow]], [[Quine dagger]] or [[Webb operator]]). Like its dual, NAND can be used by itself, without any other logical operator, to constitute a logical [[formal system]] (making NAND [[functionally complete]]). This property makes the [[NAND gate]] crucial to modern [[digital electronics]], including its use in [[computer processor]] design.

Like '''[[Logical NOR|NOR]]''' alone, it is one of the two [[sole sufficient operator|sole sufficient operators]] or [[Functional completeness|functionally complete]] binary operators which can be used to express all of the [[boolean function|boolean functions]] of propositional logic. <BR><BR>

==Definition==

The '''NAND operationnon-conjunction''' is a [[logical operation]] on two [[logical value]]s,. typically the values of two [[proposition]]s, thatIt produces a value of ''false'' if and only if both of its operands are true. In other words, itif produces a value of ''true'' if— and only if — at least one of itsthe operands[[proposition]]s is false.

===Truth table===

The [[truth table]] of '''p<math>A NAND\uparrow q''' (also written as '''p&nbsp;|&nbsp;q''' or '''p&nbsp;&uarr;&nbsp;q''')B</math> is as follows:.

{{2-ary truth table|1|1|1|0|<math>A \uparrow B</math>}}

===Logical equivalences===

{| border="1" cellpadding="1" cellspacing="0" style="text-align:center;"

The Sheffer stroke of <math>P</math> and <math>Q</math> is the negation of their conjunction

|+

! style="width:35px;background:#aaaaaa;" | p

{| style="text-align: center; border: 1px solid darkgray;"

! style="width:35px;background:#aaaaaa;" | q

! style="width:35px" | &uarr;

|-

| F || F || T

|-

| F || T || T

|-

| <math>P \uparrow Q</math>

| T || F || T

| &emsp;&emsp;<math>\Leftrightarrow</math>&emsp;&emsp;

| <math>\neg (P \land Q)</math>

|-

| [[File:Venn1110.svg|50px]]

| T || T || F

| &emsp;&emsp;<math>\Leftrightarrow</math>&emsp;&emsp;

| <math>\neg</math> [[File:Venn0001.svg|50px]]

|}

By [[De Morgan's laws]], this is also equivalent to the disjunction of the negations of <math>P</math> and <math>Q</math>

===Venn diagram===

The [[Venn Diagram]] of "A nand B" (the white area is the area covered by NAND).

{| style="text-align: center; border: 1px solid darkgray;"

[[Image:Johnston Diagram- A nand B.png|150px]]

|-

| <math>P \uparrow Q</math>

==History==

| &emsp;&emsp;<math>\Leftrightarrow</math>&emsp;&emsp;

| <math>\neg P</math>

The stroke is named for [[Henry M. Sheffer]], who proved (Sheffer 1913) that all the usual operators of [[propositional logic]] ([[negation|not]], [[logical conjunction|and]], [[logical disjunction|or]], [[logical conditional|implies]], and so on), could be expressed in terms of it. [[Charles Peirce]] (1880) had discovered this fact more than 30 years earlier, but never published his finding. Peirce also observed that all boolean operators could be defined in terms of the [[logical nor|NOR]] operator, the dual of NAND.

| <math>\lor</math>

| <math>\neg Q</math>

==Properties==

|-

| [[File:Venn1110.svg|50px]]

Nand does not possess any of the following five properties, each of which is required to be absent from at least one member of a set of [[functional completeness|functionally complete]] operators: truth-preservation, falsity-preservation, [[linear|linearity]], [[monotonic|monotonicity]], [[Duality (mathematics)|self-duality]]. An operator is truth- (falsity-) preserving if its value is truth (falsity) whenever all its arguments are truth (falsity).

| &emsp;&emsp;<math>\Leftrightarrow</math>&emsp;&emsp;

| [[File:Venn1010.svg|50px]]

==Symbol==

| <math>\lor</math>

| [[File:Venn1100.svg|50px]]

One way of expressing ''p'' NAND ''q'' is as <math>\overline{p \cdot q}</math>, where the symbol <math>\cdot</math> signifies ''AND'' and the line over the expression signifies ''not'', the logical negation of that expression.

==Natural Language/Rhetoric/Colloquial usage==

NAND is not used in everyday sentences because it exhibits an inherent inversion, which makes it confusing like a [[double negative]]. Here's an example of a sentence using:

:NAND operator: ''We will surely die if we have food '''nand''' water.''

:Common terms: ''We will surely die if we do not have both food and water.''

==Introduction, elimination, and equivalencies==

The Sheffer stroke "|" is equivalent to the negation of conjunction:

:<math> P | Q \equiv \neg (P \wedge Q)</math>

Expressed in terms of NAND, the usual operators of propositional logic are:

<table>

<tr>

<td>"not ''p''" is equivalent to "''p'' NAND ''p''"</td>

<td><math> \neg P \equiv P | P, </math></td>

</tr>

<tr>

<td>"''p'' and ''q''" is equivalent to "(''p'' NAND ''q'') NAND (''p'' NAND ''q'')"</td>

<td><math> P \wedge Q \equiv (P | Q) | (P | Q), </math></td>

</tr>

<tr>

<td>"''p'' or ''q''" is equivalent to "(''p'' NAND ''p'') NAND (''q'' NAND ''q'')"</td>

<td><math> P \vee Q \equiv (P | P) | (Q | Q), </math></td>

</tr>

<tr>

<td>"''p'' implies ''q''" is equivalent to "(''p'' NAND ''q'') NAND ''p''"</td>

<td><math> P \rightarrow Q \equiv P | (Q | Q) \equiv P | (P | Q)</math></td>

</tr>

</table>

==NAND gate==

{| class="wikitable" align=left

|- bgcolor="#ddeeff" align="center"

|colspan=2|'''INPUT'''<br>A &nbsp; B || '''OUTPUT'''<br> A NAND B

|- bgcolor="#ddffdd" align="center"

|0 || 0 || 1

|- bgcolor="#ddffdd" align="center"

|0 || 1 || 1

|- bgcolor="#ddffdd" align="center"

|1 || 0 || 1

|- bgcolor="#ddffdd" align="center"

|1 || 1 || 0

|}

==Alternative notations and names==

[[Image:NandFullAdder.png|thumb|right|300px|NAND [[Full adder]]]]

[[Charles Sanders Peirce|Peirce]] was the first to show the functional completeness of non-conjunction (representing this as <math>\overline{\curlywedge}</math>) but didn't publish his result.<ref name="peirce1880">{{cite encyclopedia |last1=Peirce |first1=C. S. |title=A Boolian Algebra with One Constant |encyclopedia=Collected Papers of Charles Sanders Peirce, Volume IV The Simplest Mathematics |editor1-last=Hartshorne |editor1-first=C. |editor2-last=Weiss |editor2-first=P. |orig-date=1880 |date=1933 |pages=13–18 |___location=Massachusetts |publisher=Harvard University Press}}</ref><ref name="peirce1902">{{cite encyclopedia |last1=Peirce |first1=C. S. |title=The Simplest Mathematics |encyclopedia=Collected Papers of Charles Sanders Peirce, Volume IV The Simplest Mathematics |editor1-last=Hartshorne |editor1-first=C. |editor2-last=Weiss |editor2-first=P. |orig-date=1902 |date=1933 |pages=189–262 |___location=Massachusetts |publisher=Harvard University Press}}</ref> Peirce's editor added <math>\overline{\curlywedge}</math>) for non-disjunction.<ref name="peirce1902"/>

In 1911, {{ill|Stamm|pl|Edward Bronisław Stamm}} was the first to publish a proof of the completeness of non-conjunction, representing this with <math>\sim</math> (the '''Stamm hook''')<ref name="zach2023">{{cite web |last1=Zach |first1=R. |title=Sheffer stroke before Sheffer: Edward Stamm |url=https://richardzach.org/2023/02/sheffer-stroke-before-sheffer-edward-stamm/ |date=18 February 2023|access-date=2 July 2023}}</ref> and non-disjunction in print at the first time and showed their functional completeness.<ref name="Stamm_1911"/>

The '''NAND gate''' is a digital [[logic gate]] that behaves in a manner that corresponds to the truth table to the left. A LOW output results only if both the inputs to the gate are HIGH. If one or both inputs are LOW, a HIGH output results.The nand gate is a universal gate in the sense that any boolean function can be implemented by nand gates.

In 1913, [[Henry Maurice Sheffer|Sheffer]] described non-disjunction using <math>\mid</math> and showed its functional completeness. Sheffer also used <math>\wedge</math> for non-disjunction.<ref name="zach2023" /> Many people, beginning with [[Jean Nicod|Nicod]] in 1917, and followed by [[Alfred North Whitehead|Whitehead]], [[Bertrand Russell|Russell]] and many others{{Who|date=May 2025}}, mistakenly thought Sheffer had described non-conjunction using <math>\mid</math>, naming this symbol the Sheffer stroke.{{Citation needed|date=May 2025}}

In 1928, [[David Hilbert|Hilbert]] and [[Wilhelm Ackermann|Ackermann]] described non-conjunction with the operator <math>/</math>.<ref name="hilbert-ackermann1928">{{cite book |last1=Hilbert |first1=D. |last2=Ackermann |first2=W. |title=Grundzügen der theoretischen Logik |edition=1 |date=1928 |publisher=Verlag von Julius Springer |___location=Berlin |page=9 |language=German}}</ref><ref name="hilbert-ackermann1950">{{cite book |last1=Hilbert |first1=D. |last2=Ackermann |first2=W. |editor1-last=Luce |editor1-first=R. E. |translator1-last=Hammond |translator1-first=L. M. |translator2-last=Leckie |translator2-first=G. G. |translator3-last=Steinhardt |translator3-first=F. |title=Principles of Mathematical Logic |date=1950 |publisher=Chelsea Publishing Company |___location=New York |page=11}}</ref>

In 1929, [[Jan Łukasiewicz|Łukasiewicz]] used <math>D</math> in <math>Dpq</math> for non-conjunction in his [[Polish notation]].<ref name="lukasiewicz1929">{{cite book |last1=Łukasiewicz |first1=J. |title=Elementy logiki matematycznej |orig-date=1929|date=1958 |___location=Warszawa |publisher=Państwowe Wydawnictwo Naukowe |edition=2 |language=Polish}}</ref>

Digital systems employing certain logic circuits take advantage of NAND's functional completeness. In complicated logical expressions, normally written in terms of other logic functions such as [[logical conjunction|AND]], [[logical disjunction|OR]], and [[negation|NOT]], writing these in terms of NAND saves on cost, because implementing such circuits using NAND gate yields a more compact result than the alternatives.

An alternative notation for non-conjunction is <math>\uparrow</math>. It is not clear who first introduced this notation, although the corresponding <math>\downarrow</math> for non-disjunction was used by Quine in 1940.<ref name="quine1940">{{cite book |last1=Quine |first1=W. V |title=Mathematical Logic |date=1981 |orig-date=1940 |publisher=Harvard University Press |___location=Cambridge, London, New York, New Rochelle, Melbourne and Sydney |edition=Revised |page=45}}</ref>

=== Symbols ===

There are two symbols for NAND gates: the 'military' symbol and the 'rectangular' symbol. For more information see [[logic gate#Symbols|logic gate symbols]].

==History==

[[Image:Nand-gate-en.svg|thumb|128px|left|'Military' NAND symbol]]

The stroke is named after [[Henry Maurice Sheffer]], who in 1913 published a paper in the ''[[Transactions of the American Mathematical Society]]''<ref name="Sheffer_1913"/> providing an axiomatization of [[Boolean algebra (structure)|Boolean algebra]]s using the stroke, and proved its equivalence to a standard formulation thereof by [[Edward Vermilye Huntington|Huntington]] employing the familiar operators of [[propositional logic]] ([[logical conjunction|AND]], [[logical disjunction|OR]], [[negation|NOT]]). Because of self-[[duality (order theory)|duality]] of Boolean algebras, Sheffer's axioms are equally valid for either of the NAND or NOR operations in place of the stroke. Sheffer interpreted the stroke as a sign for nondisjunction ([[logical NOR|NOR]]) in his paper, mentioning non-conjunction only in a footnote and without a special sign for it. It was [[Jean Nicod]] who first used the stroke as a sign for non-conjunction (NAND) in a paper of 1917 and which has since become current practice.<ref name="Nicod_1917"/><ref name="Church_1956"/> Russell and Whitehead used the Sheffer stroke in the 1927 second edition of ''[[Principia Mathematica]]'' and suggested it as a replacement for the "OR" and "NOT" operations of the first edition.

[[Image:IEC NAND.svg|frame|left|'Rectangular' NAND symbol]]

{{clear}}

[[Charles Sanders Peirce]] (1880) had discovered the [[functional completeness]] of NAND or NOR more than 30 years earlier, using the term ''[[ampheck]]'' (for 'cutting both ways'), but he never published his finding. Two years before Sheffer, {{ill|Edward Stamm|pl|Edward Bronisław Stamm}} also described the NAND and NOR operators and showed that the other Boolean operations could be expressed by it.<ref name="Stamm_1911"/>

Hardware description and pinout ===

NAND gates are basic logic gates, and as such they are recognised in [[transistor-transistor logic|TTL]] and [[CMOS]] [[integrated circuit|IC]]s.

==Properties==

[[Image:CMOS 4011 diagram.svg|thumb|240px|right|This schematic diagram shows the arrangement of NAND gates within a standard 4011 CMOS integrated circuit.]]

==== CMOS version ====

The standard, [[4000 series]], [[CMOS]] [[integrated circuit|IC]] is the 4011, which includes four independent, two-input, NAND gates.

NAND is commutative but not associative, which means that <math>P \uparrow Q \leftrightarrow Q \uparrow P</math> but <math>(P \uparrow Q) \uparrow R \not\leftrightarrow P \uparrow (Q \uparrow R)</math>.<ref>{{Cite book |last=Rao |first=G. Shanker |url=https://books.google.com/books?id=M-5m_EdvxuIC |title=Mathematical Foundations of Computer Science |date=2006 |publisher=I. K. International Pvt Ltd |isbn=978-81-88237-49-4 |pages=21 |language=en}}</ref>

===== Availability =====

These devices are available from most semiconductor manufacturers such as [[Fairchild Semiconductor]], [[Philips]] or [[Texas Instruments]]. These are usually available in both through-hole [[Dual_in-line_package|DIL]] and [[Small-Outline Integrated Circuit|SOIC]] format. Datasheets are readily available in most [[datasheet#Datasheet Search Engines|datasheet databases]].

===Functional completeness===

The standard 2-, 3-, 4- and 8-input NAND gates are available:

The Sheffer stroke, taken by itself, is a [[Functional completeness|functionally complete]] set of connectives.<ref name=":18">{{Cite web |last=Weisstein |first=Eric W. |title=Propositional Calculus |url=https://mathworld.wolfram.com/ |access-date=2024-03-22 |website=mathworld.wolfram.com |language=en}}</ref><ref name=":2">{{Citation |last=Franks |first=Curtis |title=Propositional Logic |date=2023 |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2023/entries/logic-propositional/ |access-date=2024-03-22 |edition=Fall 2023 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri |encyclopedia=The Stanford Encyclopedia of Philosophy}}</ref> This can be seen from the fact that NAND does not possess any of the following five properties, each of which is required to be absent from, and the absence of all of which is sufficient for, at least one member of a set of [[functionally complete]] operators: truth-preservation, falsity-preservation, [[affine transformation|linearity]], [[monotonic]]ity, [[self-duality]]. (An operator is truth-preserving if its value is truth whenever all of its arguments are truth-, or falsity-preserving if its value is falsity whenever all of its arguments are falsity.)<ref>{{cite book | url=https://dokumen.pub/qdownload/the-two-valued-iterative-systems-of-mathematical-logic-am-5-volume-5-9781400882366.html | isbn=9781400882366 | doi=10.1515/9781400882366 | author=Emil Leon Post | title=The Two-Valued Iterative Systems of Mathematical Logic | ___location=Princeton | publisher=Princeton University Press | series=Annals of Mathematics studies | volume=5 | date=1941 }}</ref>

It can also be proved by first showing, with a [[truth table]], that <math>\neg A</math> is truth-functionally equivalent to <math>A \uparrow A</math>.<ref name=":132">{{Cite book |last=Howson |first=Colin |title=Logic with trees: an introduction to symbolic logic |date=1997 |publisher=Routledge |isbn=978-0-415-13342-5 |___location=London; New York |pages=41–43}}</ref> Then, since <math>A \uparrow B</math> is truth-functionally equivalent to <math>\neg (A \land B)</math>,<ref name=":132" /> and <math>A \lor B</math> is equivalent to <math>\neg(\neg A \land \neg B)</math>,<ref name=":132" /> the Sheffer stroke suffices to define the set of connectives <math>\{\land, \lor, \neg\}</math>,<ref name=":132" /> which is shown to be truth-functionally complete by the [[Disjunctive Normal Form Theorem]].<ref name=":132" />

* [[CMOS]]

** 4011: Quad 2-input NAND gate

** 4023: Triple 3-input NAND gate

** 4012: Dual 4-input NAND gate

** 4068: Mono 8-input NAND gate

* [[Transistor-transistor_logic|TTL]]

** 7400: Quad 2-input NAND gate

** 7410: Triple 3-input NAND gate

** 7420: Dual 4-input NAND gate

** 7430: Mono 8-input NAND gate

==Other Boolean operations in terms of the Sheffer stroke==

=== Implementations ===

Expressed in terms of NAND <math>\uparrow</math>, the usual operators of propositional logic are:

The NAND gate is the easiest to manufacture, and also has the property of [[functional completeness]]. That is, any other logic function (AND, OR, etc.) can be [[NAND logic|implemented]] using only NAND gates. An entire processor can be created using NAND gates alone.

{|

|-

|<!--- not --->

| [[Image:NMOS_NAND.png|thumb]]|| [[Image:TTL_npn_nand.svg|thumb|200px|TTL NAND gate]]|| [[Image:CMOS_NAND.svg|right|thumbnail|100px|[[CMOS]] NAND gate]]

{| style="text-align: center; border: 1px solid darkgray;"

|}

|-

|<math>\neg P</math>

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|<math>P</math>

|<math>\uparrow</math>

|<math>P</math>

|-

|[[File:Venn10.svg|36px]]

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|[[File:Venn01.svg|36px]]

|<math>\uparrow</math>

|[[File:Venn01.svg|36px]]

|}<!--- end not--->

|&nbsp;&nbsp;&nbsp;

==Formal system based on the Sheffer stroke==

|<!--- arrow --->

The following is an example of a [[formal system]] based entirely on the Sheffer stroke, yet having the functional expressiveness of the [[propositional logic]]:

{| style="text-align: center; border: 1px solid darkgray;"

|-

|<math>P \rightarrow Q</math>

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|<math>~P</math>

|<math>\uparrow</math>

|<math>(Q \uparrow Q)</math>

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|<math>~P</math>

|<math>\uparrow</math>

|<math>(P \uparrow Q)</math>

|-

|[[File:Venn1011.svg|50px]]

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|[[File:Venn0101.svg|50px]]

|<math>\uparrow</math>

|[[File:Venn1100.svg|50px]]

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|[[File:Venn0101.svg|50px]]

|<math>\uparrow</math>

|[[File:Venn1110.svg|50px]]

|}<!--- end arrow --->

|&nbsp;&nbsp;&nbsp;

===Symbols===

|<!--- bi-arrow/equivalence --->

A B C D E F G ' <br>

{| style="text-align: center; border: 1px solid darkgray;"

( | )

|-

|<math>P \leftrightarrow Q</math>

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|<math>(P \uparrow Q)</math>

|<math>\uparrow</math>

|<math>((P \uparrow P) \uparrow (Q \uparrow Q))</math>

|-

|[[File:Venn1001.svg|50px]]

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|[[File:Venn1110.svg|50px]]

|<math>\uparrow</math>

|[[File:Venn0111.svg|50px]]

|}<!--- end bi-arrow/equivalence --->

|-

The Sheffer stroke commutes but does not associate. Hence any formal system including the Sheffer stroke must also include a means of indicating grouping. We shall employ '(' and ')' to this effect.

|&nbsp;

|-

===Syntax===

|<!--- and --->

The letters A, B, C, D, E, F and G are atoms. <br>

{| style="text-align: center; border: 1px solid darkgray;"

Any of these letters primed once or several times is also an atom (e.g. A', B&prime;&prime;, C&prime;&prime;&prime;, D&prime;&prime;&prime;&prime; are atoms). <br>

|-

|<math>P \land Q</math>

''Construction Rule I:'' An atom is a well-formed formula (''wff''). <br>

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|<math>(P \uparrow Q)</math>

''Construction Rule II:'' If X and Y are wffs, then (X|Y) is a wff. <br>

|<math>\uparrow</math>

|<math>(P \uparrow Q)</math>

''Closure Rule:'' Any formulae which cannot be constructed by means of the first two Construction Rules is not a wff.

|-

|[[File:Venn0001.svg|50px]]

The letters U, V, X, and Y are metavariables standing for wffs.

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|[[File:Venn1110.svg|50px]]

A decision procedure for determining whether a formula is well-formed goes as follows: "deconstruct" the formula by applying the Construction Rules backwards, thereby breaking the formula into smaller subformulae. Then repeat this recursive deconstruction process to each of the subformulae. Eventually the formula should be reduced to its atoms, but if some subformula cannot be so reduced, then the formula is not a wff.

|<math>\uparrow</math>

|[[File:Venn1110.svg|50px]]

===Axiom===

|}<!--- end and --->

The following ''wff''s are axiom schemata, which become axioms upon replacing all metavariables with ''wff''s.

|&nbsp;&nbsp;&nbsp;

|<!--- or --->

''[[Frege's propositional calculus|THEN-1]]:'' (U|(U|(V|(U|U))))

{| style="text-align: center; border: 1px solid darkgray;"

|-

===Inference rules===

|<math>P \lor Q</math>

''Substitution of equivalents''. Let the wff X contain one more instances of the subformula U. If U=V, then replacing one or more instances of U in X by V does not alter the truth value of X. In particular, if X=Y is a theorem, this remains the case after any substitution of V for U.

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|<math>(P \uparrow P)</math>

''Commutativity:'' (X|Y) = (Y|X)<br>

|<math>\uparrow</math>

|<math>(Q \uparrow Q)</math>

''Duality:'' If strings of the forms X and (X|X) both show up in a theorem, then if these two strings are swapped wherever they appear in the theorem, then the result will also be a theorem.<br>

|-

|[[File:Venn0111.svg|50px]]

''Double Negation:'' ((X|X)|(X|X)) = X<br>

|&nbsp;&nbsp;&nbsp;&nbsp;<math>\Leftrightarrow</math>&nbsp;&nbsp;&nbsp;&nbsp;

|[[File:Venn1010.svg|50px]]

''Mimesis:'' (U|(X|X)) = (U|(U|X)) <br>

|<math>\uparrow</math>

|[[File:Venn1100.svg|50px]]

''[[Frege's propositional calculus|THEN-3]]:'' (U|(U|(V|(V|X)))) = (V|(V|(U|(U|X))))

|}<!--- end or --->

|}

''MP-1:'' U, (U|(V|X)) |- V <br>

''MP-2:'' U, (U|(V|X)) |- X <br>

Note. The formula (U|(V|X)) has the interpretation U&rarr;V&and;X. [[Modus ponens]] is the special case of MP-1 and MP-2 when V and X are identical.

===Simplification===

Since the only connective of this logic is |, the symbol | could be discarded altogether, leaving only the parentheses to group the letters. A pair of parentheses must always enclose a pair of ''wff''s. Examples of theorems in this simplified notation are

: (A(A(B(B((AB)(AB)))))),

: (A(A((BB)(AA)))).

The resemblance to the syntax of [[LISP]] is evident.

The notation can be simplified further, by letting

: (U) := (UU)

: ((U)) <math>\equiv</math> U

for any U. This simplification causes the need to change some rules: (1) more than two letters are allowed within parentheses, (2) letters or wffs within parentheses are allowed to commute, (3) repeated letters or wffs within a same set of parentheses can be eliminated. The result is a parenthetical version of the Peirce [[existential graph]]s.

Another way to simplify the notation is to eliminate parenthesis by using [[Polish Notation]]. For example, the earlier examples with only parenthesis could be rewritten using only strokes as follows

: (A(A(B(B((AB)(AB)))))) becomes

: |A|A|B|B||AB|AB, and

: (A(A((BB)(AA)))) becomes,

: |A|A||BB|AA.

This follows the same rules as the parenthesis version, with opening parenthesis replaced with a sheffer stroke and the (redundant) closing parenthesis removed.

== See also ==

{{Div col|colwidth=30em}}

<div style="-moz-column-count:2; column-count:2;">

* [[Ampheck]]

* [[AND gate]]

* [[Boolean ___domain]]

* [[CMOS]]

* [[LawsGate of Formequivalent]] (GE)

* [[Logic gate]]

* [[Logical graph]]

* [[Minimal axioms for Boolean algebra]]

* [[NOR gate]]

* NAND [[NOTflash gatememory]]

* [[ORNAND gatelogic]]

* [[Peirce's law]]

* [[Peirce arrow|Peirce arrow]] = NOR]]

* [[Propositional logic]]

* [[Sole sufficient operator]]

{{div col end}}

* [[XOR gate]]

* [[Zeroth order logic]]

</div>

==References==

{{reflist|refs=

* [[Charles 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.

<ref name="Stamm_1911">{{cite journal |author-first=Edward Bronisław |author-last=Stamm |author-link=:pl:Edward Bronisław Stamm |journal=[[Monatshefte für Mathematik und Physik]] |title=Beitrag zur Algebra der Logik |language=de |volume=22 |issue=1 |date=1911 |doi=10.1007/BF01742795 |pages=137–149|s2cid=119816758 }}</ref>

* 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.

<ref name="Sheffer_1913">{{cite journal |author-first=Henry Maurice |author-last=Sheffer |author-link=Henry Maurice Sheffer |date=1913 |title=A set of five independent postulates for Boolean algebras, with application to logical constants |journal=[[Transactions of the American Mathematical Society]] |volume=14 |issue=4 |jstor=1988701 |doi=10.2307/1988701 |doi-access=free |pages=481–488}}</ref>

<ref name="Church_1956">{{cite book |author-last=Church |author-first=Alonzo |author-link=Alonzo Church |title=Introduction to mathematical logic |volume=1 |date=1956 |publisher=[[Princeton University Press]] |page=134}}</ref>

<ref name="Nicod_1917">{{cite journal |author-last=Nicod |author-first=Jean George Pierre |author-link=Jean George Pierre Nicod |date=1917 |title=A Reduction in the Number of Primitive Propositions of Logic |journal=[[Proceedings of the Cambridge Philosophical Society]] |volume=19 |pages=32–41}}</ref>

}}

==Further reading==

== External Links ==

* {{cite book |author-first1=Józef Maria |author-last1=Bocheński |author-link1=Józef Maria Bocheński |date=1960 |title=Precis of Mathematical Logic |author-first2=Albert Heinrich |author-last2=Menne |author-link2=:de:Albert Heinrich Menne |edition=revised |translator-first=Otto |translator-last=Bird |publisher=[[D. Reidel]] |publication-place=Dordrecht, South Holland, Netherlands}} (NB. Edited and translated from the French and German editions: [[Précis de logique mathématique]])

* {{cite book |chapter=A Boolian<!-- sic! --> Algebra with One Constant |author-first=Charles Sanders |author-last=Peirce |author-link=Charles Sanders Peirce |orig-date=1880 |title=Collected Papers of Charles Sanders Peirce |title-link=Charles Sanders Peirce bibliography#CP |volume=4 |pages=12–20 |publication-place=Cambridge |publisher=[[Harvard University Press]] |editor-first1=Charles |editor-last1=Hartshorne |editor-link1=Charles Hartshorne |editor-first2=Paul |editor-last2=Weiss |editor-link2=Paul Weiss (philosopher) |date=1931–1935}}

==External links==

*http://hyperphysics.phy-astr.gsu.edu/hbase/electronic/nand.html

* [https://iep.utm.edu/sheffers/ Sheffer stroke] article in the ''[[Internet Encyclopedia of Philosophy]]''

* http://hyperphysics.phy-astr.gsu.edu/hbase/electronic/nand.html

* [http://www.sccs.swarthmore.edu/users/06/adem/engin/e77vlsi/lab3/ Implementations of 2- and 4-input NAND gates]

* [https://web.archive.org/web/20090526075041/http://projecteuclid.org/DPubS?verb=Display&version=1.0&service=UI&handle=euclid.pja/1195520940&page=record Proofs of some axioms by Stroke function by Yasuo Setô] @ [http://projecteuclid.org Project Euclid]

{{Logical Operatorsconnectives}}

{{Common logical symbols}}

[[de:NAND-Gatter]]

[[eu:EZ-ETA ate logikoa]]

[[pt:NAND]]

[[simple:NAND gate]]

[[sk:Hradlo NAND]]

[[ta:இல்-உம்மை வாயில்]]

[[zh:Sheffer竖线]]

[[Category:Logic]]

[[Category:Boolean algebra]]

[[Category:History of logic]]

[[Category:Logic gates|NAND gate]]

[[Category:Logical connectives]]

[[Category:Logic symbols]]