Normal Form Theorem for Systems of Sequents
Publications de l'Institut Mathématique, _N_S_82 (2007) no. 96, p. 37
Cet article a éte moissonné depuis la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts
In a system of sequents for intuitionistic predicate
logic a theorem, which corresponds to Prawitz's Normal Form
Theorem for natural deduction, are proved. In sequent
derivations a special kind of cuts, maximum cuts, are defined.
Maximum cuts from sequent derivations are connected with maximum
segments from natural deduction derivations, i.e., sequent
derivations without maximum cuts correspond to normal derivations
in natural deduction. By that connection the theorem for the
system of sequents (which correspond to Normal Form Theorem for
natural deduction) will have the following form: for each sequent
derivation whose end sequent is $\Gamma\vdash A$ there is a
sequent derivation without maximum cuts whose end sequent is
$\Gamma\vdash A$.
DOI :
10.2298/PIM0796037B
Classification :
03F05
Keywords: cut-elimination theorem, normalization theorem
Keywords: cut-elimination theorem, normalization theorem
@article{10_2298_PIM0796037B,
author = {Mirjana Borisavljevi\'c},
title = {Normal {Form} {Theorem} for {Systems} of {Sequents}},
journal = {Publications de l'Institut Math\'ematique},
pages = {37 },
year = {2007},
volume = {_N_S_82},
number = {96},
doi = {10.2298/PIM0796037B},
zbl = {1164.03016},
language = {en},
url = {http://geodesic.mathdoc.fr/articles/10.2298/PIM0796037B/}
}
Mirjana Borisavljević. Normal Form Theorem for Systems of Sequents. Publications de l'Institut Mathématique, _N_S_82 (2007) no. 96, p. 37 . doi: 10.2298/PIM0796037B
Cité par Sources :