Qual è la definizione di una definizione?
Nella logica matematica o in altri sistemi formali, qual è la definizione di una definizione, formalmente?
Se "A" è definito come "B", qual è la definizione di "A"? Coinvolge sia "A" che "B" (es. "A: = B") o solo "B"?
Ad esempio, a p126 in §3. Estensioni per definizioni in VIII Interpretazioni sintattiche e forme normali nella logica matematica di Ebbinghaus , supponiamo che$S$ è un set di simboli (non logici),
3.1 Definizione. Permettere$\Phi$ essere un insieme di $S$-frasi.
(a) Supponiamo $P \notin S$ è un $n$-ary relazione simbolo e $\phi_P(v_0, ... , v_{n-1})$ un $S$-formula. Allora lo diciamo$$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ è un $S$-definizione di $P$ in $\Phi$.
Che chiamerò come un $S$-definizione di $P$ in $\Phi$:
$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?
È circolare da definire $P$ in termini di sé?
È un $𝑆$-definizione di $𝑃$ in $Φ$ un'interpretazione del simbolo $P$ come un $S'$-frase? (come parte di un'interpretazione sintattica di$S'$ in $S'$ si?)
È l'aspetto di $P$ nella sua stessa definizione $∀ 𝑣_0,....∀ 𝑣_{𝑛−1}(𝑃𝑣_0...v_{𝑛−1}↔𝜙_𝑃(𝑣_0,...,𝑣_{𝑛−1}))$, nello stesso senso della comparsa di $A$ in $𝐴:=𝐵$?
$\phi_P(v_0, ... , v_{n-1})) $? (Immagino che$P$ è definito come $\phi_P(v_0, ... , v_{n-1})) $ in $\Phi$.)
$\phi_P$? (Confronta questo con il secondo:$P$ di per sé non coinvolge variabili)
Vedere In che modo questa definizione definisce un simbolo$P$ al di fuori del set di simboli $S$ come un $S$-frase?
Grazie.
Risposte
Abbiamo una firma $S$ e lo estendiamo a $S':=S\cup\{P\}$.
Il $S$-definizione di $P$ è il $S'$-formula $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$che può essere formalmente trattato come un assioma in più rispetto al dato$S$-la teoria con cui stiamo lavorando, producendo così un equivalente $S'$-la teoria, in cui il simbolo $P$può essere utilizzato come abbreviazione della formula$\phi_P$.
Ad esempio, la formula seguente è la definizione della solita relazione di ordinamento $\le$ di numeri interi non negativi nella lingua $(0,+)$: $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
Di seguito cercherò prima di descrivere il processo in modo più intuitivo, quindi affronterò le tue preoccupazioni sulla circolarità. Sospetto che quest'ultimo punto possa effettivamente essere più utile, quindi sentiti libero di leggere prima la seconda sezione - e in particolare, penso che il motto evidenziato sarà molto utile.
(Ri: il tuo commento finale, la definizione è $(1)$- la cosa che ti dice come si comporta il nuovo simbolo, in termini di vecchi simboli che già hai e comprendi.)
La frase chiave qui è " espansione per definizioni ".
Intuitivamente, abbiamo in mente il seguente processo:
A partire da una firma $S$ e alcuni set $\Phi$ di $S$-sentenze, diventiamo un po 'infastiditi dalle inefficienze : ci sono alcune cose di cui possiamo parlare usando$S$-formule ma solo in modo indiretto. Pensa ad esempio al linguaggio della teoria degli insiemi,$\{\in\}$: possiamo esprimere cose come "$x$ è il prodotto cartesiano di $y$ e $z$"in questa lingua, ma solo tramite formule fastidiosamente lunghe (è un buon esercizio per gestire l'esempio precedente, utilizzando, ad esempio, le coppie Kuratowski).
Quindi data la nostra formula davvero complicata $\varphi(x_0,...,x_{n-1})$, vogliamo elaborare una nuova teoria che è fondamentalmente la stessa di $\Phi$ tranne per il fatto che ha anche una "abbreviazione" per $\varphi$.
In primo luogo, questo significa che vogliamo ampliare la nostra lingua: piuttosto che lavorare con $S$ con cui vogliamo lavorare $S\cup\{R\}$ per alcuni $n$-simbolo di relazione parziale $R\not\in S$ che intendiamo servire come abbreviazione di $\varphi$.
Ora dobbiamo definire una teoria in questo linguaggio più ampio. Questa teoria dovrebbe sussumere ciò che già abbiamo (cioè,$\Phi$), dovrebbe dettare correttamente il comportamento di $R$ (cioè, diciamo che è un'abbreviazione di $\varphi$) e non dovrebbe fare nient'altro. Questo ci porta a considerare la nuova teoria$$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
Il passaggio da $S,\Phi$, e $\varphi$ per $S\cup\{R\}$ e $\Phi'$è un'espansione per definizioni . Abbiamo qualche grave ridondanza qui: in un senso preciso,$\Phi'$ non è davvero migliore di $\Phi$. (Formalmente,$\Phi'$è un'estensione conservativa di$\Phi$ nel senso più forte possibile: ogni modello di $\Phi$ ha esattamente un'espansione a un modello di $\Phi'$.) Questo non è sorprendente. Noi sapevamo già che potremmo esprimere la cosa che importava via$\varphi$, volevamo solo essere in grado di farlo più rapidamente.
Per inciso, nota che questo suggerisce una versione naturale "massimamente efficiente" di qualsiasi teoria: aggiungi semplicemente nuovi simboli per ogni formula! Questo si chiama morleyizzazione ed è occasionalmente utile (anche se di solito è un po 'sciocco ).
OK, ora che dire della circolarità che ti preoccupa?
Innanzitutto, tieni presente che "$R$"di per sé è solo un simbolo. La nuova frase che stiamo aggiungendo non è realmente una definizione di $R$, ma piuttosto una definizione del significato di $R$, o se preferisci una regola che disciplini il comportamento di$R$.
Più seriamente, la circolarità non è mai un problema in FOL! L'idea chiave è la seguente, che credo sia un importante allontanamento dalle intuizioni che si potrebbero portare dalla programmazione:
Un insieme di frasi del primo ordine non crea cose, descrive cose.
Nello specifico, una serie di frasi di primo ordine $\Phi$si ritaglia una particolare classe di strutture, quelle di cui è una descrizione accurata. Ad esempio, i set dall'aspetto potenzialmente pericoloso$$\{\forall x(P(x)\leftrightarrow P(x))\}$$ e $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$sono perfettamente senza cerchi; sono solo vuoti (= presa di ogni struttura) e contraddittori (= presa di nessuna struttura) rispettivamente.