Considere la posibilidad de lógica proposicional primitiva conectivas $\{{\to},{\land},{\lor},{\bot}\}$. Vemos a $\neg \varphi$ como una abreviatura de $\varphi\to\bot$ $\varphi\leftrightarrow\psi$ como una abreviatura de $(\varphi\to\psi)\land(\psi\to\varphi)$, etc.
La clásica sequent cálculo LC tiene sus reglas, tales como
$$\frac{\Gamma \varphi\vdash \Pi \qquad \Sigma \psi\vdash \Pi} {\Gamma \Sigma \varphi\lor\psi \vdash \Pi}{\lor L} \qquad \frac{\Gamma\vdash\varphi,\Delta}{\Gamma\vdash\varphi\lor\psi\Delta}{\lor}R_1 \qquad \frac{\Gamma \vdash \psi \Delta}{\Gamma\vdash\varphi\lor\psi\Delta}{\lor}R_2 $$ $$ \frac{\Gamma\vdash\varphi,\Delta \qquad \Sigma\psi\vdash\Pi} {\Gamma \Sigma \varphi\a\psi \vdash \Delta\Pi} {\,} L \qquad \frac{\Gamma\varphi\vdash \psi\Delta}{\Gamma\vdash\varphi\a\psi\Delta} {\,} R $$ y así sucesivamente, donde $\Gamma$, $\Sigma$, $\Pi$, y $\Delta$ son finitos multisets de fórmulas.
Es bien sabido que si restringimos la forma de todos los sequents a tener exactamente una fórmula a la derecha de la $\vdash$, obtenemos un sistema a prueba de LJ para intuitionistic lógica proposicional. Esto corresponde a la necesidad de que todos los $\Delta$ está vacía y cada una de las $\Pi$ es un singleton en las formulaciones de las normas anteriores.
¿Todavía podemos obtener intuitionistic lógica si la única regla que tenemos que hacer que este cambio es ${\to}R$? En otras palabras, tenemos $$\frac{\Gamma,\varphi\vdash\psi}{\Gamma\vdash\varphi\to\psi}{\to}R'$$ junto con todas las otras reglas en su clásica formulación, incluyendo estructurales reglas con mucho $\Delta$s y $\Pi$s.
(Motivación: estoy tratando, una vez más, para envolver mi cabeza alrededor de lo que la esencial diferencia entre intuitionistic y la lógica clásica. Se dice a menudo que intuitionistic lógica surgió de Brouwer las más estrictas exigencias acerca de cómo una disyunción puede ser demostrado, pero que no puede ser toda la historia porque hay una diferencia, incluso para el implicational fragmento (sin diferencias). Ahora me pregunto si la disyunción es en realidad parte de la historia. La semántica de Kripke trata completamente clásico, y intuitionistic lógica se convierte en totalmente clásica si añadimos Peirce ley como un axioma (que de nuevo no hace mención de la disyunción). La anterior conjetura está inspirada en la de Curry-Howard isomorfismo donde Peirce ley asigna a call/cc, más o menos. Por lo tanto, tendría sentido que podemos obtener intuitionistic la lógica simplemente prohibiendo lambda abstracciones a partir de la captura de la continuación de variables).
