Sheffer stroke

The truth table of ${\displaystyle P\uparrow Q}$ (also written as ${\displaystyle P\mathop {|} Q}$, or Dpq) is as follows

${\displaystyle P}$	${\displaystyle Q}$	${\displaystyle P\uparrow Q}$
T	T	F
T	F	T
F	T	T
F	F	T

The Sheffer stroke of ${\displaystyle P}$ and ${\displaystyle Q}$ is the negation of their conjunction

${\displaystyle P\uparrow Q}$	${\displaystyle \Leftrightarrow }$	${\displaystyle \neg (P\land Q)}$
	${\displaystyle \Leftrightarrow }$	${\displaystyle \neg }$

By De Morgan's Laws, this is also equivalent to the disjunction of the negations of ${\displaystyle P}$ and ${\displaystyle Q}$

${\displaystyle P\uparrow Q}$	${\displaystyle \Leftrightarrow }$	${\displaystyle \neg P}$	${\displaystyle \lor }$	${\displaystyle \neg Q}$
	${\displaystyle \Leftrightarrow }$		${\displaystyle \lor }$

p_n for natural numbers n
( | )

The Sheffer stroke commutes but does not associate (e.g., (T | T) | F = T, but T | (T | F) = F). Hence any formal system including the Sheffer stroke as an infix symbol must also include a means of indicating grouping (grouping is automatic if the stroke is used as a prefix, thus: || TTF = T and | T | TF = F). We shall employ '(' and ')' to this effect.

We also write p, q, r, … instead of p₀, p₁, p₂.

Construction Rule I: For each natural number n, the symbol p_n is a well-formed formula (wff), called an atom.

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

Closure Rule: Any formulae which cannot be constructed by means of the first two Construction Rules are not wffs.

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

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.

All wffs of the form

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

are axioms. Instances of

(U | (V | W)), U ${\displaystyle \vdash }$ W

are inference rules.

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 wffs. Examples of theorems in this simplified notation are

(p(p(q(q((pq)(pq)))))),

(p(p((qq)(pp)))).

The notation can be simplified further, by letting

(U) := (UU)

((U)) ${\displaystyle \equiv }$ 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 graphs.

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

(p(p(q(q((pq)(pq)))))) becomes

| p | p | q | q || pq | pq, and

(p(p((qq)(pp)))) becomes,

| p | p || qq | pp.

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

Or one could omit both parentheses and strokes and allow the order of the arguments to determine the order of function application so that for example, applying the function from right to left (reverse Polish notation – any other unambiguous convention based on ordering would do)

${\displaystyle {\begin{aligned}&pqr\equiv (p\mid (q\mid r)),{\text{ whereas}}\\&rqp\equiv (r\mid (q\mid p)).\end{aligned}}}$