Search

We investigate the distinguishability of sets of relational structures concerning a class of structures in the following sense: for a fixed class of structures, given two sets of structures in this class, find a first-order formula of minimal quantifier rank that distinguishes one set from the other. We consider the following classes of structures: monadic structures, equivalence structures, and disjoint unions of linear orders. We use results of the Ehrenfeucht–Fraïssé game on these classes of structures in order to design an algorithm to find such a sentence. For these classes of structures, the problem of determining if the Duplicator has a winning strategy in an Ehrenfeucht–Fraïssé game is solved in polynomial time. We also introduce the distinguishability sentences which are sentences that distinguish between two given structures. We define the distinguishability sentences based on necessary and sufficient conditions for a winning strategy in an Ehrenfeucht–Fraïssé game. Our algorithm returns a boolean combination of such sentences. We also show that any first-order sentence is equivalent to a boolean combination of distinguishability sentences. Finally, we also show that our algorithm's running time is polynomial in the size of the input. [ABSTRACT FROM AUTHOR]

In this work, we generalize the classical fixed-point logics using relations instead of operators in order to capture the notion of nondeterminism. The basic idea is that we use loops in a relation instead of fixed-points of a function, that is, X is a fixed-point of the relation R in case the pair ( X , X ) belongs to R . We introduce the notion of initial fixed-point of an inflationary relation R and the associated operator rifp . We denote by RIFP the first-order logic with the inflationary relational fixed-point operator rifp and show that it captures the polynomial hierarchy using a translation to second-order logic. We also consider the fragment RIFP 1 with the restriction that the rifp operator can be applied at most once. We show that RIFP 1 captures the class NP and compare our logic with the nondeterministic fixed-point logic proposed by Abiteboul, Vianu and Vardi in [S. Abiteboul, M. Vardi, and V. Vianu. Fixpoint logics, relational machines, and computational complexity. Journal of the ACM , 44-1:30–56, 1997]. [ABSTRACT FROM AUTHOR]

Abstract: In Descriptive Complexity, we investigate the use of logics to characterize computational complexity classes. Since 1974, when Fagin proved that the class NP is captured by existential second-order logic, considered the first result in this area, other relations between logics and complexity classes have been established. Well-known results usually involve first-order logic and its extensions, and complexity classes in polynomial time or space. Some examples are that the first-order logic extended by the least fixed-point operator captures the class P and the second-order logic extended by the transitive closure operator captures the class PSPACE. In this paper, we will analyze the combined use of higher-order logics of order i, HO i , for , extended by the least fixed-point operator, and we will prove that each level of this hierarchy captures each level of the deterministic exponential time hierarchy. As a corollary, we will prove that the hierarchy of HO i (LFP), for , does not collapse, that is, . [Copyright &y& Elsevier]

Abstract: An expression such as , where P occurs in , does not always define P. When such expression implicitly defines P, in the sense of Beth [Beth, E. W., On Padoa''s method in the theory of definitions., Indagationes Mathematicae 15 (1953), pp. 330–339] and Padoa [Padoa, A., Essai d''une théorie algébrique des nombres entiers, precedé d''une introduction logique a une théorie deductive quelconque, in: Bibliothèque Du Congrès International de Philosophie, 1900, pp. 118–123], we call it a recursive definition. In the Least Fixed-Point Logic (LFP), we have theories where interesting relations can be recursively defined [Ebbinghaus, H.-D. and J. Flum, “Finite Model Theory,” Springer-Verlag, 1995; Libkin, L., “Elements of Finite Model Theory,” Springer, 2004]. We will show that for some sorts of recursive definitions there are explicit definitions on sufficiently strong theories of LFP. It is known that LFP, restricted to finite models, does not have Beth''s Definability Theorem [Gurevich, Y. and S. Shelah, On finite rigid structures, Journal of Symbolic Logic 61 (1996), pp. 549–562; Hodkinson, I.M., Finite variable logics, Bulletin of the EATCS 51 (1993), pp. 111–140; Dawar, A., L. Hella and P.G. Kolaitis, Implicit definability and infinitary logic in finite model theory, in: ICALP ''95: Proceedings of the 22nd International Colloquium on Automata, Languages and Programming (1995), pp. 624–635]. Beth''s Definability Theorem states that, if a relation is implicitly defined, then there is an explicit definition for it. We will also give a proof that Beth''s Definability Theorem fails for LFP without this finite model restriction. We intend to investigate fragments of LFP for which Beth''s Definability Theorem holds. [Copyright &y& Elsevier]

Abstract: The notion of the least fixed-point of an operator is widely applied in computer science as, for instance, in the context of query languages for relational databases. Some extensions of first-order classical logic (FOL) with fixed-point operators, as the least fixed-point logic (LFP), were proposed to deal with problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of finite ordered structures. The descriptive characterization of computational classes is a central issue within finite model theory (FMT). Trakhtenbrot''s theorem states that validity over finite models is not recursively enumerable, that is, completeness fails over finite models. This result is based on an underlying assumption that any deductive system is of finite nature. However, we can relax such assumption as done in the scope of proof theory for arithmetic. Motivated by Gödel incompleteness theorems, proof theory for arithmetic offer an example of a true mathematically meaningful principle non derivable in first-order arithmetic. One way of presenting this proof is based on a definition of a proof system with an infinitary rule, the ω-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Inspired by this proof, here we will propose an infinitary natural deduction system for FOL and LFP restricted to finite models, FOLfin and LFPfin , respectively, and we will prove soundness and completeness for them, and also a normalization theorem for fragments of these systems. With this infinitary deductive system for LFPfin , we aim to present a proof theory for a logic traditionally investigated within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new results through a proof theoretical perspective. [Copyright &y& Elsevier]

Abstract: Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [Prawitz, D., “Natural Deduction: A Proof-theoretical Study”, Stockholm Studies in Philosophy 3, Almqvist and Wiksell, Stockholm, 1965] from a proof-theoretical perspective. Prawitz proved weak normalization for classical logic just for a language without ∨, ∃ and with a restricted application of reduction ad absurdum. Reduction steps related to ∨, ∃ and classical negation brings about a lot of problems solved only rather recently [Seldin, J., Normalization and Excluded Middle I, Studia Logica 48 (1989), 193–217; Stalmark, G., Normalizations Theorems for Full First Order Classical Natural Deduction, The Journal of Symbolic Logic 56 (1991); Massi, C.D.B., “Provas de Normalização para a Lógica Clássica”, Ph.D. thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990; Pereira, L.C., and C.D.B. Massi, Normalização para a Lógica Clássica, O que nos faz pensar, Cadernos de Filosofia da PUC-RJ 2 (1990), 49–53]. For classical S4/S5 modal logics, Prawitz defined normalizable systems, but for a language without ∨, ∃ and ◊. We can mention cut-free Gentzen systems for S4/S5 [Meré, M.C., and L.C. Pereira. “A New Cut-Free System for Intuitionistic S4”, Encontro Brasileiro de Lógica, Salvador, 1996; Mints, G.E., “Lewis'' Systems and System T (1965–1973)”, Selected Papers in Proof Theory, Studies in Proof Threory, North-Holland, 1992, 221–293; Mints, G.E., Cut-Free Calculi of the S5 Type Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics 8 (1970), 79–82; Bragança, R.C.M., E.H. Haeusler, and L.C. Pereira, A New Cut-Free Sequent calculus for S5, The Bulletin of Symbolic Logic 5 (1999), 497–498; Braüner, T., A Cut-Free Gentzen Formulation of the Modal Logic S5, Logic Journal of the IGPL 8 (2000), 629–643; H. Wansing. Sequent Calculi for Normal Modal Propositional Logics, Journal of Logic and Computation 4 (1994), 125–142], normalizable natural deduction systems for intuitionistic modal logics [Simpson, A.K., “The Proof Theory and Semantics of Intuitionistic Modal Logic”, Ph.D. thesis, University of Edinburgh, 1994; Masini, A., 2-Sequent Calculus: Intuitionism and Natural Deduction, Journal of Logic and Computation 3 (1993), 533–562] and for full classical S4 [Martins, L.R., and A.T. Martins, “Normalizable Natural Deduction Rules for S4 Modal Operators”, World Congress on Universal Logic, Montreux, 2005, 79–80], but not for full classical S5. Here our focus is in the definition of a classical and normalizable natural deduction system for S5, taken not only □ and ◊ as primitive symbols, but also all connectives and quantifiers, including classical negation, disjunction and the existential quantifier. The normalization procedure will be based on the strategy proposed by [Massi, C.D.B., “Provas de Normalização para a Lógica Clássica”, Ph.D. thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990; Pereira, L.C., and C.D.B. Massi, Normalização para a Lógica Clássica, O que nos faz pensar, Cadernos de Filosofia da PUC-RJ 2 (1990), 49–53] to cope with the combined use of classical negation, ∨ and ∃. We will extend such results to deal with ◊ too. The elimination rule for ◊ will use the notions of connection and of essentially modal formulas already proposed by Prawitz for the introduction of □. Weak normalization and subformula property is proved for full S5. [Copyright &y& Elsevier]