|
Zapiski Nauchnykh Seminarov POMI, 2020, Volume 497, Pages 124–169
(Mi znsl7030)
|
|
|
|
Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
V. P. Orevkov St. Petersburg Department of Steklov Mathematical Institute of Russian Academy of Sciences
Abstract:
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.
Key words and phrases:
intuitionistic predicate calculus, cut elimination, upper bounds, lower bounds.
Received: 10.12.2020
Citation:
V. P. Orevkov, “Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic”, Combinatorics and graph theory. Part XII, Zap. Nauchn. Sem. POMI, 497, POMI, St. Petersburg, 2020, 124–169
Linking options:
https://www.mathnet.ru/eng/znsl7030 https://www.mathnet.ru/eng/znsl/v497/p124
|
Statistics & downloads: |
Abstract page: | 85 | Full-text PDF : | 33 | References: | 16 |
|