Regola di inferenza della generalizzazione

[Salvy95]

Ciao a tutti,
sto studiando logica formale del Mendelson.
Nel capitolo del calcolo predicativo mi sono imbattuto nella seguente regola di inferenza:
A > (x)A(x)

Non riesco proprio a comprenderne il senso.

A può essere una generica formula ben formata con predicati, esempio (Mario è bello, Giancalo è bello, ..., etc.).
Troverei più sensato invertire la relazione e scrivere che
(x)A(x) > A, in quanto stavolta qualunque nome inerisse nell'universo dei termini del discorso verificherebbe A(x) (questo me lo garantisce il per ogni) e di conseguenza, a maggior ragione, un termine specifico (una costante) verificherebbe A.

Probabilmente c'è qualcosa di molto importante che mi sfugge.
Potreste aiutarmi?

Grazie!

[gugo82]

Probabilmente significa che in $(x)A(x)$ la variabile $x$ è fittizia.

Tanto per spiegare meglio: da $A=text("Mario è bello")$ ricavi $(x)A(x)=text("Mario è bello")$, un po' come dire che $A(x)$ è una funzione "costante" di $x$.

Poi, ovviamente, meglio aspettare qualcuno più addentro in queste questioni.

[kaspar]

Probabilmente significa che in $(x)A(x)$ la variabile $x$ è fittizia.

Immagino che con \((x)A(x)\) intenda \(\forall xA(x)\) o varianti simili...

Probabilmente c'è qualcosa di molto importante che mi sfugge.

Sì, perché qui

Troverei più sensato invertire la relazione e scrivere che
(x)A(x) > A, in quanto stavolta qualunque nome inerisse nell'universo dei termini del discorso verificherebbe A(x) (questo me lo garantisce il per ogni) e di conseguenza, a maggior ragione, un termine specifico (una costante) verificherebbe A.

stai parlando dell'istanziazione universale, ovvero \(\forall x A(x) \to A(\_)\) (l'underscore \(\_\) è uno stratagemma per per dirti «mettici un qualsiasi oggetto dell'universo del discorso e \(A\) è soddisfatta»). Quello che qui invece ti si voleva spiegare è (in una simbologia più moderna, credo) \[\frac{\models A}{\models \forall x A(x)}.\] Adesso non so a che punto stia con gli studi e né conosco il testo di Mendelson e la sua simologia e impostazione, ma quello che ho scritto significa: se \(A\) è una formula valida (i.e. vera per ogni interpretazione di quella formula), pure \(\forall x A(x)\) lo è. E questo ci porta alla domanda: sai cos'è un'interpretazione di una formula, cosa un modello, cosa significa che una formula è vera in una interpretazione, cosa che è valida? Comunque sia se ne può dare una descrizione informale ed efficiente

Attenzione! La regola di generalizzazione non è una sorta di inversa per l'assioma 4 [i.e. la regola dell'istanziazione universale]. Se così fosse, il ruolo del quantificatore universale verrebbe annullato. [...] Nella premessa della regola di generalizzazione si dice che \(A(a)\) deve essere valido per una generica costante \(a\). Non stupisce perciò che da questa premessa si possa dedurre la validità di \(\forall x A(x)\) [...]

G. T. Bagni, D. Gorla, A. Labella, Introduzione alla logica e al linguaggio matematico. Insomma è quello che si fa in matematica nelle dimostrazioni: si fissano degli oggetti che, nella realtà, devono essere scelti arbitrariamente, devono essere qualsiasi.

[Salvy95]

Negli scorsi di giorni ero impossibilitato a rispondere a causa di un errore sul sito.
Ci riprovo. l'interpretazione io l'ho assimilata così:
Una f.bf. è costruita per induzione secondo precise regole sintattiche. Per definirne un significato semantico, tuttavia, è necessaria una interpretazione.
Si definiscano allora degli elementi in un dato insieme D.
Nel linguaggio della generica teoria T, le costanti individuali a, b, c, etc. sono l'ortografia di base per indicare gli elementi del succitato insieme.
Le variabili invece possono invece indicare un certo sottoinsieme degli elementi di D, o, al più, tutto D. (Voglio dire che le variabili possono assumere quei valori)
Le descrizioni definite, a mezzo dei funtori che sono il nome delle descrizioni, sono grafie del tipo f(t1, t2, tn), dove t1, ..., tn sono altre descrizioni definite, o costanti o variabili particolarizzate con la scrittura x/costante

Questo è l'universo dei termini.

Per quanto riguarda i predicati, l'interpretazione può avvenire "verbosamente" ma non è proprio precisa, oppure a mezzo di un insieme di n-uple ordinate che definiscono univocamente la relazione.

Se p è la lettera funzionale n-aria, p(t1, t2,..., tn) assume valore V se particolarizzando i termini t1, ..., tn la n-upla ordinata rientra nella definizione ostentiva della relazione, diversamente è F.

Questo è il linguaggio della interpretazione.

L'interpetazione è l'applicazione di queste regole.

Se l'applicazione di queste regole ad una f.b.f. restituisce vero, quella interpetazione è un modello per la f.b.f.

Se l'applicazione di queste regole alla congiunzione di tutti gli assiomi PROPRI di una teoria T restituisce vero, quella interpetazione è un modello per la teoria.
E' inutile considerare anche i 5 assiomi logici, perché sono veri a prescindere dalla interpetazione, in quanto anche se tutte le particolarizzazione delle metavariabili in essi contenute fosse F, il risultato, essendo tautologie, sarebbe comunque V.

L'ho formulato al volo, spero sia corretto...