Sistema di assiomi + assioma

nato_pigro1
In generale, se a un sistema di assiomi (coerente) aggiungo un'altro assioma (indipendente dagli altri per cui risulti ancora coerente la mia teoria) la completezza, o la vastità o il "numero di teoremi" della mia teoria (non so bene come chiamarla...) aumenta o diminuisce?
Banalmente se di una proposizione non derivabile dagli assiomi ne faccio un assioma ecco che la mia teoria si allarga.

Per esempio l'assiomatizzazione proposta da Hilber per la geometria euclidea aggiunge alcuni assiomi ed "allarga" la teoria, ma è sempre così? o c'è un limite?

Risposte
fields1
Un sistema di assiomi è "potenziabile", rispetto all'insieme dei teoremi dimostrabili, se e solo se non è completo.

nato_pigro1
ok. Alcune domande.

Ciò significa che se ho un sistema di assiomi completo non è possibile aggiungere un altro assioma (che non sia già un teorema) senza compometterne la coerenza?

L'assiomatizzazione di hilbert della geometria è completa?

Non sono riuscito bene a capire la differenza tra verità e dimostrabilità. Un sistema di assiomi di può dire completo quando di ogni proposizione $P$ si può dire se è vera o falsa, cioè se è possibile ricavare $P$ o $nonP$ all'interno della teoria. Ma dunque il concetto di verità coincide con quella di dimostrabilità?
Credo proprio di no, altrimenti sarebbe come dire che ogni sistema è completo, nel senso che dimostra tutto ciò che è vero perchè è vero ciò che riesce a dimostrare.
Però non riesco a coglierne la differenza...

fields1
"nato_pigro":
Ciò significa che se ho un sistema di assiomi completo non è possibile aggiungere un altro assioma (che non sia già un teorema) senza compometterne la coerenza?


Esatto

"nato_pigro":


L'assiomatizzazione di hilbert della geometria è completa?



Il sistema originale di Hilbert non è formalizzabile nella logica del prim'ordine; ha bisogno di appoggiarsi sulla teoria degli insiemi, quindi non è una teoria a sè stante.

La geometria euclidea piana è completa nella assiomatizzazione data da Tarski.

"nato_pigro":

Non sono riuscito bene a capire la differenza tra verità e dimostrabilità. Un sistema di assiomi di può dire completo quando di ogni proposizione $P$ si può dire se è vera o falsa, cioè se è possibile ricavare $P$ o $nonP$ all'interno della teoria. Ma dunque il concetto di verità coincide con quella di dimostrabilità?
Credo proprio di no, altrimenti sarebbe come dire che ogni sistema è completo, nel senso che dimostra tutto ciò che è vero perchè è vero ciò che riesce a dimostrare.
Però non riesco a coglierne la differenza...


Un sistema di assiomi e' completo se dimostra, per ogni proposizione $P$, o $P$ o $\not P$. La verita' non c'entra.

nato_pigro1
"fields":

La geometria euclidea piana è completa nella assiomatizzazione data da Tarski.


ma se l'assiomatizzazione di tarski è completa, allora, per il primo teorema di incompletezza la teoria non può essere così vasta da contenere l'aritmentica, quindi in qualche modo l'aggiunta di assiomi non potenzia la teoria?

"nato_pigro":

Non sono riuscito bene a capire la differenza tra verità e dimostrabilità. Un sistema di assiomi di può dire completo quando di ogni proposizione $P$ si può dire se è vera o falsa, cioè se è possibile ricavare $P$ o $nonP$ all'interno della teoria. Ma dunque il concetto di verità coincide con quella di dimostrabilità?
Credo proprio di no, altrimenti sarebbe come dire che ogni sistema è completo, nel senso che dimostra tutto ciò che è vero perchè è vero ciò che riesce a dimostrare.
Però non riesco a coglierne la differenza...


Un sistema di assiomi e' completo se dimostra, per ogni proposizione $P$, o $P$ o $\not P$. La verita' non c'entra.[/quote]

ok, ma la forma della proposizione $P$ quali requisiti deve avere? nel senso: io non posso pretendere che la geometria mi dimostri se la proposizione "le banane sono gialle" è vera o falsa. $P$ deve parlare di concetti geometrici, ma se i concetti geometrici non sono definiti, ma sono concetti le cui proprietà discendono dagli assiomi, allora come faccio a dire che quel sistema di assiomi non riesce a dimostrare qualche enenciato $P$?
Faccio un esempio: con l'assiomatizzazione di Euclide si è visto che non si poteva dimostrare che dato un punto interno a un triangolo e un punto esterno il segmento che li unisce interseca il triangolo, quindi è un sistema di assiomi incompleto. Ma questo non significa ammettere che abbiamo già un'idea di cosa devono essere i concetto di "intersecare" e "interno e esterno" e che questi concetti non li discendiamo dagli assiomi?
Invece di dire che la teoria è incompleta non si può dire che l'universo di quella teoria non comprende i concetti di interno ed esterno? che è come se stessimo parlando di banane?

(chiaramente non credo che sia così, solo la forma interrogativa è un modo per esprimere dei dubbi, non per proporre qualcosa).

fields1
"nato_pigro":


ma se l'assiomatizzazione di tarski è completa, allora, per il primo teorema di incompletezza la teoria non può essere così vasta da contenere l'aritmentica, quindi in qualche modo l'aggiunta di assiomi non potenzia la teoria?


Non puoi aggiungere assiomi dell'aritmetica. Non sarebbero scritti nel linguaggio adatto (vedi sotto)


"nato_pigro":

ok, ma la forma della proposizione $P$ quali requisiti deve avere? nel senso: io non posso pretendere che la geometria mi dimostri se la proposizione "le banane sono gialle" è vera o falsa. $P$ deve parlare di concetti geometrici, ma se i concetti geometrici non sono definiti, ma sono concetti le cui proprietà discendono dagli assiomi, allora come faccio a dire che quel sistema di assiomi non riesce a dimostrare qualche enenciato $P$?
Faccio un esempio: con l'assiomatizzazione di Euclide si è visto che non si poteva dimostrare che dato un punto interno a un triangolo e un punto esterno il segmento che li unisce interseca il triangolo, quindi è un sistema di assiomi incompleto. Ma questo non significa ammettere che abbiamo già un'idea di cosa devono essere i concetto di "intersecare" e "interno e esterno" e che questi concetti non li discendiamo dagli assiomi?
Invece di dire che la teoria è incompleta non si può dire che l'universo di quella teoria non comprende i concetti di interno ed esterno? che è come se stessimo parlando di banane?


Per capire la risposta a questa domanda dovresti sapere che cos'è un linguaggio formale. Ora, gli assiomi della geometria sono scritti usando certi simboli, combinati opportunamente secondo una prescritta sintassi. Ogni stringa ben formata (i.e. sintatticamente corretta) composta dai suddetti simboli è una proposizione della geometria. Allora il sistema di Tarski dimostra, per ogni proposizione della geometria, o lei oppure la sua negazione.

nato_pigro1
ho idea di cosa sia un linguaggio formale. Il mio discorso si inseriva proprio all'interno della visione formalistica.

Io non parlavo degli assiomi dell'aritmetica.
Il primo teorema di incompletezza recita:
In ogni teoria matematica $T$ sufficientemente espressiva da contenere l'aritmetica, se $T$ è coerente, esiste una proposizione $P$ per cui non è possibile dire se è vera o falsa.
Il mio riferimento all'aritmetica si riferiva al fatto che se l'assiomatizzazione della geometria di Tarski è completa (e coerente) allora non può essere sufficientemente espressiva da contentenere l'aritmentica, quindi è meno espressiva della geometria, mettiamo, di Euclide. Quindi è completa ma meno espressiva? [punto 1 che non capisco].

Riguardo al discorso della sintassi.
Prendiamo l'esempio di Hofstadter nel GEB, il gioco MU. Il sistema formale all'interno del quale si svolge è il sistema "MIU" nel senso che usa quei simboli. Abbiamo un assioma ("MI") e delle regole. Si può dimostrare che la stringa "MU" non è un teorema del sistema. Cosa si dice dunque del sistema MIU? che è incompleto perchè MU (che è una stringa ben formata) non è un teorema. E' corretto? [per favore rispondi, non vorrei iniziare un discorso partendo da presupposti sbagliati]
Inoltre, stringhe come "UUUM", "IIMUUI" o altre cosa sarebbero? rispettano o no la prescritta sintassi? [rispondi anche qui, per favore, almeno mi chiarisco le idee e poi proseguo :)]

fields1
"nato_pigro":
Io non parlavo degli assiomi dell'aritmetica.
Il primo teorema di incompletezza recita:
In ogni teoria matematica $T$ sufficientemente espressiva da contenere l'aritmetica, se $T$ è coerente, esiste una proposizione $P$ per cui non è possibile dire se è vera o falsa.
Il mio riferimento all'aritmetica si riferiva al fatto che se l'assiomatizzazione della geometria di Tarski è completa (e coerente) allora non può essere sufficientemente espressiva da contentenere l'aritmentica, quindi è meno espressiva della geometria, mettiamo, di Euclide. Quindi è completa ma meno espressiva? [punto 1 che non capisco].


Sì, la geometria assiomatizzata da Tarski non è abbastanza espressiva da rappresentare l'aritmetica. Le ragioni? Quelle che hai detto tu (sostituendo il concetto di verità con quello di dimostrabilità, come ti ho detto sopra).

Ad ogni modo, la geometria di Euclide è una teoria informale, quindi non è suscettibile di un'analisi matematica rigorosa. Sicché, confrontarne l'espressività con un sistema formale, non è un modo di procedere matematico. In generale, quando uno assiomatizza una teoria informale (ad esempio, la teoria degli insiemi), come fa a sapere se la teoria assiomatizzata è abbastanza vicina a quella "intuitiva" originale?


"nato_pigro":

Prendiamo l'esempio di Hofstadter nel GEB, il gioco MU. Il sistema formale all'interno del quale si svolge è il sistema "MIU" nel senso che usa quei simboli. Abbiamo un assioma ("MI") e delle regole. Si può dimostrare che la stringa "MU" non è un teorema del sistema. Cosa si dice dunque del sistema MIU? che è incompleto perchè MU (che è una stringa ben formata) non è un teorema. E' corretto? [per favore rispondi, non vorrei iniziare un discorso partendo da presupposti sbagliati]
Inoltre, stringhe come "UUUM", "IIMUUI" o altre cosa sarebbero? rispettano o no la prescritta sintassi? [rispondi anche qui, per favore, almeno mi chiarisco le idee e poi proseguo :)]



La sintassi è: una proposizione è una sequenza finita arbitraria composta dai simboli M, I, U.

Il problema è che qui non si può parlare di completezza, perché non c'è il simbolo per la negazione. Ad ogni modo, per non rimanere impiantati :| , supponiamo di interpretare M come negazione. Allora diremo che MIU è completo se per ogni stringa S, MIU dimostra MS o S. In questo caso MIU è incompleto: non dimostra né MU né U.

nato_pigro1
"fields":
[quote="nato_pigro"]Io non parlavo degli assiomi dell'aritmetica.
Il primo teorema di incompletezza recita:
In ogni teoria matematica $T$ sufficientemente espressiva da contenere l'aritmetica, se $T$ è coerente, esiste una proposizione $P$ per cui non è possibile dire se è vera o falsa.
Il mio riferimento all'aritmetica si riferiva al fatto che se l'assiomatizzazione della geometria di Tarski è completa (e coerente) allora non può essere sufficientemente espressiva da contentenere l'aritmentica, quindi è meno espressiva della geometria, mettiamo, di Euclide. Quindi è completa ma meno espressiva? [punto 1 che non capisco].


Sì, la geometria assiomatizzata da Tarski non è abbastanza espressiva da rappresentare l'aritmetica. Le ragioni? Quelle che hai detto tu (sostituendo il concetto di verità con quello di dimostrabilità, come ti ho detto sopra).

Ad ogni modo, la geometria di Euclide è una teoria informale, quindi non è suscettibile di un'analisi matematica rigorosa. Sicché, confrontarne l'espressività con un sistema formale, non è un modo di procedere matematico. In generale, quando uno assiomatizza una teoria informale (ad esempio, la teoria degli insiemi), come fa a sapere se la teoria assiomatizzata è abbastanza vicina a quella "intuitiva" originale? [/quote]

Rispondendo alla tua domanda arriviamo al punto a cui volevo arrivare, e cioè che il formalismo magari è rispettato nella forma (scusa il gioco di parole) ma non nella sostanza. Nel senso che una teoria non dovrebbe proporsi di descrivere il mondo o un'idea intuitiva (parlo con le parole dei formalisti più radicali) ma è semplicemente una successione di simboli senza significato, e dunque non c'è la pretesa di avvicinarsi all'idea intuitiva. Io propongo una serie di assiomi e questi mi possono produrre una serie di teoremi (altre stringhe), le stringhe producibili sono la mia realtà, nulla altro.


"fields":
[quote="nato_pigro"]
Prendiamo l'esempio di Hofstadter nel GEB, il gioco MU. Il sistema formale all'interno del quale si svolge è il sistema "MIU" nel senso che usa quei simboli. Abbiamo un assioma ("MI") e delle regole. Si può dimostrare che la stringa "MU" non è un teorema del sistema. Cosa si dice dunque del sistema MIU? che è incompleto perchè MU (che è una stringa ben formata) non è un teorema. E' corretto? [per favore rispondi, non vorrei iniziare un discorso partendo da presupposti sbagliati]
Inoltre, stringhe come "UUUM", "IIMUUI" o altre cosa sarebbero? rispettano o no la prescritta sintassi? [rispondi anche qui, per favore, almeno mi chiarisco le idee e poi proseguo :)]



La sintassi è: una proposizione è una sequenza finita arbitraria composta dai simboli M, I, U.

Il problema è che qui non si può parlare di completezza, perché non c'è il simbolo per la negazione. Ad ogni modo, per non rimanere impiantati :| , supponiamo di interpretare M come negazione. Allora diremo che MIU è completo se per ogni stringa S, MIU dimostra MS o S. In questo caso MIU è incompleto: non dimostra né MU né U.[/quote]

Dunque una stringa come "MU" rispetta la sintassi ma non è un teorema del sistema MIU. L'incompletezza del sistema deriva in qualche modo da un'idea di sintassi precedente agli assiomi e alle regole di inferenza. Se però la mia realtà sono quelle stringhe producibili e basta (come dicono i formalisti), se quando sono all'interno di un sistema formale io ho solo assiomi e regole e trasformo simboli a partire da quelli allora l'incompletezza del sistema discende da un qualcosa esterno al sistema, la sintassi appunto.
Tu prima parlavi di un "prescritta sintassi", dunque un sistema formale non è fatto solo di assiomi e regole di inferenza?

fields1
"nato_pigro":


Rispondendo alla tua domanda arriviamo al punto a cui volevo arrivare, e cioè che il formalismo magari è rispettato nella forma (scusa il gioco di parole) ma non nella sostanza. Nel senso che una teoria non dovrebbe proporsi di descrivere il mondo o un'idea intuitiva (parlo con le parole dei formalisti più radicali) ma è semplicemente una successione di simboli senza significato, e dunque non c'è la pretesa di avvicinarsi all'idea intuitiva. Io propongo una serie di assiomi e questi mi possono produrre una serie di teoremi (altre stringhe), le stringhe producibili sono la mia realtà, nulla altro.



E' una posizione del tutto legittima. E' ragionevole affermare che un formalista estremo non dovrebbe occuparsi null'altro che di stringhe. Ma usare i sistemi formali e concepirli come unico modo rigoroso di fare matematica, non implica certo l'essere un formalista estremo.


"nato_pigro":

Dunque una stringa come "MU" rispetta la sintassi ma non è un teorema del sistema MIU. L'incompletezza del sistema deriva in qualche modo da un'idea di sintassi precedente agli assiomi e alle regole di inferenza. Se però la mia realtà sono quelle stringhe producibili e basta (come dicono i formalisti), se quando sono all'interno di un sistema formale io ho solo assiomi e regole e trasformo simboli a partire da quelli allora l'incompletezza del sistema discende da un qualcosa esterno al sistema, la sintassi appunto.
Tu prima parlavi di un "prescritta sintassi", dunque un sistema formale non è fatto solo di assiomi e regole di inferenza?


Sono d'accordo. Certamente la sintassi ha un ruolo formale fondamentale nel definire la completezza; essa è matematicamente sufficiente - ed è tutto. Poi è chiaro che è più che altro l'idea semantica di verità a giustificare il concetto sintattico di completezza. Perché altrimenti non definire il concetto di completezza ad esempio così: il tal sistema è completo se per ogni intero positivo $n$ dispari le proposizioni di lunghezza $n^n$ sono derivabili.

Per quanto riguarda la logica standard, formalmente ci sono solo assiomi e regole di inferenza. Certamente se il tuo sistema comprende assiomi sintatticamente "illegali" (i.e. non adatti alla logica del prim'ordine), sarà probabile che nessuno lo consideri :-D La sintassi serve per un analisi "esterna" dei sistemi logici.

nato_pigro1
ok, grazie per la profiqua chiaccherata.
:-D

Sk_Anonymous
Un assioma è un qualcosa che si preferisce non dimostrare oppure che è IMPOSSIBILE da dimostrare?
Io propendo per la seconda, infatti da quello che ho capito un assioma dovrebbe essere fatto da termini primitivi, dai quali dunque non si può cavare nient'altro che essi stessi, rendendo dunque impossibile la dimostrazione.

Dreamphiro
Scusate la domanda, non ho letto tutte le risposte, ma cosa significa ''sufficientemente espressiva da contenere l'aritmetica''? Cosa vuol dire ''contenere l'aritmetica''?

Caenorhabditis
"lisdap":
Un assioma è un qualcosa che si preferisce non dimostrare oppure che è IMPOSSIBILE da dimostrare?

La possibilità o l'impossibilità di dimostrare qualcosa dipendono dall'elenco degli assiomi. Di solito si preferisce, per ragioni di economia, avere un set di assiomi tra loro indipendenti, cioè che ognuno di loro non sia dimostrabile a partire dagli altri.
"Dreamphiro":
Scusate la domanda, non ho letto tutte le risposte, ma cosa significa ''sufficientemente espressiva da contenere l'aritmetica''? Cosa vuol dire ''contenere l'aritmetica''?

Che puoi rappresentare un enunciato dell'aritmetica (es. "i numeri primi congrui ad 1 modulo 4 sono esprimibili come somma di due quadrati" oppure "tutti i numeri sono pari") mediante una formula di quel sistema.

Sk_Anonymous
Ma un assioma è una proposizione fatta da termini primitivi?
Alla base della versione della matematica con la teoria degli insiemi elaborata da ZF ci sono dei concetti primitivi?
Se si quali sono?

Caenorhabditis
"lisdap":
Ma un assioma è una proposizione fatta da termini primitivi?

Un sistema formale è fatto da:
    [*:2fmjsdfb]Un elenco di simboli, per esempio $a$, $k$, $s$ e $w$[/*:m:2fmjsdfb]
    [*:2fmjsdfb]Una lista di assiomi, cioè di stringhe formate da tali simboli e considerate "vere" (per esempio, potremmo convenire che "$askaawa$" sia l'unico assioma di questa teoria-esempio.[/*:m:2fmjsdfb]
    [*:2fmjsdfb]Delle regole di inferenza, cioè dei criteri che permettono di ricavare formule "vere" da altre formule "vere" (es.: se $XkY$ allora $YX$, per qualunque coppia di stringhe $X$ e $Y$; se $Xas$ allora $wX$, per qualunque $X$.[/*:m:2fmjsdfb][/list:u:2fmjsdfb]

    Dimostrerò ora il seguente teorema: $waawa$
    $askaawa$ [assioma 1]
    $aawaas$ [regola d'inferenza 1]
    $waawa$ [regola d'inferenza 2]
    C.V.D.

    Zermelo-Fraenkel funziona allo stesso modo, soltanto che ha più simboli e le sue regole d'inferenza sono un pochettino più complicate, e ha molti più assiomi: tutti quelli della logica proposizionale, che ZF include, più altri riferiti a simboli che interpretiamo come riferiti agli insiemi.

Sk_Anonymous
"Caenorhabditis":
[quote="lisdap"]Ma un assioma è una proposizione fatta da termini primitivi?

Un sistema formale è fatto da:
    [*:b6oywt4y]Un elenco di simboli, per esempio $a$, $k$ e $w$[/*:m:b6oywt4y]
    [*:b6oywt4y]Una lista di assiomi, cioè di stringhe formate da tali simboli e considerate "vere" (per esempio, potremmo convenire che "$askaawa$" sia l'unico assioma di questa teoria-esempio.[/*:m:b6oywt4y]
    [*:b6oywt4y]Delle regole di inferenza, cioè dei criteri che permettono di ricavare formule "vere" da altre formule "vere" (es.: se $XkY$ allora $YX$, per qualunque coppia di stringhe $X$ e $Y$; se $Xas$ allora $wX$, per qualunque $X$.[/*:m:b6oywt4y][/list:u:b6oywt4y]

    Dimostrerò ora il seguente teorema: $waawa$
    $askaawa$ [assioma 1]
    $aawaas$ [regola d'inferenza 1]
    $waawa$ [regola d'inferenza 2]
    C.V.D.

    Zermelo-Fraenkel funziona allo stesso modo, soltanto che ha più simboli e le sue regole d'inferenza sono un pochettino più complicate, e ha molti più assiomi: tutti quelli della logica proposizionale, che ZF include, più altri riferiti a simboli che interpretiamo come riferiti agli insiemi.[/quote]
    Da pazzi :-D
    Umm, quindi nella teoria di ZF non ci sono concetti primitivi?

Caenorhabditis
"lisdap":

Umm, quindi nella teoria di ZF non ci sono concetti primitivi?

Puoi benissimo vedere ZF, in quanto sistema formale, come una serie di stringhe da cui puoi ottenere altre stringhe con determinate regole. I "concetti primitivi" sono le interpretazioni che, convenzionalmente, si danno a determinati simboli o gruppi di simboli. Nota che l'interpretazione non è univoca: ad esempio, se cerchi "dualità" dovresti poter trovare qualche esempio di come, in alcune teorie, scambiando alcuni abbinamenti simbolo-concetto si ottiene una teoria virtualmente indistinguibile da quella originaria.

Sk_Anonymous
"Caenorhabditis":
[quote="lisdap"]Ma un assioma è una proposizione fatta da termini primitivi?

Un sistema formale è fatto da:
    [*:27n1wiev]Un elenco di simboli, per esempio $a$, $k$ e $w$[/*:m:27n1wiev]
    [*:27n1wiev]Una lista di assiomi, cioè di stringhe formate da tali simboli e considerate "vere" (per esempio, potremmo convenire che "$askaawa$" sia l'unico assioma di questa teoria-esempio.[/*:m:27n1wiev]
    [*:27n1wiev]Delle regole di inferenza, cioè dei criteri che permettono di ricavare formule "vere" da altre formule "vere" (es.: se $XkY$ allora $YX$, per qualunque coppia di stringhe $X$ e $Y$; se $Xas$ allora $wX$, per qualunque $X$.[/*:m:27n1wiev][/list:u:27n1wiev]

    Dimostrerò ora il seguente teorema: $waawa$
    $askaawa$ [assioma 1]
    $aawaas$ [regola d'inferenza 1]
    $waawa$ [regola d'inferenza 2]
    C.V.D.

    Zermelo-Fraenkel funziona allo stesso modo, soltanto che ha più simboli e le sue regole d'inferenza sono un pochettino più complicate, e ha molti più assiomi: tutti quelli della logica proposizionale, che ZF include, più altri riferiti a simboli che interpretiamo come riferiti agli insiemi.[/quote]
    Ciao, grazie! Volevo farti notare che nell'assioma che hai scritto c'è la $s$ che però non è inclusa fra i simboli che hai scelto. Ciao

Sk_Anonymous
"Caenorhabditis":
[quote="lisdap"]
Umm, quindi nella teoria di ZF non ci sono concetti primitivi?

Puoi benissimo vedere ZF, in quanto sistema formale, come una serie di stringhe da cui puoi ottenere altre stringhe con determinate regole. I "concetti primitivi" sono le interpretazioni che, convenzionalmente, si danno a determinati simboli o gruppi di simboli. Nota che l'interpretazione non è univoca: ad esempio, se cerchi "dualità" dovresti poter trovare qualche esempio di come, in alcune teorie, scambiando alcuni abbinamenti simbolo-concetto si ottiene una teoria virtualmente indistinguibile da quella originaria.[/quote]
Aggiungo un'altra cosa...mi sei stato di grande aiuto. Volevo chiederti: una volta che nel mio sistema formale ho scelto un insieme di simboli, ad esempio $l,m,n$, posso iniziare a dare definizioni (per esempio, scrivo asdasdas:=ln?)

Caenorhabditis
"lisdap":

Volevo farti notare che nell'assioma che hai scritto c'è la $s$ che però non è inclusa fra i simboli che hai scelto.

Corretto, chiedo scusa.
"lisdap":

Aggiungo un'altra cosa...mi sei stato di grande aiuto. Volevo chiederti: una volta che nel mio sistema formale ho scelto un insieme di simboli, ad esempio $l,m,n$, posso iniziare a dare definizioni (per esempio, scrivo asdasdas:=ln?)

Ogni volta che dai una definizione, tecnicamente stai passando ad un nuovo sistema formale (l"estensione per definizione" è un tipo particolare di estensione conservativa), uguale al precedente in tutto tranne che nella definizione che hai incorporato.

Rispondi
Per rispondere a questa discussione devi prima effettuare il login.