"Записки научных семинаров ПОМИ"

Том 497, стр. 124-169

С.-Петербургское отделение Математического института им. В. А. Стеклова РАН, Фонтанка 27, 191023 Санкт-Петербург, Россия

e-mail

Аннотация: Целью данной работы является получение оценок сокращения высоты секвенциального доказательства в интуиционистском исчислении предикатов с помощью сечений по формулам, содержащим существенно положительные вхождения квантора $\exists.$ Рассмотрены как доказательства с функциональными знаками, так и без функциональных знаков. Библ. -- 12 назв.
Ключевые слова: интуиционистское исчисление предикатов, устранение сечений, верхняя оценка, нижняя оценка [intuitionistic predicate calculus, cut elimination, upper bounds, lower bounds]