اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدSequent Calculus in the Topos of Trees
196
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Nakanos later modality, inspired by G{o}del-L{o}b provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic $mathrm{KM}_{mathrm{lin}}$. We give a sound and cut-free complete sequent calculus for $mathrm{KM}_{mathrm{lin}}$ via a strategy that decomposes implication into its static and irreflexive components. Our calculus provides deterministic and terminating backward proof-search, yields decidability of the logic and the coNP-completeness of its validity problem. Our calculus and decision procedure can be restricted to drop linearity and hence capture KM.
قيم البحث
اقرأ أيضاً
The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not
standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.
Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in equational style
. We show here that the equational approach corresponds to the use of a focused presentation of a type theory expressed as a sequent calculus. A typed functional language is presented, based on a sequent calculus, that we relate to the syntax and internal language of Agda. In particular, we discuss the use of patterns and case splittings, as well as rules implementing inductive reasoning and dependent products and sums.
Basic proof-search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the issues of defi
ning such sequent calculi for Pure Type Systems (PTS, which were originally presented in natural deduction style) and then organizing their rules for effective proof-search. We introduce the idea of Pure Type Sequent Calculus with meta-variables (PTSCalpha), by enriching the syntax of a permutation-free sequent calculus for propositional logic due to Herbelin, which is strongly related to natural deduction and already well adapted to proof-search. The operational semantics is adapted from Herbelins and is defined by a system of local rewrite rules as in cut-elimination, using explicit substitutions. We prove confluence for this system. Restricting our attention to PTSC, a type system for the ground terms of this system, we obtain the Subject Reduction property and show that each PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising iff the latter is. We show how to make the logical rules of PTSC into a syntax-directed system PS for proof-search, by incorporating the conversion rules as in syntax-directed presentations of the PTS rules for type-checking. Finally, we consider how to use the explicitly scoped meta-variables of PTSCalpha to represent partial proof-terms, and use them to analyse interactive proof construction. This sets up a framework PE in which we are able to study proof-search strategies, type inhabitant enumeration and (higher-order) unification.
In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity
bounds for the respective logics. We also present CondLean, a theorem prover for these logics implementing SeqS calculi written in SICStus Prolog.
Coquands cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. This paper contributes to the understand
ing of this model. We make three contributions: 1. Johnstones topological topos was created to present the geometric realization of simplicial sets as a geometric morphism between toposes. Johnstone shows that simplicial sets classify strict linear orders with disjoint endpoints and that (classically) the unit interval is such an order. Here we show that it can also be a target for cubical realization by showing that Coquands cubical sets classify the geometric theory of flat distributive lattices. As a side result, we obtain a simplicial realization of a cubical set. 2. Using the internal `interval in the topos of cubical sets, we construct a Moore path model of identity types. 3. We construct a premodel structure internally in the cubical type theory and hence on the fibrant objects in cubical sets.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
