Geodesic
Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part XII, Tome 497 (2020), pp. 124-169 
V. P. Orevkov. Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic. Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part XII, Tome 497 (2020), pp. 124-169. http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/
@article{ZNSL_2020_497_a5,
     author = {V. P. Orevkov},
     title = {Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {124--169},
     year = {2020},
     volume = {497},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/}
}
TY  - JOUR
AU  - V. P. Orevkov
TI  - Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2020
SP  - 124
EP  - 169
VL  - 497
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/
LA  - ru
ID  - ZNSL_2020_497_a5
ER  - 
%0 Journal Article
%A V. P. Orevkov
%T Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
%J Zapiski Nauchnykh Seminarov POMI
%D 2020
%P 124-169
%V 497
%U http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/
%G ru
%F ZNSL_2020_497_a5

Voir la notice du chapitre de livre provenant de la source Math-Net.Ru

We prove upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic for the case when cut formulas may only contain essentially positive occurrences of the existential quantifier. We consider the cases of both proofs with and proofs without function symbols.

[1] A. G. Dragalin, Matematicheskii intuitsionizm. Vvedenie v teoriyu dokazatelstv, Nauka, M., 1979 | MR

[2] S. K. Klini, “Perestanovochnost primenenii pravil v gentsenovskikh ischisleniyakh LK i LJ”, Matematicheskaya teoriya logicheskogo vyvoda, Nauka, M., 1967

[3] S. K. Klini, Matematicheskaya logika, Mir, M., 1973

[4] B. Yu. Konev, “Utochnenie otsenok vysoty termov v naibolee obschem unifikatore”, Zap. nauchn. seminarov POMI, 241, 1997, 117–134 | Zbl

[5] B. Yu. Konev, “Verkhnyaya otsenka vysoty termov v vyvodakh s secheniyami po formulam ogranichennoi glubiny svyazannykh vkhozhdenii”, Zap. nauchn. seminarov POMI, 277, 2001, 80–103 | Zbl

[6] G. E. Mints, V. P. Orevkov, “O pogruzhayuschikh operatsiyakh”, Zap. nauchn. seminarov POMI, 4, 1967, 163–175

[7] V. P. Orevkov, “O glivenkovskikh klassakh sekventsii”, Tr. Matem. in-ta AN SSSR, 98, 1968, 131–154 | MR | Zbl

[8] V. P. Orevkov, “Nizhnie otsenki uvelicheniya slozhnosti vyvodov posle ustraneniya sechenii”, Zap. nauchn. seminarov POMI, 88, 1979, 137–162 | Zbl

[9] V. P. Orevkov, Complexity of proofs and their transformations in axiomatic theories, Amer. Math. Soc., 1993 | MR | Zbl

[10] R. Harrop, “Concering formulas of types $A\rightarrow B\vee C, A\rightarrow\exists xB(x)$”, J. Symbolic Logic, 25:1 (1960), 27–32 | DOI | MR | Zbl

[11] R. Statman, The predicate calculus is not a Kalmar elementary speed-up of the equation calculus, Cambbridge, 1975 | MR

[12] R. Statman, “Bounds for proof-search and speed-up in the predicate calculus”, Ann. Math. Logic, 15 (1978), 225–287 | DOI | MR | Zbl