We sketch a simple proof of Herbrand's theorem for Gentzen's calculi of sequents LK and LJ in the general case, without restrictions to sequents containing only prenex formulas. In the case of classical logic LK, the statement of the theorem is that for any sequent S of LK, S is derivable in first order LK if and only if for some p the Herbrand expansion E_p(S) is provable in the propositional part of LK. In the case of intuitionistic logic LJ, a sequent S is derivable in first order LJ if and only if for some p the Herbrand expansion E_p(S) is provable in the propositional part of LJ with an "adequate" proof, where a proof of E_p(S) is adequate if it satisfies certain conditions on permutability of inferences given in Kleene 1952.
Herbrand's Theorem for Calculi of Sequents LK and LJ
BELLIN, Gianluigi
1979-01-01
Abstract
We sketch a simple proof of Herbrand's theorem for Gentzen's calculi of sequents LK and LJ in the general case, without restrictions to sequents containing only prenex formulas. In the case of classical logic LK, the statement of the theorem is that for any sequent S of LK, S is derivable in first order LK if and only if for some p the Herbrand expansion E_p(S) is provable in the propositional part of LK. In the case of intuitionistic logic LJ, a sequent S is derivable in first order LJ if and only if for some p the Herbrand expansion E_p(S) is provable in the propositional part of LJ with an "adequate" proof, where a proof of E_p(S) is adequate if it satisfies certain conditions on permutability of inferences given in Kleene 1952.File | Dimensione | Formato | |
---|---|---|---|
Herbrand1978.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
586.1 kB
Formato
Adobe PDF
|
586.1 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.