Proof theory and Martin-Löf Type Theory

AbstractWe discuss Lorenzen’s consistency proof for ramified type theory without reducibility, published in 1951, in its historical context and highlight Lorenzen’s contribution to the development of modern proof theory, notably by the introduction of the $$\omega $$ ω -rule.

Download Full-text

ETA-RULES IN MARTIN-LÖF TYPE THEORY

Bulletin of Symbolic Logic ◽

10.1017/bsl.2019.21 ◽

2019 ◽

Vol 25 (03) ◽

pp. 333-359

Author(s):

ANSTEN KLEV

Keyword(s):

Lower Order ◽

Category Theory ◽

Type Theory ◽

Proof Theory ◽

Arbitrary Element ◽

Higher Order

AbstractThe eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher order eta rule is part of that type theory. The main aim of this article is to clarify this somewhat puzzling situation. It will be argued that lower order eta rules do not, whereas the higher order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.

Download Full-text

An intensional type theory: motivation and cut-elimination

Journal of Symbolic Logic ◽

10.2307/2694928 ◽

2001 ◽

Vol 66 (1) ◽

pp. 383-400 ◽

Cited By ~ 4

Author(s):

Paul C Gilmore

Keyword(s):

Type Theory ◽

Proof Theory ◽

Predicate Logic ◽

Order Term ◽

Higher Order ◽

Cut Elimination ◽

Consistency Proof ◽

Completeness Proof ◽

Higher Order Term

AbstractBy the theory TT is meant the higher order predicate logic with the following recursively defined types:(1) 1 is the type of individuals and [] is the type of the truth values:(2) [τ1…..τn] is the type of the predicates with arguments of the types τ1…..τn.The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication.In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms.The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT: a consequence is the redundancy of cut.

Download Full-text

Proof Theory of Martin-Löf Type Theory. An overview

Mathématiques et sciences humaines ◽

10.4000/msh.2959 ◽

2004 ◽

Cited By ~ 1

Author(s):

Anton Setzer

Keyword(s):

Type Theory ◽

Proof Theory

Download Full-text

Exploring the Jungle of Intuitionistic Temporal Logics

Theory and Practice of Logic Programming ◽

10.1017/s1471068421000089 ◽

2021 ◽

pp. 1-34

Author(s):

JOSEPH BOUDOU ◽

MARTÍN DIÉGUEZ ◽

DAVID FERNÁNDEZ-DUQUE ◽

PHILIP KREMER

Keyword(s):

Programming Languages ◽

Type Theory ◽

Proof Theory ◽

Order Relation ◽

Point Of View ◽

Temporal Logics ◽

Functional Programming Languages ◽

Order Relations ◽

Theory Point ◽

Axiomatic Systems

Abstract The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible to extend functional programming languages with new features via type theory, while from the semantics perspective, several logics for reasoning about dynamical systems and several semantics for logic programming have their roots in this framework. We consider several axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. We provide two distinct interpretations of “henceforth”, both of which are natural intuitionistic variants of the classical one. We completely establish the order relation between the semantically defined logics based on both interpretations of “henceforth” and, using our soundness results, show that the axiomatically defined logics enjoy the same order relations.

Download Full-text

A logical framework combining model and proof theory

Mathematical Structures in Computer Science ◽

10.1017/s0960129512000424 ◽

2013 ◽

Vol 23 (5) ◽

pp. 945-1001 ◽

Cited By ~ 11

Author(s):

FLORIAN RABE

Keyword(s):

Model Theory ◽

Category Theory ◽

Type Theory ◽

Proof Theory ◽

Software Verification ◽

Logical Framework ◽

Dependent Type Theory ◽

Logical Frameworks ◽

Balanced Approach ◽

Dependent Type

Mathematical logic and computer science have driven the design of a growing number of logics and related formalisms such as set theories and type theories. In response to this population explosion, logical frameworks have been developed as formal meta-languages in which to represent, structure, relate and reason about logics.Research on logical frameworks has diverged into separate communities, often with conflicting backgrounds and philosophies. In particular, two of the most important logical frameworks are the framework of institutions, from the area of model theory based on category theory, and the Edinburgh Logical Framework LF, from the area of proof theory based on dependent type theory. Even though their ultimate motivations overlap – for example in applications to software verification – they have fundamentally different perspectives on logic.In the current paper, we design a logical framework that integrates the frameworks of institutions and LF in a way that combines their complementary advantages while retaining the elegance of each of them. In particular, our framework takes a balanced approach between model theory and proof theory, and permits the representation of logics in a way that comprises all major ingredients of a logic: syntax, models, satisfaction, judgments and proofs. This provides a theoretical basis for the systematic study of logics in a comprehensive logical framework. Our framework has been applied to obtain a large library of structured and machine-verified encodings of logics and logic translations.

Download Full-text

La théorie intuitionniste des types : sémantique des preuves et théorie des constructions

Dialogue ◽

10.1017/s0012217300009537 ◽

1997 ◽

Vol 36 (2) ◽

pp. 323-340

Author(s):

Michel Bourdeau

Keyword(s):

Set Theory ◽

Subject Matter ◽

Type Theory ◽

Proof Theory ◽

Cartesian Product ◽

Functional Space ◽

Functional Dependency ◽

Classical Approach ◽

Constructive Theory ◽

The Subject

AbstractMartin-Löf's constructive theory introduces, beside proof processes—the brouwerian mental construction—proof objects that could become the subject matter of a new kind of proof theory. In contradistinction to the classical approach, the proposition can then be defined as the set of its proofs. The lower level type theory is therefore a set theory, where the operators Σ and Π generalize the Cartesian product and the functional space to families of sets. To obtain the familiar logical constants, we have only to choose the logical reading of a : A. Σ and Π become ∃ and ∀, or, if there is no functional dependency, & and ⊃.

Download Full-text