=Paper=
{{Paper
|id=None
|storemode=property
|title=On the Decidability of the ∃*∀* Prefix Class in Set Theory
|pdfUrl=https://ceur-ws.org/Vol-1068/paper-i04.pdf
|volume=Vol-1068
|dblpUrl=https://dblp.org/rec/conf/cilc/Policriti13
}}
==On the Decidability of the ∃*∀* Prefix Class in Set Theory==
<pdf width="1500px">https://ceur-ws.org/Vol-1068/paper-i04.pdf</pdf>
<pre>
On the decidability of the ∃∗ ∀∗ prefix class in
                 Set Theory

                               Alberto Policriti

 Dipartimento di Matematica e Informatica, Universit degli Studi di Udine



  Abstract. In this talk I will describe the set-theoretic version of the
  Classical Decision Problem for First Order Logic. I will then illustrate
  the result on the decidability of the satisfiability problem class of purely
  universal formulae (∃∗ ∀∗ -sentences) on the unquantified language whose
  relational symbols are membership and equality. The class we studied
  is, in the classical (first order) case, the so-called Bernays-Schoenfinkel-
  Ramsey (BSR) class. The set-theoretic decision problem calls for the
  existence of an algorithm that, given a purely universal formula in mem-
  bership and equality, establishes whether there exist sets that substituted
  for the free variables will satisfy the formula. The sets to be used are pure
  sets, namely sets whose only possible elements are themselves sets. Much
  of the difficulties in solving the decision problem for the BSR class in Set
  Theory came from the ability to express infinity in it, a property not
  shared by the classical BSR class. The result makes use of a set-theoretic
  version of the argument Ramsey used to characterize the spectrum of
  the BSR class in the classical case. This characterization was the result
  that motivated Ramsey celebrated combinatorial theorem.

</pre>