We study Löwenheim-Skolem and Omitting Types theorems in Transition Algebra, a logical system obtained by enhancing many sorted first-order logic with features from dynamic logic. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to actions in dynamic logics to define necessity and possibility operators. We show that Upward Löwenheim-Skolem theorem, any form of compactness, and joint Robinson consistency property fail due to the expressivity of transitive closures of transitions. In this non-compact many-sorted logical system, we develop a forcing technique method by generalizing the classical method of forcing used by Keisler to prove Omitting Types theorem. Instead of working within a single signature, we work with a directed diagram of signatures, which allows us to establish Downward Löwenheim-Skolem and Omitting Types theorems despite the fact that models interpret sorts as sets, possibly empty. Building on a complete system of proof rules for Transition Algebra, we extend it with additional proof rules to reason about constructor-based and/or finite transition algebras. We then establish the completeness of this extended system for a fragment of Transition Algebra obtained by restricting models to constructor-based and/or finite transition algebras.

Ehrenfeucht-Fraïssé games provide means to characterize elementary equivalence for first-order logic, and by standard translation also for modal logics. We propose a novel generalization of Ehrenfeucht-Fraïssé games to hybrid-dynamic logics which is direct and fully modular: parameterized by the features of the hybrid language we wish to include, for instance, the modal and hybrid language operators as well as first-order existential quantification. We use these games to establish a new modular Fraïssé-Hintikka theorem for hybrid-dynamic propositional logic and its various fragments. We study the relationship between countable game equivalence (determined by countable Ehrenfeucht-Fraïssé games) and bisimulation (determined by countable back-and-forth systems). In general, the former turns out to be weaker than the latter, but under certain conditions on the language, the two coincide. As a corollary we obtain an analogue of the Hennessy-Milner theorem. We also prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism.

We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to the actions used in dynamic logics in order to define necessity and possibility operators. This leads to a higher degree of expressivity than that of many-sorted first-order logic. For example, one can finitely axiomatize both the finiteness and the reachability of models, neither of which are ordinarily possible in many-sorted first-order logic. We introduce syntactic entailment and study basic properties such as compactness and completeness, showing that the latter does not hold when standard finitary proof rules are used. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To that end, we generalize the forcing method introduced in model theory by Robinson from a single signature to a category of signatures, and we apply it to obtain a completeness result for signatures that are at most countable.

Abstract Lindström’s theorem characterizes first-order logic in terms of its essential model theoretic properties. One cannot gain expressive power extending first-order logic without losing at least one of compactness or downward Löwenheim–Skolem property. We cast this result in an abstract framework of institution theory, which does not assume any internal structure either for sentences or for models, so it is more general than the notion of abstract logic usually used in proofs of Lindström’s theorem; indeed, it can be said that institutional model theory is both syntax and semantics free. Our approach takes advantage of the methods of institutional model theory to provide a structured proof of Lindström’s theorem at a level of abstraction applicable to any logical system that is strong enough to describe its own concept of isomorphism and its own concept of elementary equivalence. We apply our results to some logical systems formalized as institutions and widely used in computer science practice.

The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions . To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.

Abstract We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones.

Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.

Abstract We develop an abstract proof calculus for hybrid logics whose sentences are ( hybrid ) Horn clauses , and we prove a Birkhoff completeness theorem for hybrid logics in the general setting provided by the institution theory . This result is then applied to particular cases of hybrid logics with user-defined sharing, where the first-order variables in quantified sentences are interpreted uniformly across worlds.

The present article describes a method for proving Downward Löwenheim–Skolem Theorem within an arbitrary institution satisfying certain logic properties. In order to demonstrate the applicability of the present approach, the abstract results are instantiated to many-sorted first-order logic and preorder algebra. In addition to the first technique for proving Downward Löwenheim–Skolem Theorem, another one is developed, in the spirit of institution-independent model theory, which consists of borrowing the result from a simpler institution across an institution comorphism. As a result, the Downward Löwenheim–Skolem Property is exported from first-order logic to partial algebras, and from higher-order logic with intensional Henkin semantics to higher-order logic with extensional Henkin semantics. The second method successfully extends the domain of application of Downward Löwenheim–Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Löwenheim–Skolem Theorem is interpolation in constructor-based logics with universally quantified sentences. The interpolation property is established by borrowing it from a base institution for its constructor-based variant across an institution morphism. This result is important as interpolation for constructor-based first-order logics is still an open problem.

The constructor-based logics constitute the logical foundation of the so-called OTS/CafeOBJ method, a modelling, specification and verification method of the observational transition systems. The important role played in algebraic specifications by the initial algebras semantics is well known. Free models along presentation morphisms provide semantics for the modules with initial denotation in structured specification languages. Following Goguen and Burstall, the notion of logical system over which we build specifications is formalized as an institution. The present work is an institution-independent study of the existence of free models along sufficient complete presentation morphisms in logics with constructors in the signatures.

The completeness of the infinitary language ℒω1,ω was proved by Carol Karp in 1964.We express and prove the completeness of infinitary first-order logics in the institution-independent setting by using forcing, a powerful method for constructing models. As a consequence of this abstraction, the completeness theorem becomes available for the infinitary versions of many ‘first order’ logical systems that appear in the area of logic or computer science.

Journal Article An Institution-independent Generalization of Tarski's Elementary Chain Theorem Get access Daniel Găină, Daniel Găină Department of Fundamentals of Computer Science, Faculty of Mathematics, University of Bucharest. Search for other works by this author on: Oxford Academic Google Scholar Andrei Popescu Andrei Popescu Department of Fundamentals of Computer Science, Faculty of Mathematics, University of Bucharest. Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 16, Issue 6, December 2006, Pages 713–735, https://doi.org/10.1093/logcom/exl006 Published: 12 August 2006