Domanda su Teorema di una teoria formale

[Lodosage]

Nelle mie dispense possiedo questa spiegazione:

Una teoria formale è definita quando sono fissati:
- un insieme di simboli (alfabeto),
- un insieme di stringhe privilegiate di simboli (f.b.f.),
- un insieme privilegiato di f.b.f. (assiomi o base della conoscenza) e
- un insieme di regole di riscrittura (o di inferenza) che in presenza di un certo insieme di f.b.f .
permetta di scriverne in modo algoritmico altre (inferite o dedotte dalle precedenti).

Data una teoria formale H (cioè specificati tutti gli insiemi precedentemente elencati), chiamiamo
dimostrazione nella teoria formale H una sequenza finita di f.b.f. che siano o assiomi o formule
dedotte dalle precedenti tramite le regole di inferenza, diciamo teorema della teoria una f.b.f. A (e
scriviamo |-H A) che sia l’ultima formula di una dimostrazione.

Dato un insieme G di f.b.f. diciamo che una formula A è (sintatticamente) deducibile in H da G (e
scriviamo G|-H A) se esiste una sequenza finita di f.b.f. che siano o assiomi o formule di G o formule
dedotte dalle precedenti tramite le regole di inferenza, la cui ultima formula sia A.
Un teorema di H è dunque una formula deducibile da un insieme vuoto di f.b.f.



Sinceramente non ho capito l'affermazione "Un teorema di H è dunque una formula deducibile da un insieme vuoto di f.b.f.", se è vero che un teorema della teoria è una f.b.f. ricavata da formule precedenti e assiomi, perché poi mi viene detto che un teorema di H è deducibile da un insieme vuoto di f.b.f. quando H per essere una teoria formale deve possedere "un insieme privilegiato di f.b.f."?

[40rob]

"Leoddio":Nelle mie dispense possiedo questa spiegazione:

Una teoria formale è definita quando sono fissati:
- un insieme di simboli (alfabeto),
- un insieme di stringhe privilegiate di simboli (f.b.f.),
- un insieme privilegiato di f.b.f. (assiomi o base della conoscenza) e
- un insieme di regole di riscrittura (o di inferenza) che in presenza di un certo insieme di f.b.f .
permetta di scriverne in modo algoritmico altre (inferite o dedotte dalle precedenti).

Data una teoria formale H (cioè specificati tutti gli insiemi precedentemente elencati), chiamiamo
dimostrazione nella teoria formale H una sequenza finita di f.b.f. che siano o assiomi o formule
dedotte dalle precedenti tramite le regole di inferenza, diciamo teorema della teoria una f.b.f. A (e
scriviamo |-H A) che sia l’ultima formula di una dimostrazione.

Dato un insieme G di f.b.f. diciamo che una formula A è (sintatticamente) deducibile in H da G (e
scriviamo G|-H A) se esiste una sequenza finita di f.b.f. che siano o assiomi o formule di G o formule
dedotte dalle precedenti tramite le regole di inferenza, la cui ultima formula sia A.
Un teorema di H è dunque una formula deducibile da un insieme vuoto di f.b.f.



Sinceramente non ho capito l'affermazione "Un teorema di H è dunque una formula deducibile da un insieme vuoto di f.b.f.", se è vero che un teorema della teoria è una f.b.f. ricavata da formule precedenti e assiomi, perché poi mi viene detto che un teorema di H è deducibile da un insieme vuoto di f.b.f. quando H per essere una teoria formale deve possedere "un insieme privilegiato di f.b.f."?

L'insieme di assiomi della teoria $H$ non hanno detto da nessuna parte che deve stare in $G$ (gli assiomi possono stare nella sequenza di cui parlano dopo) ed essendo $G$ un insieme può essere al limite anche vuoto. La formula finale $A$ della sequenza potrebbe essere ricavata anche soltanto da assiomi specifici della teoria $H$ e altre formule deducibili da questi, in tal caso sarebbe vera la relazione $G = \emptyset$, $G \vdash_H A$ (ma questo vale proprio in base alla loro definizione).
L'insieme vuoto a cui si riferiscono è $G$.

Usando un'analogia $G$ rappresenta una specie di serbatoio di emergenza di formule che può essere anche vuoto.
Se $G$ è vuoto in base alla loro definizione

"Dato un insieme $G$ di f.b.f. diciamo che una formula $A$ è (sintatticamente) deducibile in $H$ da $G$ (e scriviamo $G \vdash_H A$) se (e solo se) esiste una sequenza finita di f.b.f. che siano o assiomi o formule di $G$ o formule dedotte dalle precedenti tramite le regole di inferenza, la cui ultima formula sia $A$."

può esistere comunque questa sequenza che faccia valere la relazione $\emptyset \vdash_H A$ ma in questa sequenza (ad esempio $B_1,...B_n, A$) compaiono solo gli assiomi specifici di $H$ e le formule dedotte dalle precedenti tramite le regole di inferenza, la cui ultima formula è $A$.

[Lodosage]

Scusa se non ho ancora risposto ma ero impegnato per un altro esame.

Dunque le formule precedenti a cui si riferisce il primo paragrafo sarebbero gli assiomi già presenti in H, in questo modo una teoria di H è deducibile senza bisogno di fare appello a insiemi esterni ad H giusto?

Se è così avevo fatto male ad interpretare "un teorema di H è deducibile da un insieme vuoto di f.b.f.", io avevo capito che un teorema di H non è dedotto da nessuna fbf...