Una Dimostrazione della Coerenza dell'Aritmetica nel Calcolo dei Sequenti G3c

Abstract

L'obiettivo della tesi è quello di formalizzare l'aritmetica di Peano all'interno del calcolo dei sequenti, per poi dimostrarne la coerenza. Verrà ripresa la dimostrazione originale di Gentzen, nella versione in Mancosu, Galvan, Zach (2021), ma sarà utilizzato il calcolo G3c, invece che l'originale LK. Grazie alle proprietà strutturali del calcolo scelto, la dimostrazione si semplificherà.

The aim of this thesis is to formalize Peano Arithmetic within the sequent calculus and then prove its consistency. Gentzen’s original proof will be revisited in the version presented in Mancosu, Galvan, and Zach (2021), but the calculus G3c will be used instead of the original LK system. Owing to the structural properties of the chosen calculus, the proof will be simplified.