Oggetti ben formatimodifica

Se una raccolta di oggetti (simboli e sequenze di simboli) deve essere considerata “ben formata”, deve esistere un algoritmo per determinare, fermandosi con una risposta “sì” o “no”, se l’oggetto è ben formato (in matematica un wff abbrevia la formula ben formata). Questo algoritmo, all’estremo, potrebbe richiedere (o essere) una macchina di Turing o una macchina equivalente a Turing che “analizza” la stringa di simboli presentata come” dati ” sul suo nastro; prima che una macchina universale di Turing possa eseguire un’istruzione sul suo nastro, deve analizzare i simboli per determinare l’esatta natura dell’istruzione e/o del dato codificato lì. In casi più semplici una macchina a stati finiti o un automa pushdown può fare il lavoro. Enderton descrive l’uso di “alberi” per determinare se una formula logica (in particolare una stringa di simboli con parentesi) è ben formata. Alonzo Chiesa 1934 descrive la costruzione di “formule” (ancora: sequenze di simboli) come scritto nel suo λ-calcolo mediante l’uso di una descrizione ricorsiva di come avviare una formula e quindi costruire sul simbolo di partenza usando concatenazione e sostituzione.

Esempio: Church ha specificato il suo λ-calcolo come segue (la seguente è la versione semplificata tralasciando le nozioni di variabile libera e vincolata). Questo esempio mostra come una teoria degli oggetti inizia con una specifica di un sistema di oggetti di simboli e relazioni (in particolare mediante l’uso della concatenazione di simboli):

(1) Dichiarare i simboli: {,}, (,), λ, più un numero infinito di variabili a, b, c, …, X, … (2) Definire formula: una sequenza di simboli (3) Definire la nozione di “formula ben formata” (wff) ricorsivamente a partire dalla “base” (3.i):

• (3.1) (basis) Una variabile x è un wff
• (3.2) Se F e X sono wff, allora {F} (X) è un wff; se x si verifica in F o X allora si dice che sia una variabile in {F} (X).
• (3.3) Se M è ben formato e x si verifica in M allora λx è un wff.

(4) Definire varie abbreviazioni:

• {F} abbrevia in F(X) se F è un singolo simbolo
• F {\displaystyle {{F}}}
  

  abbrevia in {F}(X,Y) o F(X,Y) se F è un singolo simbolo

• λx1λx2…] abbrevia in λx1x2…xn * M
• λab * a(b) abbrevia in 1
• λab•a(a (b)) abbrevia in 2, ecc.

(5) Definire la nozione di “sostituzione” della formula N per la variabile x in tutto M (Church 1936)

Oggetti indefiniti (primitivi) Edit

Alcuni oggetti possono essere “indefiniti” o “primitivi” e ricevere definizione (nei termini dei loro comportamenti) con l’introduzione degli assiomi.

Nel prossimo esempio, i simboli non definiti saranno { ※ ,},∫}. Gli assiomi descriveranno i loro comportamenti.

AxiomsEdit

Kleene osserva che gli assiomi sono costituiti da due insiemi di simboli: (i) gli oggetti non definiti o primitivi e quelli che sono precedentemente noti. Nell’esempio riportato di seguito, è conosciuto in precedenza il seguente sistema ( O, ※, ↀ, ∫ ) O che costituisce un insieme di oggetti (il “dominio”), ※ è un oggetto del dominio, ↀ e ∫ sono simboli per le relazioni tra gli oggetti, => indica il “SE” operatore logico, ε è il simbolo che indica “è un elemento dell’insieme O”, e “n” viene utilizzato per indicare un arbitrario elemento dell’insieme di oggetti O.

Dopo (i) una definizione di “stringa S” – un oggetto che è un simbolo ※ o simboli concatenati ※, or o∫, e (ii) una definizione di stringhe “ben formate” — (base) ※ e ↀS, ∫S dove S è una qualsiasi stringa, arrivano gli assiomi:

• ※ ※ =>※, in parole: “SE ↀ viene applicato all’oggetto ※ ALLORA l’oggetto ※ risultati.”
• ∫n ε O, in parole “SE ∫ viene applicato ad un oggetto arbitrario “n” in O ALLORA questo oggetto ∫n è un elemento di O”.
• εn ε O, “SE ↀ viene applicato all’oggetto arbitrario” n “in O ALLORA questo oggetto ↀn è un elemento di O”.
• ∫∫n => n, “SE applied viene applicato all’oggetto ∫ n ALLORA l’oggetto n risulta.”
• ∫ↀn => n, “SE ∫ viene applicato all’oggetto ↀn ALLORA l’oggetto n risulta.”

Quindi quale potrebbe essere l’interpretazione (prevista) di questi simboli, definizioni e assiomi?

Se definiamo ※ come “0”, ∫ come “successore” e ↀ come “predecessore” allora ↀ ※ => ※ indica “sottrazione corretta” (a volte designata dal simbolo∸, dove “predecessore” sottrae un’unità da un numero, quindi 0 1 1 = 0). La stringa ” ∫ ∫ n = > n ” indica che se prima il successore viene applicato a un oggetto arbitrario n e poi il predecessore ↀ viene applicato a ∫n, l’originale n risulta.”

Questo insieme di assiomi è “adeguato”? La risposta corretta sarebbe una domanda: “Adeguato per descrivere cosa, in particolare?”Gli assiomi determinano a quali sistemi, definiti dall’esterno della teoria, si applica la teoria.”(Kleene 1952: 27). In altre parole, gli assiomi possono essere sufficienti per un sistema ma non per un altro.

In effetti, è facile vedere che questo insieme di assiomi non è molto buono—infatti, è incoerente (cioè, produce risultati incoerenti, indipendentemente dalla sua interpretazione):

Esempio: Define ※ as 0, ∫※ as 1, and ↀ1 = 0. Dal primo assioma,※ ※ = 0, so ∫※ ※ = ∫0 = 1. Ma l’ultimo assioma specifica che per qualsiasi n arbitrario incluso ※ = 0, ∫ↀn => n, quindi questo assioma stabilisce che ∫ↀ0 => 0, non 1.

Osserva anche che l’insieme degli assiomi non specifica che ∫n n n. Oppure, ad eccezione del caso n=※, ↀn n n. Se dovessimo includere questi due assiomi avremmo bisogno di descrivere le nozioni intuitive “uguali” simboleggiate da = e non-uguali simboleggiati da ≠.