Since $\vdash A\land B\to A$ and $\vdash A\land B\to B$, by modus ponens and instances of the theorem schema 1 above, we have $\vdash\neg A\to\neg(A\land B)$ and $\vdash\neg B\to\neg(A\land B)$. This proves the first three cases.

For the last case, we start with the axiom $A\to(B\to A\land B)$, or $A\vdash B\to A\land B$ by the deduction theorem. Apply modus ponens twice to instances of schema 1, we get $A\vdash\neg\neg B\to\neg\neg(A\land B)$, or $\neg\neg B\vdash A\to\neg\neg(A\land B)$ by the deduction theorem twice. Again, applying modus ponens twice to instances of 1, we have $\neg\neg B\vdash\neg\neg A\to\neg\neg\neg\neg(A\land B)$, or $\neg\neg B,\neg\neg A\vdash\neg\neg\neg\neg(A\land B)$ by the deduction theorem. One application of modus ponens to an instance of schema 2, we have $\neg\neg B,\neg\neg A\vdash\neg\neg(A\land B)$, as desired. ∎

Since $\vdash A\to A\lor B$ and $\vdash B\to A\lor B$, by modus ponens twice to instances of the schema 1, we have $\vdash\neg\neg A\to\neg\neg(A\lor B)$ and $\vdash\neg\neg B\to\neg\neg(A\lor B)$. This settles the last three cases.

For the first case, we use the axiom $(A\to\perp)\to((B\to\perp)\to((A\lor B)\to\perp))$, which is just $\neg A\to(\neg B\to\neg(A\lor B))$, or $\neg A,\neg B\vdash\neg(A\lor B)$ by the deduction theorem twice. ∎

For the first two, all we need is $\neg A\vdash\neg\neg(A\to B)$. To see this, we have deduction

so $\neg A,A\vdash B$, or $\neg A\vdash A\to B$ by the deduction theorem. Since $(A\to B)\to\neg\neg(A\to B)$ is an instance of schema 3, by modus ponens, $\neg A\vdash\neg\neg(A\to B)$ as desired.

For the third, by the deduction theorem, it is enough to show $\neg\neg A,\neg B,A\to B\vdash\perp$. Now,

is a deduction of $\perp$ from $\neg\neg A,\neg B$, and $A\to B$, where $(A\to B)\to(\neg B\to\neg A)$ is a theorem.

For the last, all we need to show is $\neg\neg B\vdash\neg\neg(A\to B)$. We start with $B\to(A\to B)$, which is an axiom. Applying modus ponens twice to instances of 1, we have $\vdash\neg\neg B\to\neg\neg(A\to B)$, or $\neg\neg B\vdash\neg\neg(A\to B)$. ∎

We use induction on the number $n$ of primitive logical connectives ($\land,\lor$, and $\to$) in $A$. If $n=0$, then $A$ is either $\perp$ or a propositional variable $p$. If $A$ is $\perp$, then $\perp\vdash\perp$, or $\vdash\neg\perp$, or $\vdash v[\perp]$. If $A$ is $p$, then clearly $v[p]\vdash v[p]$. Now, if $A$ has $n+1$ connectives, and is either $B\land C$, $B\lor C$, or $B\to C$, then $B$ and $C$ has no more than $n$ connectives. By induction,

or

By the first three lemmas above, $v[B],v[C]\vdash v[A]$, so by modus ponens twice,

∎

Let $v$ be any interpretation, then $v[p_{1}],\ldots,v[p_{m}]\vdash v[A]$ by the last lemma, where $p_{1},\ldots,p_{m}$ are all the propositional variables in $A$. Since $A$ is a tautology,

If $m=0$, then we are done. Otherwise, let $v_{1}$ and $v_{2}$ be two interpretations such that $v_{1}[p_{i}]=v_{2}[p_{i}]$ for $i=1,\ldots,m-1$, and $v_{1}[p_{m}]=\neg p_{m}$ and $v_{2}[p_{m}]=\neg\neg p_{m}$, so that

By applying the deduction theorem twice to each of the above deductive relations, we get

Apply schema 2 to the second deductive relation above, we get

By the deduction theorem once more, we have

With the axiom instance $(\neg A\to\neg p_{m})\to((\neg A\to\neg\neg p_{m})\to\neg\neg A)$, apply modus ponens to each of the last two deductive relations, we get

so that $v[p_{m}]$ is removed from the original deductive relation. Continue this process until all of the $v[p_{i}]$ are removed on the left, and we get

∎

By the theorem, $\vdash\neg\neg\neg A$. But $\vdash\neg\neg\neg A\to\neg A$, $\vdash\neg A$ by modus ponens. ∎

If $\vdash_{c}A$, then by the soundness theorem of classical propositional logic, $A$ is a tautology of truth-value semantics, which is just $V_{2}$, and therefore by the theorem above, $\vdash_{i}\neg\neg A$.

Conversely, if $\vdash_{i}\neg\neg A$, then certainly $\vdash_{c}\neg\neg A$, as PL${}_{i}$ is a subsystem of PL${}_{c}$. Since $\neg\neg A\to A$ is a theorem of PL${}_{c}$, we get $\vdash_{c}A$ by modus ponens. ∎