Tłumaczenie Friedmana
W logice matematycznej przekład Friedmana jest pewnym przekształceniem formuł intuicjonistycznych . Między innymi można go użyć do wykazania, że 0 Π 2 różnych teorii pierwszego rzędu matematyki klasycznej są również twierdzeniami matematyki intuicjonistycznej. Jej nazwa pochodzi od nazwiska jej odkrywcy, Harveya Friedmana .
Definicja
Niech A i B będą formułami intuicjonistycznymi, w których żadna zmienna wolna B nie jest kwantyfikowana w A . Translacja AB jest atomowej zdefiniowana przez zastąpienie każdej podformuły C A przez C ∨ B . Dla celów tłumaczenia ⊥ jest również uważane za wzór atomowy, dlatego jest zastępowane przez ⊥ ∨ B (co jest równoważne B ). Zauważ, że ¬ A jest skrótem dla A → ⊥, stąd (¬ A ) B = A B → B .
Aplikacja
Translację Friedmana można wykorzystać do pokazania domknięcia wielu teorii intuicjonistycznych pod regułą Markowa oraz do uzyskania wyników częściowej konserwatywności . Kluczowym warunkiem jest, aby były rozstrzygalne, pozwalając na zbieżność niekwantyfikowanych twierdzeń teorii intuicjonistycznej i klasycznej.
Na przykład, jeśli A jest dowodliwe w arytmetyce Heytinga (HA), to AB jest również dowodliwe w HA. Ponadto, jeśli A jest 0 formułą Σ 1 , to AB równoważne jest w HA A ∨ B . To daje do zrozumienia ze:
- 0 Arytmetyka Heytinga jest zamknięta pod pierwotną rekurencyjną regułą Markowa (MP PR ): jeśli formuła ¬¬ A jest dowodliwa w HA, gdzie A jest formułą Σ 1 , to A jest również dowodliwa w HA.
- 00 Arytmetyka Peano jest Π 2 -konserwatywna w stosunku do arytmetyki Heytinga: jeśli arytmetyka Peano dowodzi Π 2 -formuły A , to A jest już dowodliwe w HA.