Solution (source code)

= Solution

A <logical derivation> from $\Gamma$ is a finite <sequence> of <propositional formulas>, each either a member of $\Gamma$, an instance of one of the three <axioms>, or obtained from earlier lines by one of the two displayed <inference rules>. The notation $\Gamma\vdash\alpha$ means that some such <logical derivation> ends in $\alpha$. Writing $\vdash\alpha$ means derivability with no assumptions.

<Propositional consistency> means that there is no <propositional formula> $\theta$ for which both $\Gamma\vdash\theta$ and $\Gamma\vdash\neg\theta$. Equivalently not every <propositional formula> is derivable. To check the equivalence directly for this calculus, use the identity theorem proved in (ii): from $\theta\to\theta$ and L3 obtain $\theta\to(\neg\theta\to\eta)$; two uses of <modus ponens rule> give arbitrary $\eta$. Thus a contradictory theory proves everything. Conversely a theory proving everything proves a <propositional formula> and its <negation>.