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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.