Arytmetyka heytowania - Heyting arithmetic

W logice matematycznej , Heytinga arytmetyka (czasami w skrócie HA ) jest aksjomatyzacji arytmetycznych zgodnie z filozofią intuicjonizmu . Został nazwany na cześć Arenda Heytinga , który jako pierwszy go zaproponował.

Wprowadzenie

Arytmetyka Heytinga przyjmuje aksjomaty arytmetyki Peano (PA), ale używa logiki intuicjonistycznej jako reguł wnioskowania. W szczególności prawo wyłączonego środka nie obowiązuje w ogóle, chociaż aksjomat indukcji można wykorzystać do udowodnienia wielu konkretnych przypadków. Na przykład, można udowodnić, że x , y N  : x = y x y jest twierdzeniem (dowolne dwie liczby naturalne są sobie równe lub różne). W rzeczywistości, ponieważ "=" jest jedynym symbolem predykatu w arytmetyce Heytinga, wynika z tego, że dla dowolnego wzoru bez kwantyfikatora φ , x , y , z , ... ∈ N  : φ ∨ ¬ φ jest twierdzeniem ( gdzie x , y , z ... są wolnymi zmiennymi w φ ).

Historia

Kurt Gödel badał związek między arytmetyką Heytinga a arytmetyką Peano. Użył negatywnego tłumaczenia Gödela – Gentzena, aby udowodnić w 1933 r., Że jeśli HA jest spójny, to również PA jest spójny.

Pojęcia pokrewne

Arytmetyki Heyting nie należy mylić z algebrami Heytinga , które są intuicjonistycznym odpowiednikiem algebr Boole'a .

Zobacz też

Bibliografia

Zewnętrzne linki