Loading AI tools
Из Википедии, свободной энциклопедии
Устранимость сечений (теорема Генцена, элиминационная теорема) — свойство логических исчислений, согласно которому всякую секвенцию, выводимую в данном исчислении, можно вывести без применения правила сечений[1]. Играет фундаментальную роль в теории доказательств и важную методологическую роль в математической логике в целом в связи с тем, что предоставляет конструктивный метод доказательства непротиворечивости, в частности, для классической и интуиционистской логик первого порядка[2].
Для классического и интуиционистского исчислений секвенций свойство доказано Генценом в 1934 году. В 1953 году высказана гипотеза Такеути, согласно которой устранимость сечений имеет место для простой теории типов и соответствующих ей логик высших порядков, впоследствии она нашла подтверждение — для классической логики второго порядка устранимость сечений доказал Тейт[англ.], для простой теории типов — Такахаси и Правица[швед.], вскоре найдены доказательства для серии неклассических теорий высших порядков (Драгалин) и развитых теорий типов (Жирар[англ.] для системы F).
Символическая формулировка: пусть и — доказуемые секвенции исчисления ; если — секвенция исчисления , то она доказуема[3].
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.