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 $arphi^exists$ of $arphi$ belongs to $Theta$, for any $arphiinPhi$. In 1988, Parlamento and Policriti already showed how to apply G"odel-like arguments to a very weak axiomatic set theory, with respect to the class of $Sigma_1$-formulae with $(orallexistsorall)_0$-matrix, i.e., existential closures of formulae that contain just restricted quantifiers of the kind $(orall x in y)$ and $(exists x in y)$ and are writeable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a `$orall$'). While revisiting their work, we show slightly stronger theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of $(orallexists)_0$-matrices, namely formulae with at most one alternation of restricted quantifiers.

Very weak, essentially undecidabile set theories

Domenico Cantone;Mattia Panettiere;
2021-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 $arphi^exists$ of $arphi$ belongs to $Theta$, for any $arphiinPhi$. In 1988, Parlamento and Policriti already showed how to apply G"odel-like arguments to a very weak axiomatic set theory, with respect to the class of $Sigma_1$-formulae with $(orallexistsorall)_0$-matrix, i.e., existential closures of formulae that contain just restricted quantifiers of the kind $(orall x in y)$ and $(exists x in y)$ and are writeable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a `$orall$'). While revisiting their work, we show slightly stronger theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of $(orallexists)_0$-matrices, namely formulae with at most one alternation of restricted quantifiers.
2021
Decidability
Set Theory
Gödel Incompleteness
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/20.500.11769/518937
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact