Vi prego di aiutarmi a uscirne fuori.

Non e' il primo post che piazzo sull'argomento.
Ora pero' credo di avere le idee piu' chiare e quindi, con
un po' di fortuna, questa volta un vostro aiuto sara' risolutivo.

Mi scuso per la poca rigorosita' delle affermazioni che seguono :
Sia L il linguaggio predicativo formale sufficiente a parlare di
aritmetica.  L e' la "macchina" che produce le fbf.
F l'insieme di tutte le fbf (enunciati ben formati) costruibili con L,
A l'insieme degli assiomi, che e' un sottoinsieme di F.

Sappiamo dal teorema di Godel che esistono fbf VERE che
non sono dimostrabili ALL'INTERNO  del sistema formale
detto sopra.
Benissimo.
La mia semplice domanda e' :
se non sono dimostrabili, come facciamo a sapere che sono
vere ?
----------------------------------------------------------------------------------------
Piccola digressione :
Ho letto questo esempio sul libro "la prova di Godel"
di Newmann.
supponiamo di avere un gruppo di assiomi tramite i
quali si costruisce una figura piana, ad esempio un triangolo.
Il triangolo e' un "modello" degli assiomi.
Ora e' chiaro che puo' esistere qualche proprieta' di questo
triangolo OSSERVABILE nel senso letterale del termine,
(ad esempio che ha 2 angoli acuti) quindi VERA nel
modello.
Supponiamo ora di sapere che questa proprieta' sia comune A TUTTI i
possibili modelli costruibili con gli assiomi dati.
E siano questi in NUMERO FINITO, quindi controllabili uno
per uno.
Essa allora e' VERA nel sistema formale !
Bene. Tuttavia potrebbe verificarsi il caso che questa proprieta'
non sia DERIVABILE a partire dagli assiomi.
Ma io so che e' vera lo stesso, per altra via. Per "osservazione"
diretta. La vedo !

Ma :
se i modelli costruibili sono infiniti ?
Come si fa a controllare che una fbf e' VERA, visto che
con la dimostrazione non la si "acchiappa" ?!?

Capite il mio cruccio ?