In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic (IPL) raises some technical and conceptual issues. We relate Sandqvist's (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist's constructions. This naturality includes Sandqvist's treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist's semantics can also be viewed as the natural disjunction in a category of sheaves.
The Sup Connective in IMALL: A Categorical Semantics
Université de Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所、洛林信息与自动研究与创新中心）；DCyT, Universidad Nacional de Quilmes（奎尔姆斯国立大学计算与技术研究系）；IMERL, FIng, Universidad de la República（乌拉圭共和国大学工程与情报学院数学、电子与计算机研究研究所）
Using the category of metric spaces as a template, we develop a metric analogue of the categorical semantics of classical/intuitionistic logic, and show that the natural notion of predicate in this "continuous semantics" is equivalent to the a priori separate notion of predicate in continuous logic, a logic which is independently well-studied by model theorists and which finds various applications. We show this equivalence by exhibiting the real interval [0,1] in the category of metric spaces as a "continuous subobject classifier" giving a correspondence not only between the two notions of pre…
This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism. Aside, a sound and complete semantics for the corresponding lambda-calculus is derived, too. This semantics extends, in a way, the more traditional meanings given by Heyting categories, the topos-theoretic interpretation, and Kripke models. The feature which justifies the introduction of this novel semantics is the fact that it is 'point-free', i.e., there is n…
The primary goal of this paper is to recast the semantics of modal logic, and dynamic epistemic logic (DEL) in particular, in category-theoretic terms. We first review the category of relations and categories of Kripke frames, with particular emphasis on the duality between relations and adjoint homomorphisms. Using these categories, we then reformulate the semantics of DEL in a more categorical and algebraic form. Several virtues of the new formulation will be demonstrated: The DEL idea of updating a model into another is captured naturally by the categorical perspective -- which emphasizes a…
National Research University Higher School of Economics（俄罗斯国立高等经济大学）
We propose a categorial grammar based on classical multiplicative linear logic. This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)} are not abstract $λ$-terms, but simply tuples of words with labeled endpoints, we call them {\it multiwords}. At least, this gives a concrete and intuitive representation of ACG. A key observation is that the class of multiwords has a fundamental algebraic structure. Namely, multiwords can be organized in a category, very similar to the category of topologi…
Model theoretic internality provides conditions under which the group of automorphisms of a model over a reduct is itself a definable group. In this paper we formulate a categorical analogue of the condition of internality, and prove an analogous result on the categorical level. The model theoretic statement is recovered by considering the category of definable sets.
We present a topos-theoretic interpretation of (a categorical generalization of) Fraisse's construction in model theory, with applications to countably categorical theories.
Forking is a central notion of model theory, generalizing linear independence in vector spaces and algebraic independence in fields. We develop the theory of forking in abstract, category-theoretic terms, for reasons both practical (we require a characterization suitable for work in $μ$-abstract elementary classes, i.e. accessible categories with all morphisms monomorphisms) and expository (we hope, with this account, to make forking accessible - and useful - to a broader mathematical audience). In particular, we present an axiomatic definition of what we call a stable independence notion on a…
Inspired by Zermelo's quasi-categoricity result characterizing the models of second-order Zermelo-Fraenkel set theory $\text{ZFC}_2$, we investigate when those models are fully categorical, characterized by the addition to $\text{ZFC}_2$ either of a first-order sentence, a first-order theory, a second-order sentence or a second-order theory. Thus we mount an analysis of the categorical large cardinals. This mathematical analysis leads naturally to philosophical issues concerning structuralism and realism, including especially the tension between categoricity and reflection. Ultimately we ident…
Frobenius Galois expansions of substructural logics:Algebraization, Kalman equivalence and positive cone semantics
School of Science, Xi’an Petroleum University（西安石油大学理学院）；School of Mathematics and Data Science, Shaanxi University of Science and Technology（陕西科技大学数学与数据科学学院）；School of Science, Xi Hang University（西航大学理学院）
Answering a question of Junker and Ziegler, we construct a countable first order structure which is not omega-categorical, but does not have any proper non-trivial reducts, in either of two senses (model-theoretic, and group-theoretic). We also construct a strongly minimal set which is not omega-categorical but has no proper non-trivial reducts in the model-theoretic sense.
We classify the computability-theoretic complexity of two index sets of classes of first-order theories: We show that the property of being an $\aleph_0$-categorical theory is $Π^0_3$-complete; and the property of being an Ehrenfeucht theory $Π^1_1$-complete. We also show that the property of having continuum many models is $Σ^1_1$-hard. Finally, as a corollary, we note that the properties of having only decidable models, and of having only computable models, are both $Π^1_1$-complete.
