23 mai 2011
Daniel Leivant (Indiana University - Bloomington)Second order logic is a master descriptive framework for computation and programming, and yet its standard proof theory far exceeds the realm of computability. Three independent methods can be used to tame the comprehension principle of second order logic so as to convey a more computational contents: restriction to formulas with direct computational contents, prohibition of set parameters, and ramification. The various combinations of these three give rise to a cube of complexity classes, going from the full analytical hierarchy to PTime.