Logics that define their own semantics
countable logics over finite vocabulariesfinite model theorymodel checking Turing machinesnesting hierarchies for generalized quantifiersPTIMErecursive logicsself definability
Logic in computer science (03B70) Model theory of finite structures (03C13) Logic with extra quantifiers and operators (03C80) Abstract model theory (03C95) Turing machines and related notions (03D10) Complexity of computation (including implicit computational complexity) (03D15) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)
The capability of logical systems to express their own satisfaction relation is a key issue in mathematical logic. Our notion of self definability is based on encodings of pairs of the type (structure, formula) into single structures wherein the two components can be clearly distinguished. Hence, the ambiguity between structures and formulas, forming the basis for many classical results, is avoided. We restrict ourselves to countable, regular, logics over finite vocabularies. Our main theorem states that self definability, in this framework, is equivalent to the existence of complete problems under quantifier-free reductions. Whereas this holds true for arbitrary structures, we focus on examples from finite model theory. Here, the theorem sheds new light on nesting hierarchies for certain generalized quantifiers. They can be interpreted as failure of self definability in the according extensions of first-order logic. As a further application we study the possibility of the existence of recursive logics for PTIME. We restate a result of Dawar concluding from recursive logics to complete problems. We show that for the model checking Turing machines associated with a recursive logic, it makes no difference whether or not they may use built-in clocks.
This page was built for publication: Logics that define their own semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1818429)
