# Assessment exercises 3 - the Sheffer stroke

This set of exercises develops a formal system for propositional logic with a single binary logical connective, $|$, known as the Sheffer stroke or NAND operation. The rules are slightly more complicated, but it is remarkable that a fully expressive propositional logic can be developed from the single symbol.

We start with a set of letters $X$ and the terms $ST ( X )$ built from $X$ with the $|$ symbol only. So each $a ∈ X$ is in $ST ( X )$ and if $α , β ∈ ST ( X )$ then so is $( α | β )$.

The following are rules of the system. (We will see shortly that a much smaller set of rules suffices, but it is convenient when learning the system to have a larger set handy.)

Given rule: if $α ∈ Σ$ then $Σ ⊢ α$.

|-Elimination rules: (|-EL) if $Σ ⊢ β$ and $Σ ⊢ ( α | β )$ then $Σ ⊢ ( α | α )$; (|-ER) if $Σ ⊢ α$ and $Σ ⊢ ( α | β )$ then $Σ ⊢ ( β | β )$.

||-Elimination rules: (||-EL) if $Σ ⊢ β$ and $Σ ⊢ ( ( α | α ) | β )$ then $Σ ⊢ α$; (||-ER) if $Σ ⊢ α$ and $Σ ⊢ ( α | ( β | β ) )$ then $Σ ⊢ β$.

|-Introduction rules: (|-IL) if $Σ , α ⊢ ( β | β )$ then $Σ ⊢ ( α | β )$; and (|-IR) if $Σ , α ⊢ ( β | β )$ then $Σ ⊢ ( β | α )$.

||-Introduction rules: (||-IL) if $Σ , α ⊢ β$ then $Σ ⊢ ( α | ( β | β ) )$; and (||-IR) if $Σ , α ⊢ β$ then $Σ ⊢ ( ( β | β ) | α )$.

Weakening rules: (WL) if $Σ ⊢ ( α | α )$ then $Σ ⊢ ( β | α )$; and (WR) if $Σ ⊢ ( α | α )$ then $Σ ⊢ ( α | β )$.

Cut rules: (|-CutL) if $Σ ⊢ ( α | ( β | β ) )$ and $Σ ⊢ ( α | β )$ then $Σ ⊢ ( α | α )$; (|-CutR) if $Σ ⊢ ( ( α | α ) | β )$ and $Σ ⊢ ( α | β )$ then $Σ ⊢ ( β | β )$. (Similar rules may be invented/discovered for Cut on the other side, or cut where the hypotheses has $( ( α | α ) | … )$ and the conclusion is $α$, etc. But the ones listed already suffice.)

Double negation rule: if $Σ ⊢ ( ( α | α ) | ( α | α ) )$ then $Σ ⊢ α$.

In the following, the Given rule should be assumed as available implicitly at all times.

Exercise 3.1.

Show that from ||-IL one can prove $( α | ( α | α ) )$ for all $α$.

Exercise 3.2.

Show that using only WL, ||-EL and |-IL one can show $α ⊢ ( ( α | α ) | ( α | α ) )$ for all $α$.

Exercise 3.3.

Use |-EL and |-IL (or |-ER and |-IR) to derive the following metarule: if $Σ ⊢ ( α | β )$ then $Σ ⊢ ( β | α )$. Deduce that given |-EL and |-IL (or |-ER and |-IR) the left version of each rule is equivalent to the right version, in the sense that if one is given the other is available as a metarule.

Exercise 3.4.

Show that the |-CutL rule is a metarule of the system with ||-ER, |-EL and |-IL.

We now show completeness and soundness theorems for the system with these rules. From now on we assume $⊢$ refers to provability using any of the rules, or equivalently using rules |-EL, ||-EL, |-IL, ||-IL, WL and the double negation rule.

Definition.

A valuation is a map $v : X → ⊤ ⊥$. Valuations are extended to arbitrary terms of $ST ( X )$ by $v ( α | β ) = v ( α ) ′ ∨ v ( β ) ′$.

Definition.

$Σ ⊨ β$ means that for all valuations $v$, if $v ( α ) = ⊤$ for all $α ∈ Σ$ then $v ( β ) = ⊤$.

Exercise 3.5.

Prove the Soundness Theorem, that $Σ ⊢ β$ implies $Σ ⊨ β$. (Using induction on the length of proofs.)

Definition.

A set $Σ$ is consistent if for no $γ$ is it the case that $Σ ⊢ γ$ and $Σ ⊢ ( γ | γ )$.

Exercise 3.6.

Use |-IL, ||-IL and a cut rule to show that if $Σ ∪ α$ is inconsistent then $Σ ⊢ ( α | α )$. Deduce that if $Σ$ is consistent and $α$ is any term in $ST ( X )$ then at least one of $Σ ∪ α$ or $Σ ∪ ( α | α )$ is consistent.

Exercise 3.7.

Prove that if $Σ ⊬ α$ then $Σ ∪ ( α | α )$ is consistent. (Use introduction rules, cut and the double negation rule.)

Exercise 3.8.

Show that if $Σ ⊆ ST ( X )$ is consistent then there is a maximally consisten $Σ + ⊇ Σ$. For this $Σ +$ show that:

(a) the valuation $v ( p ) = ⊤$ if $p ∈ Σ +$ and $v ( p ) = ⊥$ if $( p | p ) ∈ Σ +$ is well-defined;

(b) if $( α | β ) ∈ Σ +$ then at least one of $α ∉ Σ +$ or $β ∉ Σ +$;

(c) if $( α | β ) ∉ Σ +$ then both $α ∈ Σ +$ and $β ∈ Σ +$;

(d) hence (by induction on terms in $ST ( X )$) $v ( α ) = ⊤$ iff $α ∈ Σ +$.

Exercise 3.9.

(a) Deduce from the previous exercise that $Σ$ is consistent implies that there is a valuation making each $α ∈ Σ$ true.

(b) Now assume that $Σ ⊬ β$ and use (a) to show that there is a valuation making each $α ∈ Σ$ true and $β$ false, i.e. that $Σ ⊭ β$.