Reinhard Kahle

		Universes over Frege structures


Frege structures can be syntactically defined as a theory of truth
over applicative theories. In analogy to universes in explicit
mathematics we introduce universes over Frege structures as
propositional functions closed under the truth conditions. In contrast
to the corresponding theories of explicit mathematics, our theories
allow a direct syntactical embedding of iterated fixed point theories.
In this talk we will present the proof-theoretic treatment of
universes over Frege structures and discuss the calibration of Frege
structures in the landscape of proof theory.