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 \in X$ is in $ST (X)$ and if $α, β \in 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 $α \in Σ$ then $Σ ⊢ α$ .

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

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

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

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 ||-I_L one can prove $(α | (α | α))$ for all $α$ .

Exercise 3.2.

Show that using only W_L, ||-E_L and |-I_L one can show $α ⊢ ((α | α) | (α | α))$ for all $α$ .

Exercise 3.3.

Exercise 3.4.

Show that the |-Cut_L rule is a metarule of the system with ||-E_R, |-E_L and |-I_L.

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 |-E_L, ||-E_L, |-I_L, ||-I_L, W_L and the double negation rule.

Definition.

A valuation is a map $v : X \to \{⊤ ⊥\}$ . Valuations are extended to arbitrary terms of $ST (X)$ by $v (α | β) = v (α)' \lor v (β)'$ .

Definition.

$Σ ⊨ β$ means that for all valuations $v$ , if $v (α) = ⊤$ for all $α \in Σ$ 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 |-I_L, ||-I_L and a cut rule to show that if $Σ \cup \{α\}$ is inconsistent then $Σ ⊢ (α | α)$ . Deduce that if $Σ$ is consistent and $α$ is any term in $ST (X)$ then at least one of $Σ \cup \{α\}$ or $Σ \cup \{(α | α)\}$ is consistent.

Exercise 3.7.

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

Exercise 3.8.

Show that if $Σ \subseteq ST (X)$ is consistent then there is a maximally consisten $Σ^{+} \supseteq Σ$ . For this $Σ^{+}$ show that:

(a) the valuation $v (p) = ⊤$ if $p \in Σ^{+}$ and $v (p) = ⊥$ if $(p | p) \in Σ^{+}$ is well-defined;

(b) if $(α | β) \in Σ^{+}$ then at least one of $α \notin Σ^{+}$ or $β \notin Σ^{+}$ ;

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

Exercise 3.9.

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

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