A canonical proof-theoretic approach to model theory

LOPEZ POMBO, CARLOS GUSTAVO; CHOCRÓN, PAULA; VISSANI, IGNACIO; MAIBAUM, THOMAS S. E.

Sinaia

Workshop; Worshop on Algebraic Development Techniques; 2014

Universitatea din București

Logic has proved essential as a formal language for describing different aspects of software artefacts. These formal descriptions, frequently called specifications, have served not only as requirements documentation but also for proving prop- erties, provided the logical language in which the specification is written has an appropriate reasoning tool. Semantics is an integral part of logic, as providing logical descriptions of real-world phenomena requires people to agree on how these descriptions should be interpreted. In this sense, model theory has been seen as providing the cornerstone for the satisfaction of this need. Model theory is usually understood as the study of classes of mathematical structures satisfying formulae in a formal language of choice. Model theory is a tool for characterising semantic notions, like meaning and truth, associated to syntactic objects, like formulae and proofs, of a corresponding language. From a category theory point of view the model theory of a logic has been formalised as an institution [1]. An institution is a structure ⟨Sign,Sen,Mod,{|=Σ}Σ∈|Sign|⟩ formed by: 1) a cate- gory of signatures Sign, 2) a grammar functor Sen : Sign → Set providing a set of sentences for each signature, 3) a model functor Mod : Signop → Cat providing a class of semantic structures for each signature, 4) a family of binary rela- tions {|=Σ }Σ∈|Sign| such that given Σ ∈ |Sign|, |=Σ ⊆ |Mod(Σ)| × |Sen(Σ)|, and 5) satisfying that for all σ : Σ → Σ′ ∈ ||Sign||, α ∈ Sen(Σ) and M ∈ Mod(Σ′), M|=Σ′ Sen(σ)(α)ifandonlyifMod(σ)(M)|=Σα. In mathematical logic, given a logical system, we are forced to consider all possible semantic structures that can interpret its sentences, while in computer science we are mostly concerned about the analysability of the semantics as we rely on it to prove properties of software artefacts (as well as meta properties of the logic itself). Usually, we place trust only in those structures that can be described resorting to a formal logical language; typically they are maximal consistent theories in the language of choice, like those used in Henkin?s com- pleteness proof for equational logic [2], or theories over some formalisation of set theory. Our aim is to undertake a recasting of the notion of semantics in syntactic terms to support this approach. Behavioural specifications, such as those written in any dynamic logic [3], temporal logics, both linear time [4], and branching time [5,6], etc., usually in- volve the following common elements: 1) an interpretation of a subset of symbols whose interpretation is fixed for all states usually referred to as rigid, 2) an or- dering of states (for example, sequences of states in linear temporal logics, trees of states in branching time temporal logics, a single state in dynamic logics, etc.) such that each of the constituent states provide an interpretation of a different subset of symbols, referred to as flexible symbols, and 3) a satisfaction relation providing meaning for behavioural logic operators. Generally, the ordering of states is obtained from a binary relation between them; for example, in dynamic logics there is a set of atomic actions and regular programs defined over them; in temporal logics, both linear time and branching time, there is a single transition relation; in deontic logics there are events produced by actions, etc. This paper addresses the question of whether such a class of structures can be constructed in a canonical way so the definition of the functor Mod, in the definition of institutions, can be given in concrete representable terms. Equational logic extended with extra-logical predicate symbols has been widely accepted as an appropriate specification language for describing the oper- ations of abstract data types [7]. Equational theories can also be used to provide interpretations, of extra-logical symbols by considering formulae of the form f(t1,...,tn) = t and P(t1,...,tn) where t1,...,tn and t are ground terms of the logical language of choice. On the other hand, we extend the Elementary The- ory of Binary Relations [8] by incorporating the additional relational operators of ω-closure fork algebras [9]. This class of relation algebras have been used to reason about relations due to their complete (almost) equational calculus and its easy-to-understand concrete semantics, build out of a set of binary relations. In this work we propose a general framework that facilitates the definition of the semantics of a logical system by identifying and properly characterising its static and dynamic properties. To make the approach flexible, we propose the use of a higher-order extension of equational logic to formalise the static aspects, while the dynamic properties characterising the accessibility relations between states are expressed by means of concrete models for fork algebraic terms.