scholarly journals Modal Homotopy Type Theory

2020 ◽  
Author(s):  
David Corfield
Keyword(s):  
Modal Logic ◽  
Homotopy Type ◽  
Type Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Bertrand Russell ◽  
First Order ◽  
Homotopy Type Theory ◽  
General Variation

In[KF1] 1914, in an essay entitled ‘Logic as the Essence of Philosophy’, Bertrand Russell promised to revolutionize philosophy by introducing there the ‘new logic’ of Frege and Peano: “The old logic put thought in fetters, while the new logic gives it wings.” A century later, this book proposes a comparable revolution with a newly emerging logic, modal homotopy type theory. Russell’s prediction turned out to be accurate. Frege’s first-order logic, along with its extension to modal logic, is to be found throughout anglophone analytic philosophy. This book provides a considerable array of evidence for the claim that philosophers working in metaphysics, as well as those treating language, logic or mathematics, would be much better served with the new ‘new logic’. It offers an introduction to this new logic, thoroughly motivated by intuitive explanations of the need for all of its component parts—the discipline of a type theory, the flexibility of type dependency, the more refined homotopic notion of identity and a powerful range of modalities. Innovative applications of the calculus are given, including analysis of the distinction between objects and events, an intrinsic treatment of structure and a conception of modality both as a form of general variation and as allowing constructions in modern geometry. In this way, we see how varied are the applications of this powerful new language—modal homotopy type theory.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

Resolution in type theory

1971 ◽  
Vol 36 (3) ◽  
pp. 414-432 ◽  
Author(s):  
Peter B. Andrews
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Different Types ◽  
Axiomatic Set Theory ◽  
Order Predicate Calculus

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

Logical Tools

2021 ◽  
pp. 14-52
Author(s):  
Cian Dorr ◽  
John Hawthorne ◽  
Juhani Yli-Vakkuri
Keyword(s):  
Modal Logic ◽  
Possible Worlds ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
System P

This chapter presents the system of classical higher-order modal logic which will be employed throughout this book. Nothing more than a passing familiarity with classical first-order logic and standard systems of modal logic is presupposed. We offer some general remarks about the kind of commitment involved in endorsing this logic, and motivate some of its more non-standard features. We also discuss how talk about possible worlds can be represented within the system.

scholarly journals Subformula Linking for Intuitionistic Logic with Application to Type Theory

2021 ◽  
pp. 200-216
Author(s):  
Kaustuv Chaudhuri
Keyword(s):  
Theorem Proving ◽  
Intuitionistic Logic ◽  
Type Theory ◽  
Linear Logic ◽  
Interactive Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Direct Manipulation ◽  
First Order

AbstractSubformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating links between subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.

scholarly journals Completeness theorems for first-order logic analysed in constructive type theory

2021 ◽  
Vol 31 (1) ◽  
pp. 112-151
Author(s):  
Yannick Forster ◽  
Dominik Kirst ◽  
Dominik Wehr
Keyword(s):  
Type Theory ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
The Standard Model ◽  
Coq Proof Assistant ◽  
Game Theoretic ◽  
Completeness Theorems

Abstract We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak K̋nig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

Logic in the 1930s: Type Theory and Model Theory

2013 ◽  
Vol 19 (4) ◽  
pp. 433-472 ◽  
Author(s):  
Georg Schiemer ◽  
Erich H. Reck
Keyword(s):  
Twentieth Century ◽  
Model Theory ◽  
Type Theory ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Gradual Transformation ◽  
Standard Framework ◽  
Theory And Model ◽  
Made In

AbstractIn historical discussions of twentieth-century logic, it is typically assumed that model theory emerged within the tradition that adopted first-order logic as the standard framework. Work within the type-theoretic tradition, in the style of Principia Mathematica, tends to be downplayed or ignored in this connection. Indeed, the shift from type theory to first-order logic is sometimes seen as involving a radical break that first made possible the rise of modern model theory. While comparing several early attempts to develop the semantics of axiomatic theories in the 1930s, by two proponents of the type-theoretic tradition (Carnap and Tarski) and two proponents of the first-order tradition (Gödel and Hilbert), we argue that, instead, the move from type theory to first-order logic is better understood as a gradual transformation, and further, that the contributions to semantics made in the type-theoretic tradition should be seen as central to the evolution of model theory.

scholarly journals Tableau-based translation from first-order logic to modal logic

2021 ◽  
Vol 56 ◽  
pp. 57-74
Author(s):  
Tin Perkov ◽  
Luka Mikec
Keyword(s):  
Modal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Modal Formula ◽  
First Order ◽  
Starting Point ◽  
Invariance Test

We define a procedure for translating a given first-order formula to an equivalent modal formula, if one exists, by using tableau-based bisimulation invariance test. A previously developed tableau procedure tests bisimulation invariance of a given first-order formula, and therefore tests whether that formula is equivalent to the standard translation of some modal formula. Using a closed tableau as the starting point, we show how an equivalent modal formula can be effectively obtained.

scholarly journals A Quantified Coalgebraic van Benthem Theorem

2021 ◽  
pp. 551-571
Author(s):  
Paul Wild ◽  
Lutz Schröder
Keyword(s):  
Modal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Transition Systems ◽  
First Order ◽  
Wide Range ◽  
Symmetry Assumption ◽  
Invariant Properties ◽  
Bounded Rank

AbstractThe classical van Benthem theorem characterizes modal logic as the bisimulation-invariant fragment of first-order logic; put differently, modal logic is as expressive as full first-order logic on bisimulation-invariant properties. This result has recently been extended to two flavours of quantitative modal logic, viz. fuzzy modal logic and probabilistic modal logic. In both cases, the quantitative van Benthem theorem states that every formula in the respective quantitative variant of first-order logic that is bisimulation-invariant, in the sense of being nonexpansive w.r.t. behavioural distance, can be approximated by quantitative modal formulae of bounded rank. In the present paper, we unify and generalize these results in three directions: We lift them to full coalgebraic generality, thus covering a wide range of system types including, besides fuzzy and probabilistic transition systems as in the existing examples, e.g. also metric transition systems; and we generalize from real-valued to quantale-valued behavioural distances, e.g. nondeterministic behavioural distances on metric transition systems; and we remove the symmetry assumption on behavioural distances, thus covering also quantitative notions of simulation.

Modal Types

2020 ◽  
pp. 107-138
Author(s):  
David Corfield
Keyword(s):  
Twentieth Century ◽  
Modal Logic ◽  
Temporal Logic ◽  
Homotopy Type ◽  
Type Theory ◽  
Possible World ◽  
De Re ◽  
Rigid Designators ◽  
Homotopy Type Theory ◽  
De Dicto

Modal logic flourished throughout the twentieth century. Kripke provided a semantics in terms of possible world recognized by mathematicians to be an example of varying sets. This allows a formulation in terms of monads generated by adjunctions. Modal homotopy type theory adds the radical idea that modalities apply to all types, not just propositions, so as to make sense of possible steps and necessary ingredients. The proximity is shown between the structures discovered by modal logicians and common ideas in mathematics of stability under variation. We can then reformulate many ideas in current philosophical metaphysical uses of modal logic, such as rigid designators, counterparts, the de re/de dicto distinction, and so on. Worlds are understood as extended contexts, allowing a formulation of counterfactuals. A form of temporal logic is also easily generated in the same vein.

Sign in / Sign up

Export Citation Format

Share Document