Decidibilità e completezza dell'aritmetica di Presburger

L’intento di questa tesi è quello di dimostrare la completezza e la decidibilità dell’aritmetica classica di Presburger (PrA) seguendo la dimostrazione ad opera di Halbeisen e Krapf in 'Gödel’s Theorems and Zermelo’s Axioms'. L’aritmetica classica di Presburger è una sottoteoria dell’aritmetica classica di Peano (PA), descritta nel linguaggio dell’aritmetica di PrA privo dell’operazione di moltiplicazione e con i soli assiomi riguardanti il successore e lo zero, l’addizione e l’induzione. Mentre PA è una teoria indecidibile e incompleta per i Teoremi di Incompletezza di Gödel, PrA risulta una teoria decidibile e completa. Proveremo questo fatto nel capitolo 5, utilizzando la dimostrazione ideata da Herbert Enderton in 'A mathematical introduction to logic' nel 1972. Tale dimostrazione è una variazione adattata direttamente a PrA della dimostrazione originale di completezza e decidibilità data da Mojzesz Presburger per la teoria classica del primo ordine Th(Z,0,1,+) nel linguaggio di PrA sul modello standard dei numeri interi, che viene riportata nel capitolo 4. Essa consiste nel fornire un algoritmo di riduzione delle formule predicative a formule proposizionali decidibili, con l’aiuto dei teoremi di forma prenessa normale per la logica classica predicativa e di una procedura per eliminare i quantificatori esistenziali.