Handbook of Proof Theory (eBook)

S.R. Buss (Herausgeber)

eBook Download: EPUB

1998 | 1. Auflage
810 Seiten
Elsevier Science (Verlag)
978-0-08-053318-6 (ISBN)

Infos

This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth.

The chapters are arranged so that the two introductory articles come first, these are then followed by articles from core classical areas of proof theory, the handbook concludes with articles that deal with topics closely related to computer science.

Inhalt

Front Cover 1
Handbook of Proof Theory 4
Copyright Page 5
Table of Contents 10
Preface 6
List of Contributors 8
Chapter I. An Introduction to Proof Theory 12
Chapter II. First-Order Proof Theory of Arithmetic 90
Chapter III. Hierarchies of Provably Recursive Functions 160
Chapter IV. Subsystems of Set Theory and Second Order Number Theory 220
Chapter V. Gödel's Functional ("Dialectica") Interpretation 348
Chapter VI. Realizability 418
Chapter VII. The Logic of Provability 486
Chapter VIII. The Lengths of Proofs 558
Chapter IX. A Proof-Theoretic Framework for Logic Programming 650
Chapter X. Types in Logic, Mathematics and Programming 694
Name Index 798
Subject Index 808

Textauszug

Chapter I

An Introduction to Proof Theory

Samuel R. Buss    Departments of Mathematics and Computer Science, University of California, San Diego La Jolla, California 92093–0112, USA

Proof Theory is the area of mathematics which studies the concepts of mathematical proof and mathematical provability. Since the notion of “proof” plays a central role in mathematics as the means by which the truth or falsity of mathematical propositions is established; Proof Theory is, in principle at least, the study of the foundations of all of mathematics. Of course, the use of Proof Theory as a foundation for mathematics is of necessity somewhat circular, since Proof Theory is itself a subfield of mathematics.

There are two distinct viewpoints of what a mathematical proof is. The first view is that proofs are social conventions by which mathematicians convince one another of the truth of theorems. That is to say, a proof is expressed in natural language plus possibly symbols and figures, and is sufficient to convince an expert of the correctness of a theorem. Examples of social proofs include the kinds of proofs that are presented in conversations or published in articles. Of course, it is impossible to precisely define what constitutes a valid proof in this social sense; and, the standards for valid proofs may vary with the audience and over time. The second view of proofs is more narrow in scope: in this view, a proof consists of a string of symbols which satisfy some precisely stated set of rules and which prove a theorem, which itself must also be expressed as a string of symbols. According to this view, mathematics can be regarded as a ‘game’ played with strings of symbols according to some precisely defined rules. Proofs of the latter kind are called “formal” proofs to distinguish them from “social” proofs.

In practice, social proofs and formal proofs are very closely related. Firstly, a formal proof can serve as a social proof (although it may be very tedious and unintuitive) provided it is formalized in a proof system whose validity is trusted. Secondly, the standards for social proofs are sufficiently high that, in order for a proof to be socially accepted, it should be possible (in principle!) to generate a formal proof corresponding to the social proof. Indeed, this offers an explanation for the fact that there are generally accepted standards for social proofs; namely, the implicit requirement that proofs can be expressed, in principle, in a formal proof system enforces and determines the generally accepted standards for social proofs.

Proof Theory is concerned almost exclusively with the study of formal proofs: this is justified, in part, by the close connection between social and formal proofs, and it is necessitated by the fact that only formal proofs are subject to mathematical analysis. The principal tasks of Proof Theory can be summarized as follows. First, to formulate systems of logic and sets of axioms which are appropriate for formalizing mathematical proofs and to characterize what results of mathematics follow from certain axioms; or, in other words, to investigate the proof-theoretic strength of particular formal systems. Second, to study the structure of formal proofs; for instance, to find normal forms for proofs and to establish syntactic facts about proofs. This is the study of proofs as objects of independent interest. Third, to study what kind of additional information can be extracted from proofs beyond the truth of the theorem being proved. In certain cases, proofs may contain computational or constructive information. Fourth, to study how best to construct formal proofs; e.g., what kinds of proofs can be efficiently generated by computers?

The study of Proof Theory is traditionally motivated by the problem of formalizing mathematical proofs; the original formulation of first-order logic by Frege [1879] was the first successful step in this direction. Increasingly, there have been attempts to extend Mathematical Logic to be applicable to other domains; for example, intuitionistic logic deals with the formalization of constructive proofs, and logic programming is a widely used tool for artificial intelligence. In these and other domains, Proof Theory is of central importance because of the possibility of computer generation and manipulation of formal proofs.

This handbook covers the central areas of Proof Theory, especially the mathematical aspects of Proof Theory, but largely omits the philosophical aspects of proof theory. This first chapter is intended to be an overview and introduction to mathematical proof theory. It concentrates on the proof theory of classical logic, especially propositional logic and first-order logic. This is for two reasons: firstly, classical first-order logic is by far the most widely used framework for mathematical reasoning, and secondly, many results and techniques of classical first-order logic frequently carryover with relatively minor modifications to other logics.

This introductory chapter will deal primarily with the sequent calculus, and resolution, and to lesser extent, the Hilbert-style proof systems and the natural deduction proof system. We first examine proof systems for propositional logic, then proof systems for first-order logic. Next we consider some applications of cut elimination, which is arguably the central theorem of proof theory. Finally, we review the proof theory of some non-classical logics, including intuitionistic logic and linear logic.

1 Proof theory of propositional logic

Classical propositional logic, also called sentential logic, deals with sentences and propositions as abstract units which take on distinct True/False values. The basic syntactic units of propositional logic are variables which represent atomic propositions which may have value either True or False. Propositional variables are combined with Boolean functions (also called connectives): a k-ary Boolean function is a mapping from {T, F}k to {T, F} where we use T and F to represent True and False. The most frequently used examples of Boolean functions are the connectives and ⊥ which are the 0-ary functions with values T and F, respectively; the binary connectives ∧, ∨, ⊃, ↔ and ⊕ for “and”, “or”, “if-then”, “if-and-only-if” and “parity”; and the unary connective ¬ for negation. Note that ∨ is the inclusive-or and ⊕ is the exclusive-or.

We shall henceforth let the set of propositional variables be V = {p1, p2, p3,…}; however, our theorems below hold also for uncountable sets of propositional variables. The set of formulas is inductively defined by stating that every propositional variable is a formula, and that if A and B are formulas, then (¬A), (A∧ B), (A∨ B), (A ⊃ B), etc., are formulas. A truth assignment consists of an assignment of True/False values to the propositional variables, i.e., a truth assignment is a mapping τ : V → {T, F}. A truth assignment can be extended to have domain the set of all formulas in the obvious way, according to Table 1; we write ¯A for the truth value of the formula A induced by the truth assignment τ.

Table 1

Values of a truth assignment ¯

T

T

F

T

T

T

T

F

T

F

F

F

T

F

F

T

F

T

T

F

T

T

F

T

F

F

T

F

F

T

T

F

A formula A involving only variables among p1,…,pk defines a k-ary Boolean function fA, by letting fA (x1,…,xk) equal the truth value ¯A where τ(pi) = xi for all i. A language is a set of connectives which may be used in the formation of L-formulas. A language L is complete if and only if every Boolean function can be defined by an L-formula. Propositional logic can be formulated with any complete (usually finite) language L — for the time being, we shall use the language ¬,∧, ∨ and ⊃ .

A propositional formula A is said to be a tautology or to be...

Produkt-Details

• Erscheint lt. Verlag: 9.7.1998
• Sprache: englisch
• Themenwelt: Informatik ► Theorie / Studium ► Algorithmen
• Themenwelt: Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik
• Themenwelt: Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
• ISBN-10: 0-08-053318-3 / 0080533183
• ISBN-13: 978-0-08-053318-6 / 9780080533186