Арифметика Гейтинга - Heyting arithmetic
В математической логике , гейтингова арифметическое (иногда сокращенно ГА ) является аксиоматизация арифметики в соответствии с философией интуиционизма . Он назван в честь Аренд Хейтинг , которая первой предложила его.
Вступление
Арифметика Гейтинга принимает аксиомы арифметики Пеано (PA), но использует интуиционистскую логику в качестве правил вывода. В частности, закон исключенного третьего в общем случае не выполняется, хотя аксиому индукции можно использовать для доказательства многих конкретных случаев. Например, можно доказать, что ∀ x , y ∈ N : x = y ∨ x ≠ y - теорема (любые два натуральных числа либо равны друг другу, либо не равны друг другу). Фактически, поскольку "=" является единственным предикатным символом в арифметике Гейтинга, отсюда следует, что для любой бескванторной формулы φ , ∀ x , y , z , ... ∈ N : φ ∨ ¬ φ является теоремой ( где x , y , z ... - свободные переменные в φ ).
История
Курт Гёдель изучал взаимосвязь между арифметикой Гейтинга и арифметикой Пеано. Он использовал отрицательный перевод Гёделя – Генцена, чтобы доказать в 1933 году, что если HA непротиворечиво, то PA также непротиворечиво.
Связанные понятия
Не следует путать арифметику Гейтинга с алгебрами Гейтинга , которые являются интуиционистским аналогом булевых алгебр .
Смотрите также
Рекомендации
- Ульрих Коленбах (2008), Прикладная теория доказательств , Springer.
- Энн С. Трельстра , изд. (1973), Метаматематические исследования интуиционистской арифметики и анализа , Springer, 1973.
внешняя ссылка
- Стэнфордская энциклопедия философии : « Интуиционистская теория чисел » Джоан Мощовакис .
- Фрагменты арифметики Гейтинга Вольфганга Бёрра
 |
Эта статья по математической логике - незавершенная . Вы можете помочь Википедии, расширив ее . |