En Ebbinghaus et al., La Lógica matemática, un secuente de cálculo con las siguientes reglas se utiliza:
(Ant) $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma' & \varphi\end{array}$, if $\Gamma \subseteq \Gamma'$ $\qquad$ (Assm) $\begin{array}{ll} \\ \hline \Gamma & \varphi\end{array}$ si $\varphi \in \Gamma$
(PC) $\begin{array}{lll} \Gamma & \psi & \varphi \\ \Gamma & \lnot \psi & \varphi \\ \hline \Gamma & & \varphi\end{array}$ $\qquad\qquad$ (Ctr) $\begin{array}{lll} \Gamma & \lnot\varphi & \psi \\ \Gamma & \lnot \varphi & \lnot \psi \\ \hline \Gamma & & \varphi\end{array}$
($\lor A$) $\begin{array}{lll} \Gamma & \varphi & \chi \\ \Gamma & \psi & \chi\\ \hline \Gamma & (\varphi\lor\psi) & \chi\end{array}$ $\qquad$ ($\lor S$) $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma & (\varphi\lor\psi)\end{matriz}$, $\begin{array}{ll} \Gamma & \varphi \\ \hline \Gamma & (\psi\lor\varphi)\end{array}$
($\exists A$) $\begin{array}{lll} \Gamma & \varphi\frac{y}{x} & \psi \\ \hline \Gamma & \exists x\varphi & \psi\end{array}$, if $s$ is not free in $\Gamma \; \exists x\varphi \; \psi$
($\exists S$) $\begin{array}{ll} \Gamma & \varphi\frac{t}{x} \\ \hline \Gamma & \exists x\varphi\end{array}$
($\equiv$) $\begin{array}{l} \\ \hline t \equiv t\end{array}$ $\qquad\qquad$ (Sub) $\begin{array}{lll} \Gamma & & \varphi\frac{t}{x} \\ \hline \Gamma & t \equiv t' & \varphi\frac{t'}{x}\end{array}$
Parece que este cálculo sólo consiste en la deducción de reglas, sin ningún tipo de esquemas de axioma. Es esto correcto? O debemos interpretar (Assm) y ($\equiv$) como axioma esquemas, debido a que deducir algo de la nada? Lo que sobre (Ant) y (Sub), cuando la conclusión no está determinada únicamente por las premisas, porque pueden contener fórmulas arbitrarias o términos?
[Pregunta extra: La de Hilbert del sistema sólo tiene dos deducción de reglas, pero muchos de los axiomas y esquemas de axioma. Con la de Hilbert del sistema, a menudo me he tenido que buscar "pruebas" en algún lugar, porque no he podido encontrar por mí mismo. Con el secuente cálculo, me parecen ser capaces de encontrar las pruebas mí mismo. Hay un matemático explicación para este fenómeno?]
En su revisión del citado libro, Peter Smith critica fuertemente el elegido de sistema de deducción:
Ch. 4 se llama " Un Secuente de Tornasol. La versión elegida es realmente, realmente, no es muy agradable. Para empezar (aunque a un menor punto de que sólo afecta a la legibilidad), en lugar de escribir un secuente como $\text{‘}\Gamma \vdash \varphi\text{'}$ o $\text{‘}\Gamma \Rightarrow \varphi\text{'}$, o incluso el $\text{‘}\Gamma : \varphi\text{'}$, EFT sólo tienes que escribir un unpunctuated $\text{‘}\Gamma \; \varphi\text{'}$. Mucho más serio, que la adopción de un sistema de reglas que muchos dirían que se mezcla estructurales de las reglas clásicas y las reglas lógicas para las conectivas sin principios camino (perdiendo sólo la información que es un secuente sistema puede ser utilizado para resaltar). [Para ser más específicos, se introduce un clásico 'de Prueba por Casos de' regla que nos lleva desde el sequents (en su notación) $\Gamma \; \psi \; \varphi$$\Gamma \; \lnot \psi \; \varphi$$\Gamma \; \varphi$, y luego apelar a la Prueba por Casos a la Corte como un derivado de la regla. Esto realmente se enturbia las aguas de varias maneras!]
La cosa más cercana a la (Corte) que se deriva como consecuencia de las reglas en el libro de la Regla de la Cadena:
(Ch) $\begin{array}{lll} \Gamma & & \varphi \\ \Gamma & \varphi & \psi \\ \hline \Gamma & & \psi \end{array}$ $\quad$ while (Cut) would be $\begin{array}{lcr} \Gamma & \vdash & \Delta \; \varphi \\ \varphi \; \Lambda & \vdash & \psi \\ \hline \Gamma \; \Lambda & \vdash & \Delta \; \psi \end{matriz}$ or $\begin{array}{lll} \Gamma & & \varphi \\ \varphi & \Lambda & \psi \\ \hline \Gamma & \Lambda & \psi \end{array}$
No veo cómo (Ch) o (Cut) podría reemplazar (PC). No estoy seguro de si esto está relacionado con el hecho de que el anterior cálculo interpreta un secuente $\phi \; \varphi \; \psi \; \chi$$\phi \rightarrow (\varphi \rightarrow (\psi \rightarrow \chi))$, de modo que cada sequent debe tener exactamente una succedent, y el $\vdash$ signo puede ser omitido. Es posible añadir (Cut) como regla general, quitar una de las otras reglas, y posiblemente ajustar el resto de reglas ligeramente, y obtener el mismo cálculo (donde el original sin modificar las reglas puede ser obtenida tal y como se deriva de las reglas)?
