Another 0-1 system

This set of exercises concerns an interesting modifcation of the formal system of Chapter 3 of The Mathematics of Logic. The alphabet is again $\{0, 1\}$ and all strings of finite length including zero length are again well-formed formulas. The Given rule is included as before, and the lengthening and shortening rules are now as follows.

Lengthening: if $σ τ$ is written down then so can $σ i τ$ , where $σ, τ \in 2^{*}$ are any strings and $i$ is $0$ or $1$ .
Shortening: if $σ 0 τ$ and $σ 1 τ$ are both written down then so may be $σ τ$ , where $σ, τ \in 2^{*}$ are any strings.

Thus the system allows lengthening and shortening at any position in a string, not just at the end. Since $σ, τ$ may be empty, the old rules are instances of the new rules, but not the other way round. This makes the analysis of the system quite tricky at times, and somewhat different to the other system. Do not expect these exercises to be straightforward or even similar to the related results for the other system.

Exercise.

Show that if $Σ ⊢ σ$ then there is a formal proof of $σ$ from $Σ$ which consists of three blocks: a block of applications of the Given rule; then a (possibly empty) block of applications of Lengthening; then a (possibly empty) block of applications of Shortening.

Exercise.

Is it true whenever $Σ ⊢ σ$ there is a formal proof of $σ$ from $Σ$ which consists of three blocks: a block of applications of the Given rule; then a (possibly empty) block of applications of Shortening; then a (possibly empty) block of applications of Lengthening? (I don't know the answer!)

Exercise.

(Possibly rather hard!) Give a (useful) semantics for the system and prove Soundness and Completeness theorems.