Полнота атомных начальных секвенций
В секвенциальном исчислении полнота атомарных начальных секвенций утверждает, что начальные секвенции A ⊢ A (где A — произвольная формула ) могут быть получены только из атомарных начальных секвенций p ⊢ p (где p — атомарная формула ). Эта теорема играет роль, аналогичную эта-разложению в лямбда-исчислении и двойственную к исключению разреза и бета-редукции . Обычно это можно установить индукцией по структуре A , что гораздо проще, чем методом исключения разреза.
Ссылки
[ редактировать ]- Гаиси Такеути . Теория доказательств . Том 81 исследований по логике и основам математики . Северная Голландия, Амстердам, 1975 год.
- Анн Сьерп Трульстра и Хельмут Швихтенберг . Основная теория доказательств . Издание: 2, иллюстрированное, переработанное. Опубликовано издательством Кембриджского университета, 2000 г.
 | Эта математической логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее . |