Арифметика Гейтинга - Heyting arithmetic

В математическая логика, Арифметика Гейтинга (иногда сокращенно HA) является аксиоматизацией арифметики в соответствии с философией интуиционизм.[1] Он назван в честь Аренд Хейтинг, который первым предложил это.

Вступление

Арифметика Гейтинга принимает аксиомы Арифметика Пеано (PA), но использует интуиционистская логика как правила вывода. В частности, закон исключенного среднего в общем случае не выполняется, хотя аксиому индукции можно использовать для доказательства многих конкретных случаев. Например, можно доказать, что ∀ Икс, y ∈ N : Икс = y ∨ Икс ≠ y это теорема (любые два натуральные числа либо равны друг другу, либо не равны друг другу). Фактически, поскольку "=" - единственный предикат символа в арифметике Гейтинга, из этого следует, что для любого квантификатор -бесплатная формула п, ∀ Икс, y, z, … ∈ N : п ∨ ¬п это теорема (где Икс, y, z… Являются свободные переменные в п).

История

Курт Гёдель изучал взаимосвязь между арифметикой Гейтинга и арифметикой Пеано. Он использовал Негативный перевод Гёделя – Гентцена доказать в 1933 году, что если HA непротиворечиво, то PA также непротиворечиво.

Связанные понятия

Не следует путать арифметику Гейтинга с Гейтинговые алгебры, которые являются интуиционистским аналогом Булевы алгебры.

Смотрите также

Рекомендации

  1. ^ Троельстра 1973: 18
  • Ульрих Коленбах (2008), Теория прикладных доказательств, Springer.
  • Энн С. Трельстра, изд. (1973), Метаматематическое исследование интуиционистской арифметики и анализа, Спрингер, 1973.

внешняя ссылка