Własności dysjunkcji i istnienia

W logice matematycznej właściwości dysjunkcji i istnienia są „cechami charakterystycznymi” teorii konstruktywnych , takich jak arytmetyka Heytinga i konstruktywne teorie mnogości (Rathjen 2005).

Właściwość dysjunkcyjna

Własność dysjunkcji jest spełniona przez teorię, jeśli kiedykolwiek zdanie A ∨ B jest twierdzeniem , to albo A jest twierdzeniem, albo B jest twierdzeniem.

Właściwość istnienia

Własność istnienia lub własność świadka jest spełniona przez teorię, jeśli kiedykolwiek zdanie (∃ x ) A ( x ) jest twierdzeniem, gdzie A ( x ) nie ma innych zmiennych wolnych, to istnieje taki wyraz t , którego teoria dowodzi A ( t ) .

Powiązane właściwości

Rathjen (2005) wymienia pięć właściwości, które może posiadać teoria. Należą do nich właściwość alternatywna ( DP ), właściwość istnienia ( EP ) i trzy dodatkowe właściwości:

Numeryczna $gdzie$ ) teoria udowodni φ nie innych $\ varphi ({\ bar {n}})}$ Displaystyle dla pewnego ${\ Displaystyle n \ in \ mathbb {N} {\ tekst {.}}}$ Tutaj ${\ displaystyle {\ bar {n}}}$ jest terminem w ${\ displaystyle T}$ reprezentującym liczbę n .
Reguła Kościoła (CR) stwierdza, że jeśli teoria dowodzi ${\ Displaystyle (\ forall x \ in \ mathbb {N}) (\ istnieje y \ in \mathbb {N} )\varphi (x,y)}$ wtedy istnieje liczba naturalna e taka, że pozwalając $obliczalną$ funkcją z indeksem e , dowodzi ${\ Displaystyle (\ forall x) \ varphi (x, f_ {e} (x))}$ .
Wariant reguły Churcha, CR ₁ , stwierdza, że jeśli teoria udowodni ${\ Displaystyle (\ istnieje f \ okrężnica \ mathbb {N} \ do \ mathbb {N}) \ psi (f)}$ to istnieje liczba naturalna e taka, że teoria dowodzi, $\ Displaystyle \ psi (f_ {e$ jest całkowita i dowodzi, że $)}$ .

$}$ właściwości można wyrazić bezpośrednio tylko dla teorii, które mają zdolność do kwantyfikowania liczb naturalnych, a dla CR ₁ kwantyfikowania funkcji od do $}$ . W praktyce można powiedzieć, że teoria ma jedną z tych właściwości, jeśli definicyjne rozszerzenie teorii ma właściwość określoną powyżej (Rathjen 2005).

Tło i historia

Kurt Gödel (1932) stwierdził bez dowodu, że intuicjonistyczna logika zdań (bez dodatkowych aksjomatów) ma właściwość dysjunkcji; wynik ten został udowodniony i rozszerzony na intuicjonistyczną logikę predykatów przez Gerharda Gentzena (1934, 1935). Stephen Cole Kleene (1945) udowodnił, że arytmetyka Heytinga ma własność alternatywy i własność istnienia. Metoda Kleene'a wprowadziła technikę realizability , która jest obecnie jedną z głównych metod badania teorii konstruktywnych (Kohlenbach 2008; Troelstra 1973).

Chociaż najwcześniejsze wyniki dotyczyły konstruktywnych teorii arytmetyki, wiele wyników jest również znanych z konstruktywnych teorii mnogości (Rathjen 2005). John Myhill (1973) wykazał, że IZF z aksjomatem zastępowania wyeliminowanym na rzecz aksjomatu zbioru ma własność alternatywy, numeryczną własność istnienia i własność istnienia. Michael Rathjen (2005) udowodnił, że CZF ma właściwość alternatywy i numeryczną właściwość istnienia.

Większość klasycznych teorii, takich jak arytmetyka Peano i ZFC, nie ma właściwości istnienia ani alternatywy. Niektóre klasyczne teorie, takie jak ZFC plus aksjomat konstruowalności , mają słabszą postać własności istnienia (Rathjen 2005).

w topoi

Freyd i Scedrov (1990) zauważyli, że właściwość dysjunkcji zachodzi w wolnych algebrach Heytinga i wolnych toposach . W kategoriach kategorycznych , w wolnym toposie, $odpowiada$ to faktowi, że końcowy nie jest połączeniem dwóch właściwych podobiektów. Wraz z właściwością istnienia przekłada się to na twierdzenie, że $,$ nierozkładalnym obiektem rzutowym - funktor który reprezentuje ( funktor sekcji globalnej ) zachowuje epimorfizmy i koprodukty .

Relacje

Istnieje kilka zależności między pięcioma właściwościami omówionymi powyżej.

W warunkach arytmetyki numeryczna właściwość istnienia implikuje właściwość alternatywy. Dowód wykorzystuje fakt, że dysjunkcję można przepisać jako egzystencjalną formułę kwantyfikującą po liczbach naturalnych:

{\ Displaystyle A \ vee B \ równoważnik (\ istnieje n) [(n = 0 \ do A) \ klin (n \neq 0\do B)]}

.

Dlatego jeśli

{\ Displaystyle A \ vee B}

jest twierdzeniem

{\ Displaystyle T}

, więc jest

{\ Displaystyle \ istnieje n \ dwukropek (n =0\do A)\klin (n\neq 0\do B)}

.

Tak więc, zakładając numeryczną właściwość istnienia, istnieje taka, że ${\ displaystyle s}$

{\ Displaystyle ({\ bar {s}} = 0 \ do A) \ klin ({\ bar {s}} \ neq 0 \ do B)}

jest twierdzeniem. Ponieważ jest liczbą, można konkretnie sprawdzić wartość : jeśli $s$ $¯ {\$ {\ displaystyle s = 0}, to jest $displaystyle {$ \ $}$ twierdzenie i jeśli ${\ Displaystyle s \ neq 0},$ $jest$ twierdzeniem .

Harvey Friedman (1974) udowodnił, że w każdym rekurencyjnie przeliczalnym rozszerzeniu arytmetyki intuicjonistycznej właściwość alternatywy implikuje numeryczną własność istnienia. Dowód wykorzystuje zdania samoodnoszące się w sposób podobny do dowodu twierdzeń Gödla o niezupełności . Kluczowym krokiem jest znalezienie granicy na kwantyfikatorze egzystencjalnym we wzorze (∃ x )A( x ), tworząc ograniczoną formułę egzystencjalną (∃ x < n )A( x ). Formułę ograniczoną można więc zapisać jako skończoną dysjunkcję A(1)∨A(2)∨...∨A(n). Wreszcie, można zastosować eliminację dysjunkcji , aby pokazać, że jeden z dysjunkcji jest możliwy do udowodnienia.

Zobacz też

Peter J. Freyd i Andre Scedrov, 1990, Kategorie, Alegorie . Holandia Północna.
Harvey Friedman , 1975, Właściwość dysjunkcji implikuje numeryczną właściwość istnienia , Uniwersytet Stanowy Nowego Jorku w Buffalo.
Gerhard Gentzen , 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift t. 39 n. 2, s. 176–210.
Gerhard Gentzen , 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift t. 39 n. 3, s. 405–431.
Kurt Gödel , 1932, „Zum intuitionistischen Aussagenkalkül”, Anzeiger der Akademie der Wissenschaftischen in Wien , t. 69, s. 65–66.
Stephen Cole Kleene, 1945, „O interpretacji intuicjonistycznej teorii liczb”, Journal of Symbolic Logic , t. 10, s. 109–124.
Ulrich Kohlenbach , 2008, Stosowana teoria dowodu , Springer.
John Myhill , 1973, „Niektóre właściwości intuicjonistycznej teorii mnogości Zermelo-Fraenkla”, w: A. Mathias i H. Rogers, Cambridge Summer School in Mathematical Logic , Lectures Notes in Mathematics, t. 337, s. 206–231, Springer.
Michael Rathjen, 2005, „ Rozłączenie i właściwości pokrewne dla konstruktywnej teorii mnogości Zermelo-Fraenkla ”, Journal of Symbolic Logic , t. 70 n. 4, s. 1233–1254.
Anne S. Troelstra , wyd. (1973), Metamatematyczne badanie intuicjonistycznej arytmetyki i analizy , Springer.

Linki zewnętrzne

Logika intuicjonistyczna Joan Moschovakis, Stanford Encyclopedia of Philosophy