Генцен, Герхард: различия между версиями

Его [[Теорема Генцена об устранении сечения|теорема об устранении сечения]] является краеугольным камнем [[теоретико-доказательная семантика|теоретико-доказательной семантики]]. В 1936 году Генцен {{Не переведено 2|Доказательство непротиворечивости Генцена|доказал|en|Gentzen's consistency proof}} совместность [[Аксиомы Пеано|аксиом Пеано]], то есть непротиворечивость арифметики<ref>''Генцен Г.'' Непротиворечивость чистой теории чисел. // Математическая теория логического вывода. М.: Наука, 1967, стр. 77-153.</ref>; для этого ему понадобилось добавить к [[Логика первого порядка|логике первого порядка]] дополнительную аксиому (бескванторную [[Трансфинитная индукция|трансфинитную индукцию]]). Тем самым он завершил выполнение программы [[Гильберт, Давид|Гильберта]] по формализации [[Метаматематика|оснований математики]].