Proprietà di disgiunzione ed esistenza - Disjunction and existence properties

Nella logica matematica , la disgiunzione e le proprietà di esistenza sono i "tratti distintivi" di teorie costruttive come l' aritmetica di Heyting e le teorie degli insiemi costruttivi (Rathjen 2005).

Proprietà di disgiunzione

La proprietà di disgiunzione è soddisfatta da una teoria se, ogni volta che una frase A ∨ B è un teorema , allora A è un teorema o B è un teorema.

Proprietà di esistenza

La proprietà di esistenza o la proprietà testimone è soddisfatta da una teoria se, ogni volta che una frase (∃ x ) A ( x ) è un teorema, dove A ( x ) non ha altre variabili libere, allora esiste un termine t tale che la teoria dimostra A ( t ) .

Proprietà correlate

Rathjen (2005) elenca cinque proprietà che una teoria può possedere. Questi includono la proprietà di disgiunzione ( DP ), la proprietà di esistenza ( EP ) e tre proprietà aggiuntive:

• La proprietà di esistenza numerica (NEP) afferma che se la teoria dimostra , dove φ non ha altre variabili libere, allora la teoria dimostra per alcune. Ecco un termine per rappresentare il numero n .${\ displaystyle (\ esiste x \ in \ mathbb {N}) \ varphi (x)}$${\ displaystyle \ varphi ({\ bar {n}})}$${\ displaystyle n \ in \ mathbb {N} {\ text {.}}}$${\ displaystyle {\ bar {n}}}$${\ displaystyle T}$
• La regola di Church (CR) afferma che se la teoria dimostraallora esiste un numero naturale e tale che, lasciandoessere la funzione calcolabile con indice e , la teoria lo dimostra.${\ displaystyle (\ forall x \ in \ mathbb {N}) (\ esiste y \ in \ mathbb {N}) \ varphi (x, y)}$${\ displaystyle f_ {e}}$${\ displaystyle (\ forall x) \ varphi (x, f_ {e} (x))}$
• Una variante della regola di Church, CR ₁ , afferma che se la teoria dimostra, allora esiste un numero naturale e tale che la teoria dimostra che è totale e dimostra .${\ Displaystyle (\ exist f \ colon \ mathbb {N} \ to \ mathbb {N}) \ psi (f)}$${\ displaystyle f_ {e}}$${\ displaystyle \ psi (f_ {e})}$

Queste proprietà possono essere espresse direttamente solo per teorie che hanno la capacità di quantificare su numeri naturali e, per CR ₁ , quantificare su funzioni da a . In pratica, si può dire che una teoria ha una di queste proprietà se un'estensione definizionale della teoria ha la proprietà sopra indicata (Rathjen 2005). ${\ displaystyle \ mathbb {N}}$${\ displaystyle \ mathbb {N}}$

Background e storia

Kurt Gödel  (1932) affermò senza prove che la logica proposizionale intuizionistica (senza assiomi aggiuntivi) ha la proprietà di disgiunzione; questo risultato è stato provato ed esteso alla logica intuizionistica dei predicati da Gerhard Gentzen  (1934, 1935). Stephen Cole Kleene  (1945) ha dimostrato che l' aritmetica di Heyting ha la proprietà di disgiunzione e la proprietà di esistenza. Il metodo di Kleene ha introdotto la tecnica della realizzabilità , che oggi è uno dei metodi principali nello studio delle teorie costruttive (Kohlenbach 2008; Troelstra 1973).

Mentre i primi risultati erano per teorie costruttive dell'aritmetica, molti risultati sono noti anche per teorie costruttive degli insiemi (Rathjen 2005). John Myhill  (1973) ha mostrato che IZF con l' assioma di sostituzione eliminato a favore dell'assioma di raccolta ha la proprietà di disgiunzione, la proprietà di esistenza numerica e la proprietà di esistenza. Michael Rathjen (2005) ha dimostrato che CZF ha la proprietà di disgiunzione e la proprietà di esistenza numerica.

La maggior parte delle teorie classiche, come l'aritmetica di Peano e ZFC , non hanno la proprietà di esistenza o disgiunzione. Alcune teorie classiche, come ZFC più l' assioma della costruibilità , hanno una forma più debole della proprietà di esistenza (Rathjen 2005).

In topoi

Freyd e Scedrov (1990) hanno osservato che la proprietà di disgiunzione vale nelle algebre di Heyting libere e nei topoi liberi . In termini categorici , nelle topos liberi , che corrisponde al fatto che l' oggetto terminale , non è l'unione di due sotto-oggetti appropriati. Insieme alla proprietà esistenza traduce all'affermazione che è un indecomposable oggetto proiettiva -il funtore rappresenta (globale-sezione functor) conserva epimorphisms e coprodotti . ${\ displaystyle \ mathbf {1}}$${\ displaystyle \ mathbf {1}}$

Relazioni

Esistono diverse relazioni tra le cinque proprietà discusse sopra.

Nell'impostazione dell'aritmetica, la proprietà di esistenza numerica implica la proprietà di disgiunzione. La dimostrazione utilizza il fatto che una disgiunzione può essere riscritta come una formula esistenziale che quantifica su numeri naturali:

${\ Displaystyle A \ vee B \ equiv (\ exist n) [(n = 0 \ to A) \ wedge (n \ neq 0 \ to B)]}$.

Pertanto, se

${\ displaystyle A \ vee B}$è un teorema di , così è .${\ displaystyle T}$${\ Displaystyle \ esiste n \ colon (n = 0 \ to A) \ wedge (n \ neq 0 \ to B)}$

Quindi, assumendo la proprietà di esistenza numerica, ne esistono di tali che ${\ displaystyle s}$

${\ displaystyle ({\ bar {s}} = 0 \ to A) \ wedge ({\ bar {s}} \ neq 0 \ to B)}$

è un teorema. Poiché è un numero, si può verificare concretamente il valore di : se allora è un teorema e se allora è un teorema. ${\ displaystyle {\ bar {s}}}$${\ displaystyle s}$${\ displaystyle s = 0}$${\ displaystyle A}$${\ displaystyle s \ neq 0}$${\ displaystyle B}$

Harvey Friedman (1974) ha dimostrato che in ogni estensione ricorsivamente enumerabile dell'aritmetica intuizionistica , la proprietà di disgiunzione implica la proprietà di esistenza numerica. La dimostrazione utilizza frasi autoreferenziali in modo simile alla dimostrazione dei teoremi di incompletezza di Gödel . Il passaggio chiave è trovare un limite al quantificatore esistenziale in una formula (∃ x ) A ( x ), producendo una formula esistenziale limitata (∃ x < n ) A ( x ). La formula limitata può quindi essere scritta come una disgiunzione finita A (1) ∨A (2) ∨ ... ∨A (n). Infine, l' eliminazione della disgiunzione può essere utilizzata per dimostrare che una delle disgiunzioni è dimostrabile.

Guarda anche

• Teoria costruttiva degli insiemi
• Heyting aritmetica
• Legge di mezzo escluso
• Realizzabilità
• Quantificatore esistenziale

Riferimenti

• Peter J. Freyd e Andre Scedrov, 1990, Categorie, Allegorie . Olanda settentrionale.
• Harvey Friedman , 1975, La proprietà disgiunzione implica la proprietà di esistenza numerica , State University di New York a Buffalo.
• Gerhard Gentzen , 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift v. 39 n. 2, pagg. 176–210.
• Gerhard Gentzen , 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, pagg. 405–431.
• Kurt Gödel , 1932, "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaftischen a Vienna , v. 69, pp. 65-66.
• Stephen Cole Kleene, 1945, " Sull'interpretazione della teoria intuizionistica dei numeri", Journal of Symbolic Logic , v. 10, pp. 109-124.
• Ulrich Kohlenbach , 2008, Teoria della dimostrazione applicata , Springer.
• John Myhill , 1973, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", in A. Mathias e H. Rogers, Cambridge Summer School in Mathematical Logic , Lectures Notes in Mathematics v. 337, pp. 206-231, Springer.
• Michael Rathjen, 2005, " The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory ", Journal of Symbolic Logic , v. 70 n. 4, pagg. 1233–1254.
• Anne S. Troelstra , ed. (1973), Indagine metamatematica dell'aritmetica e dell'analisi intuizioniste , Springer.

link esterno

• Logica intuizionistica di Joan Moschovakis, Stanford Encyclopedia of Philosophy