scholarly journals Fibrations, Logical Predicates and Indeterminates

1993 ◽  
Vol 22 (462) ◽  
Author(s):  
Claudio Alberto Hermida
Keyword(s):  
Type Theory ◽  
Lambda Calculus ◽  
Fundamental Property ◽  
Order Logic ◽  
First Order Logic ◽  
Data Types ◽  
Main Concept ◽  
First Order ◽  
Categorical Logic ◽  
Abstract Presentation

<p>Within the framework of categorical logic/type theory, we provide a category-theoretic account of some logical concepts, i.e. first-order logical predicates for simply typed lambda-calculus, structural induction for inductive data types, and indeterminates for polymorphic calculi.</p><p> </p><p>The main concept which underlies the issues above is that of fibration, which gives an abstract presentation of the indexing present in all cases: predicates indexed by types/contexts in first-order logic and types indexed by kinds in polymorphic calculi.</p><p>The characterisation of the logical concepts in terms of fibrations relies on a fundamental property of adjunctions between fibrations, which in particular relates some structure in the total category of a fibration with that of the fibres. Suitable instances of this property reflect the above-mentioned logical concepts in an abstract way, independently of their syntactic presentation, thereby illuminating their main features.</p>

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.).

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 Logical Querying of Relational Databases

2016 ◽  
Vol 5 (4) ◽  
pp. 58
Author(s):  
Luminita Pistol ◽  
Radu BUCEA-MANEA-TONIS
Keyword(s):  
Relational Databases ◽  
Lambda Calculus ◽  
Formal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Short Introduction ◽  
First Order

This paper aims to demonstrate the usefulness of formal logic and lambda calculus in database programming. After a short introduction in propositional and first order logic, we implement dynamically a small database and translate some SQL queries in filtered java 8 streams, enhanced with Tuples facilities from jOOλ library.   

Locally cartesian closed categories and type theory

1984 ◽  
Vol 95 (1) ◽  
pp. 33-48 ◽  
Author(s):  
R. A. G. Seely
Keyword(s):  
Type Theory ◽  
Free Variable ◽  
Order Logic ◽  
First Order Logic ◽  
Topos Theory ◽  
First Order ◽  
Cartesian Closed Categories ◽  
Cartesian Closed ◽  
Indexed Category

It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/A are cartesian closed. In such a category, the notion of a ‘generalized set’, for example an ‘A-indexed set’, is represented by a morphism B → A of C, i.e. by an object of C/A. The point about such a category C is that C is a C-indexed category, and more, is a hyper-doctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A, the predicates with a free variable of type A are morphisms into A, and ‘proofs’ are morphisms over A. We see here a certain ‘ambiguity’ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A, which is a predicate over A; a morphism 1 → A can be viewed either as an object of type A or as a proof of the proposition A.

scholarly journals Using Vampire in Soundness Proofs of Type Systems

10.29007/22x6 ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
Sebastian Erdweg ◽  
Mira Mezini
Keyword(s):  
Programming Languages ◽  
Type System ◽  
Lambda Calculus ◽  
Type Systems ◽  
Current Approach ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Domain Specific ◽  
Automated Proof

Type systems for programming languages shall detect type errors in programs before runtime. To ensure that a type system meets this requirement, its soundness must be formally verified. We aim at automating soundness proofs of type systems to facilitate the development of sound type systems for domain-specific languages.Soundness proofs for type systems typically require induction. However, many of the proofs of individual induction cases only require first-order reasoning. For the development of our workbench Veritas, we build on this observation by combining automated first-order theorem provers such as Vampire with automated proof strategies specific to type systems. In this paper, we describe how we encode type soundness proofs in first-order logic using TPTP. We show how we use Vampire to prove the soundness of type systems for the simply-typed lambda calculus and for parts of a typed SQL. We report on which parts of the proofs are handled well by Vampire, and what parts work less well with our current approach.

Sign in / Sign up

Export Citation Format

Share Document