Editing Propositional formula (section)

== Reduced sets of connectives ==

[[File:Propositional formula NANDs.png|400px|thumb|right|The engineering symbol for the NAND connective (the 'stroke') can be used to build any propositional formula. The notion that truth (1) and falsity (0) can be defined in terms of this connective is shown in the sequence of NANDs on the left, and the derivations of the four evaluations of a NAND b are shown along the bottom. The more common method is to use the definition of the NAND from the truth table.]]

A set of logical connectives is called complete if every propositional formula is tautologically equivalent to a formula with just the connectives in that set. There are many complete sets of connectives, including <math>\{\land, \lnot\}</math>, <math>\{\lor, \lnot\}</math>, and <math>\{\to, \lnot\}</math>. There are two binary connectives that are complete on their own, corresponding to NAND and NOR, respectively.<ref>As well as the first three, Hamilton pp.19-22 discusses logics built from only | (NAND), and ↓ (NOR).</ref> Some pairs are not complete, for example <math>\{\land, \lor\}</math>.

=== The stroke (NAND) ===
The binary connective corresponding to NAND is called the [[Sheffer stroke]], and written with a vertical bar | or vertical arrow ↑. The completeness of this connective was noted in ''Principia Mathematica'' (1927:xvii). Since it is complete on its own, all other connectives can be expressed using only the stroke. For example, where the symbol " ≡ " represents ''logical equivalence'':
: ~p ≡ p|p
: p → q ≡ p|~q
: p &or; q ≡ ~p|~q
: p & q ≡ ~(p|q)
In particular, the zero-ary connectives <math>\top</math> (representing truth) and <math>\bot</math> (representing falsity) can be expressed using the stroke:
: <math>\top \equiv (a|(a|a))</math>
: <math>\bot \equiv (\top | \top)</math>

===  IF ... THEN ... ELSE ===

This connective together with { 0, 1 }, ( or { F, T } or { <math>\bot</math>, <math>\top</math> } ) forms a complete set. In the following the IF...THEN...ELSE [[Relation (mathematics)|relation]] (c, b, a) = d represents ( (c → b) &or; (~c → a) ) ≡ ( (c & b) &or; (~c & a) ) = d
: (c, b, a):
: (c, 0, 1) ≡ ~c
: (c, b, 1) ≡ (c → b)
: (c, c, a) ≡ (c &or; a)
: (c, b, c) ≡ (c & b)

Example: The following shows how a theorem-based proof of "(c, b, 1) ≡ (c → b)" would proceed, below the proof is its truth-table verification. ( Note: (c → b) is ''defined'' to be (~c &or; b) ):
:* Begin with the reduced form: ( (c & b) &or; (~c & a) )
:* Substitute "1" for a: ( (c & b) &or; (~c & 1) )
:* Identity (~c & 1) = ~c: ( (c & b) &or; (~c) )
:* Law of commutation for V:  ( (~c) &or; (c & b)  )
:* Distribute "~c V" over (c & b): ( ((~c) &or; c ) & ((~c) &or; b )
:* Law of excluded middle (((~c) &or; c ) = 1 ): ( (1) & ((~c) &or; b ) )
:* Distribute "(1) &" over ((~c) &or; b): ( ((1) & (~c)) &or; ((1) & b )) )
:* Commutivity and Identity (( 1 & ~c) = (~c & 1) = ~c, and (( 1 & b) ≡ (b & 1) ≡ b: ( ~c &or; b )
:* ( ~c &or; b ) is defined as '''c → b''' Q. E. D.

In the following truth table the column labelled "taut" for tautology evaluates logical equivalence (symbolized here by ≡) between the two columns labelled d. Because all four rows under "taut" are 1's, the equivalence indeed represents a tautology.
{|style="margin-left: auto; margin-right: auto; border: none;"
|- style="font-size:9pt; text-align:center"
| width="27.75" Height="12" | 
| width="20.25" | 
| width="18.75" | 
| width="18.75" | 
| width="6.75" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
|style="background-color:#FDE9D9" width="11.25" | d
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="12.75" | 
|style="background-color:#DDD9C3" width="19.5" | taut
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
| width="11.25" | 
|style="background-color:#FDE9D9" width="11.25" | d
| width="11.25" | 
| width="12.75" | 
| width="12.75" | 
|- style="font-size:9pt;font-weight:bold" align="center"
|style="background-color:#F2F2F2" Height="12" | rows
| c
| b
| a
|style="background-color:#A5A5A5" | 
| (
| (
| (
| c
|style="background-color:#DBE5F1" | &
| b
| )
|style="background-color:#FDE9D9" | V
| (
|style="background-color:#EAF1DD" | ~
| (
| c
| )
|style="background-color:#DBE5F1" | &
| a
| )
| )
|style="background-color:#DDD9C3" |  ≡
| (
|style="background-color:#EAF1DD" | ~
| (
| c
| )
|style="background-color:#FDE9D9" | V
| b
| )
| )
|- style="font-size:9pt" align="center"
|style="background-color:#F2F2F2" Height="12" | 0,1
| 0
| 0
| 1
|style="background-color:#A5A5A5" | 
| 
| 
| 
| 0
|style="background-color:#DBE5F1" | 0
| 0
| 
|style="background-color:#FDE9D9" | 1
| 
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
|style="background-color:#DBE5F1" | 1
| 1
| 
| 
|style="background-color:#DDD9C3" | 1
| 
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
|style="background-color:#FDE9D9" | 1
| 0
| 
| 
|- style="font-size:9pt" align="center"
|style="background-color:#F2F2F2" Height="12" | 2,3
| 0
| 1
| 1
|style="background-color:#A5A5A5" | 
| 
| 
| 
| 0
|style="background-color:#DBE5F1" | 0
| 1
| 
|style="background-color:#FDE9D9" | 1
| 
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
|style="background-color:#DBE5F1" | 1
| 1
| 
| 
|style="background-color:#DDD9C3" | 1
| 
|style="background-color:#EAF1DD" | 1
| 
| 0
| 
|style="background-color:#FDE9D9" | 1
| 1
| 
| 
|- style="font-size:9pt" align="center"
|style="background-color:#F2F2F2" Height="12" | 4,5
| 1
| 0
| 1
|style="background-color:#A5A5A5" | 
| 
| 
| 
| 1
|style="background-color:#DBE5F1" | 0
| 0
| 
|style="background-color:#FDE9D9" | 0
| 
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
|style="background-color:#DBE5F1" | 0
| 1
| 
| 
|style="background-color:#DDD9C3" | 1
| 
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
|style="background-color:#FDE9D9" | 0
| 0
| 
| 
|- style="font-size:9pt" align="center"
|style="background-color:#F2F2F2" Height="12" | 6,7
| 1
| 1
| 1
|style="background-color:#A5A5A5" | 
| 
| 
| 
| 1
|style="background-color:#DBE5F1" | 1
| 1
| 
|style="background-color:#FDE9D9" | 1
| 
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
|style="background-color:#DBE5F1" | 0
| 1
| 
| 
|style="background-color:#DDD9C3" | 1
| 
|style="background-color:#EAF1DD" | 0
| 
| 1
| 
|style="background-color:#FDE9D9" | 1
| 1
| 
| 
|}