Completezza della Logica del primo ordine

[pnp1]

Salve a tutti.

Scrivo per chiedervi dei chiarimenti riguardo alla completezza della logica del primo ordine e i teoremi di incompletezza di Godel perché sento che sto facendo confusione.

Poiché inevitabilmente scriverò delle cavolate, divido tutto il discorso in punti, in modo che possiate facilmente indicarmi in quali punti sbaglio.

Dunque, Godel ha dimostrato la completezza della logica del primo ordine, e i teoremi di incompletezza.

(1) Detto in modo informale, il teorema di completezza ci dice che la logica del primo ordine è completa, ovvero è in grado di derivare ogni formula sintatticamente corretta che è logicamente vera.

(2) Il primo teorema di incompletezza ci dice che qualsiasi teoria T abbastanza espressiva da descrivere l'aritmetica non è completa, ovverosia esiste un enunciato in T che non può essere né dimostrato né confutato in T.

(3) Ma nel linguaggio del primo ordine è possibile esprimere l'aritmetica di Robinson, che come è scritto qui:
http://it.wikipedia.org/wiki/Aritmetica_di_Robinson
ricade nelle ipotesi dei teoremi di incompletezza di Godel, e dunque è incompleta.

Dunque c'è qualcosa che non capisco

(4) La logica del primo ordine è completa, ma una teoria esprimile con la logica del primo ordine è incompleta, sembra una contraddizione.

Indubbiamente sbaglio al punto (4), ma non capisco dove?

Qui:
http://it.wikipedia.org/wiki/Teorema_di ... G%C3%B6del
Lascia intendere che si tratti di un "differente significato di completezza", ma non riesco a capire bene.

In particolare:
(5)

Il Teorema di completezza di Gödel è un teorema fondamentale della logica matematica ottenuto dal logico Kurt Gödel nel 1929. Esso stabilisce una corrispondenza tra verità semantica e dimostrabilità logica nella logica del primo ordine.
[...]
I teoremi di incompletezza di Gödel, riferendosi ad un differente significato di completezza, mostrano come se una sufficientemente potente formalizzazione dell'aritmetica è consistente, allora esiste una formula F, dipendente dalla formalizzazione scelta, di cui non si può dimostrare la verità né di F, né della sua negazione.

Qualcuno potrebbe spiegarmi bene tutta la faccenda?

Vi ringrazio!