Teorema di compattezza

• Sia 𝛤 una teoria, eventualmente infinita, per qualche linguaggio L. Allora:
  • Se ogni sottoinsieme finito di 𝛤 ha un modello, allora anche 𝛤 stesso ha un modello

Teorema di semidecidibilità

• Il teorema di validità e completezza (semantico) sancisce che se Q è una verità logica allora posso algoritmicamente stabilire che lo è, infatti Q è una verita logica se e solo se è dimostrabile in ℱ

  • Elencando le prove una ad una, prima o poi trovo quella che mostra che Q è un teorema (dimostrato senza premesse).

• Il teorema di semidecidibilità invece prova che non vi può essere un metodo algoritmico per elencare gli enunciati Q che non sono verità logiche.

  • Se ci fosse un tale algoritmo potrei decidere, per ogni enunciato Q, se è una verità logica o no
    • Si elencano tutte le prove, una dopo l'altra
    • Si elencherebbero in parallelo tutte le controprove, una dopo l'altra
    • Ovviamente a un certo punto ci si fermerebbe: o si è trovata una prova di Q o una controprova.
  • Dunque, c'e un algoritmo che: su input Q, termina (ma non sa quando) e affermare che Q è una verità logica, se lo è. Se non lo è, non ci sono criteri universalmente validi per decidere quando terminare.

• Conseguenza: La procedura FO-Con in alcuni casi non validerà argomentazioni valide è marchera l'argomentazione con un punto interrogativo (si è arressa per ragioni di esaurimento risorse o ragioni pragmatiche).