LFCS Seminar: Alberto Policriti
The decidability of the BernaysSchoenfinkelRamsey class in Set Theory
What 


When 
Jun 12, 2012 from 04:00 PM to 05:00 PM 
Where  IF 4.314.33 
Add event to calendar 
vCal iCal 
In this talk I will describe the settheoretic version of the Classical Decision Problem for First Order Logic. I will then illustrate the result on the decidability of the class of purely universal formulae on the unquantified language whose relational symbols are membership and equality. The class we studied is, in the classical (first order) case, the socalled BernaysSchoenfinkelRamsey (BSR) class.
The settheoretic decision problem calls for the existence of an algorithm that, given a purely universal formula in membership 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 elements are 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 proprety not shared by the classical BSR class. The result makes use of a settheoretic 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.
This is joint work with E. Omodeo.