Normal Form Theorem for Systems of Sequents
Publications de l'Institut Mathématique, _N_S_82 (2007) no. 96, p. 37 .

Voir la notice de l'article provenant de 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
@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 },
     publisher = {mathdoc},
     volume = {_N_S_82},
     number = {96},
     year = {2007},
     doi = {10.2298/PIM0796037B},
     zbl = {1164.03016},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.2298/PIM0796037B/}
}
TY  - JOUR
AU  - Mirjana Borisavljević
TI  - Normal Form Theorem for Systems of Sequents
JO  - Publications de l'Institut Mathématique
PY  - 2007
SP  - 37 
VL  - _N_S_82
IS  - 96
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.2298/PIM0796037B/
DO  - 10.2298/PIM0796037B
LA  - en
ID  - 10_2298_PIM0796037B
ER  - 
%0 Journal Article
%A Mirjana Borisavljević
%T Normal Form Theorem for Systems of Sequents
%J Publications de l'Institut Mathématique
%D 2007
%P 37 
%V _N_S_82
%N 96
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.2298/PIM0796037B/
%R 10.2298/PIM0796037B
%G en
%F 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. http://geodesic.mathdoc.fr/articles/10.2298/PIM0796037B/

Cité par Sources :