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
- Ulrich Kohlenbach (2008), Stosowana teoria dowodu , Springer.
- Anne S. Troelstra , wyd. (1973), Metamathematyczne badanie intuicjonistycznej arytmetyki i analizy , Springer, 1973.
Zewnętrzne linki
- Stanford Encyclopedia of Philosophy : „ Intuitionistic Number Theory ” Joan Moschovakis .
- Fragments of Heyting Arithmetic autorstwa Wolfganga Burra