Explaining Gentzen's consistency proof within infinitary proof 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

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

Transmission of Truthmakers

10.1093/oso/9780198777892.003.0009 ◽

2017 ◽

Author(s):

Neil Tennant

Keyword(s):

Proof Theory ◽

Binary Operation ◽

Formal Semantics ◽

Cut Elimination ◽

Infinitary Proof Theory

We begin by introducing the formal genus ‘conditional M-relative construct’, of which M-relative truthmakers and falsitymakers, and core proofs, are species. Fortunately they can stand in symbiotic relations, even though they cannot hybridize. We aim to generalize the earlier method we used in order to prove Cut-Elimination, so that the inputs P for the binary operation [P,P′] can be truthmakers (whereas P′ remains a core proof); and so that the reduct itself, when it is finally determined by recursive application of all the transformations called for, is a truthmaker for the conclusion of P′. This result can be understood as revealing that formal semantics can be carried out in a kind of infinitary proof-theory. Core proof transmits truth courtesy of normalization.

Download Full-text

Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa

Bulletin of Symbolic Logic ◽

10.2307/421108 ◽

1996 ◽

Vol 2 (2) ◽

pp. 159-188 ◽

Cited By ~ 5

Author(s):

Wolfram Pohlers

Keyword(s):

Mathematical Logic ◽

Computer Science ◽

Proof Theory ◽

Axiom System ◽

Theoretical Research ◽

Cut Elimination ◽

Extended Version ◽

Consistency Proof ◽

Exciting Field ◽

Axiom Systems

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions.

Download Full-text