Аннотация:
Целью данной работы является получение оценок сокращения высоты секвенциального доказательства в интуиционистском исчислении предикатов с помощью сечений по формулам, содержащим существенно положительные вхождения квантора $\exists$. Рассмотрены как доказательства с функциональными знаками, так и без функциональных знаков. Библ. – 12 назв.
Ключевые слова:интуиционистское исчисление предикатов, устранение сечений, верхняя оценка, нижняя оценка.
Полный текст:
PDF файл (361 kB)