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.
Fulltext:
PDF file (361 kB)