WikiDer > Арифметика Гейтинга

Heyting arithmetic

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

Вступление

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

История

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

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

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

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

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

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

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