Upper and Lower Bounds for the Height of Proofs in Sequent Calculus for Intuitionistic Logic

Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic are proved for the case when cut formulas may only contain essentially positive occurrences of the existential quantifier. The considered cases include both proofs with and proofs without function symbols.

Saved in:
Bibliographic Details
Published in:Journal of mathematical sciences (New York, N.Y.) N.Y.), 2023-09, Vol.275 (2), p.195-224
Main Author: Orevkov, V. P.
Format: Article
Language:English
Subjects:
Lower bounds
Mathematics
Mathematics and Statistics
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic are proved for the case when cut formulas may only contain essentially positive occurrences of the existential quantifier. The considered cases include both proofs with and proofs without function symbols.
ISSN:1072-3374
1573-8795
DOI:10.1007/s10958-023-06671-z