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

1996 ◽  
Vol 2 (2) ◽  
pp. 159-188 ◽  
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.

An intensional type theory: motivation and cut-elimination

2001 ◽  
Vol 66 (1) ◽  
pp. 383-400 ◽  
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.

scholarly journals The Prospects for Mathematical Logic in the Twenty-First Century

2001 ◽  
Vol 7 (2) ◽  
pp. 169-196 ◽  
Author(s):  
Samuel R. Buss ◽  
Alexander S. Kechris ◽  
Anand Pillay ◽  
Richard A. Shore
Keyword(s):  
Mathematical Logic ◽  
Computer Science ◽  
Set Theory ◽  
Model Theory ◽  
Proof Theory ◽  
Recursion Theory ◽  
First Century ◽  
Future Developments ◽  
The Future ◽  
Twenty First Century

AbstractThe four authors present their speculations about the future developments of mathematical logic in the twenty-first century. The areas of recursion theory, proof theory and logic for computer science, model theory, and set theory are discussed independently.

Some Fixpoint Techniques in Algebraic Structures and Applications to Computer Science

1987 ◽  
Vol 10 (4) ◽  
pp. 387-413
Author(s):  
Irène Guessarian
Keyword(s):  
Logic Programming ◽  
Computer Science ◽  
Proof Theory ◽  
Algebraic Structures ◽  
Data Bases

This paper recalls some fixpoint theorems in ordered algebraic structures and surveys some ways in which these theorems are applied in computer science. We describe via examples three main types of applications: in semantics and proof theory, in logic programming and in deductive data bases.

scholarly journals Preface

2011 ◽  
Vol 21 (4) ◽  
pp. 671-677 ◽  
Author(s):  
GÉRARD HUET
Keyword(s):  
Mathematical Logic ◽  
Computer Science ◽  
20Th Century ◽  
Theorem Proving ◽  
Propositional Calculus ◽  
Interactive Theorem Proving ◽  
Predicate Calculus ◽  
Special Issue ◽  
Mathematical Structures ◽  
Infinite Domains

This special issue of Mathematical Structures in Computer Science is devoted to the theme of ‘Interactive theorem proving and the formalisation of mathematics’.The formalisation of mathematics started at the turn of the 20th century when mathematical logic emerged from the work of Frege and his contemporaries with the invention of the formal notation for mathematical statements called predicate calculus. This notation allowed the formulation of abstract general statements over possibly infinite domains in a uniform way, and thus went well beyond propositional calculus, which goes back to Aristotle and only allowed tautologies over unquantified statements.

Mathematical Logic: Proof Theory, Constructive Mathematics

2008 ◽  
pp. 907-952
Author(s):  
Samuel Buss ◽  
Helmut Schwichtenberg ◽  
Ulrich Kohlenbach
Keyword(s):  
Mathematical Logic ◽  
Proof Theory ◽  
Constructive Mathematics

PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS

2019 ◽  
Vol 13 (4) ◽  
pp. 720-747
Author(s):  
SERGEY DROBYSHEVICH ◽  
HEINRICH WANSING
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Axiom System ◽  
Modal Logics ◽  
Cut Elimination ◽  
Proof Systems ◽  
Image Position ◽  
Axiomatic Extension

AbstractWe present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing (2010) and Odintsov & Wansing (2017), as well as the modal logic KN4 with strong implication introduced in Goble (2006). In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.

Sign in / Sign up

Export Citation Format

Share Document