In a first-order theory Theta, the decision problem for a class of formulae Phi is solvable if there is an algorithmic procedure that can assess whether or not the existential closure of phi(there exists) of phi belongs to Theta, for any phi is an element of Phi. In 1988, Parlamento and Policriti already showed how to tailor arguments a la Godel to a very weak axiomatic set theory, referring them to the class of Sigma(1)- formulae with (for all there exists for all)(0)-matrix, i.e. existential closures of formulae that contain just restricted quantifiers of the forms (for all x is an element of y) and (there exists x is an element of y) and are writable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a 'for all'). While revisiting their work, we show slightly less weak theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of (for all there exists)(0)-matrices, namely formulae with at most one alternation of restricted quantifiers.

Reconciling transparency, low Δ0-complexity and axiomatic weakness in undecidability proofs

Cantone D.
Membro del Collaboration Group
;
Omodeo E.
Membro del Collaboration Group
;
2023-01-01

Abstract

In a first-order theory Theta, the decision problem for a class of formulae Phi is solvable if there is an algorithmic procedure that can assess whether or not the existential closure of phi(there exists) of phi belongs to Theta, for any phi is an element of Phi. In 1988, Parlamento and Policriti already showed how to tailor arguments a la Godel to a very weak axiomatic set theory, referring them to the class of Sigma(1)- formulae with (for all there exists for all)(0)-matrix, i.e. existential closures of formulae that contain just restricted quantifiers of the forms (for all x is an element of y) and (there exists x is an element of y) and are writable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a 'for all'). While revisiting their work, we show slightly less weak theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of (for all there exists)(0)-matrices, namely formulae with at most one alternation of restricted quantifiers.
2023
https://academic.oup.com/logcom/article/33/4/738/7095786
File in questo prodotto:
File Dimensione Formato  
exad010.pdf

accesso aperto

Tipologia: Documento in Versione Editoriale
Licenza: Creative commons
Dimensione 496.62 kB
Formato Adobe PDF
496.62 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/3067079
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact