Solidez: ⊢ implica ⊨

Es el Teorema 1.35 de (Huth y Ryan, 2004) , donde están todos los detalles. Se procede por inducción sobre la longitud $k$ de una prueba de $\Gamma \vdash \psi$.

• Base ($k=1$): una prueba de longitud $1$ es una premisa, $\phi \vdash \phi$, cuya validez semántica $\phi \vDash \phi$ es inmediata, o una instancia de LEM, $\vdash \phi\vee\neg\phi$, verdadera bajo toda valuación por bivalencia.
• Paso inductivo: suponiendo el teorema para pruebas más cortas (hipótesis de inducción), se analiza la última regla usada. Por ejemplo, si es $\rightarrow\mathrm{i}$ para derivar $\phi \rightarrow \chi$, hay una subprueba de $\Gamma, \phi \vdash \chi$, luego $\Gamma, \phi \vDash \chi$. Para una valuación $v$ que hace verdadera a $\Gamma$: si $v(\phi)=F$, entonces $v(\phi \rightarrow \chi)=T$; si $v(\phi)=T$, la hipótesis da $v(\chi)=T$, de nuevo $v(\phi \rightarrow \chi)=T$. En ambos casos $\Gamma \vDash \phi\rightarrow\chi$.
• Regla clásica (RAA): si la última regla es la reducción al absurdo (de una subprueba de $\Gamma,\neg\phi \vdash \bot$ se concluye $\Gamma \vdash \phi$), la hipótesis de inducción da $\Gamma,\neg\phi \vDash \bot$. Sea $v$ una valuación que satisface $\Gamma$; si fuera $v(\phi)=F$ se tendría $v(\neg\phi)=T$, con lo que $v$ satisfaría $\Gamma\cup\{\neg\phi\}$ y, por la hipótesis, $v(\bot)=T$, imposible. Luego $v(\phi)=T$ y $\Gamma\vDash\phi$. RAA es, junto con LEM, la única regla cuya validez depende esencialmente de que la semántica sea bivalente: para semánticas no clásicas (como la de Kripke de la lógica intuicionista) ambas dejan de ser sólidas, mientras que las reglas del núcleo intuicionista siguen siéndolo.

Los demás casos ($\wedge\mathrm{i}$, $\wedge\mathrm{e}$, $\vee\mathrm{i}$, $\vee\mathrm{e}$, $\rightarrow\mathrm{e}$, $\neg\mathrm{i}$, $\neg\mathrm{e}$, $\bot\mathrm{e}$) son análogos y rutinarios (cada regla preserva la verdad semántica); los detalles están en (Huth y Ryan, 2004) . Por inducción, el teorema vale para toda prueba.