In his introductory paper to first-order logic, Jon Barwise writes in the Handbook of Mathematical Logic :[T]he informal notion of provable used in mathematics is made precise by the formal notion provable in first-order logic. Following a sug[g]estion of Martin Davis, we refer to this view as Hilbert’s Thesis.This paper reviews the discussion of Hilbert’s Thesis in the literature. In addition to the question whether it is justifiable to use Hilbert’s name here, the arguments for this thesis are compared with (...) those for Church’s Thesis concerning computability. This leads to the question whether one could provide an analogue for proofs of the concept of partial recursive function. (shrink)

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{ the exact proof-theoretic ordinals of these systems are presented.

This paper deals with universes in explicit mathematics. After introducing some basic definitions, the limit axiom and possible ordering principles for universes are discussed. Later, we turn to least universes, strictness and name induction. Special emphasis is put on theories for explicit mathematics with universes which are proof-theoretically equivalent to Feferman's.

We give a survey on truth theories for applicative theories. It comprises Frege structures, universes for Frege structures, and a theory of supervaluation. We present the proof-theoretic results for these theories and show their syntactical expressive power. In particular, we present as a novelty a syntactical interpretation of ID1 in a applicative truth theory based on supervaluation.

We give a reading of binary necessity statements of the form “ϕ is necessary for ψ” in terms of proofs. This reading is based on the idea of interpreting such statements as “Every proof of ψ uses ϕ”.

We study the logical relationship of various forms of induction, as well as quantification operators in applicative theories. In both cases the introduced notion of $\hbox{\sf N}$ -strictness allows us to obtain the appropriate results.

In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories.

In this programmatic paper we renew the well-known question “What is a proof?”. Starting from the challenge of the mathematical community by computer assisted theorem provers we discuss in the first part how the experiences from examinations of proofs can help to sharpen the question. In the second part we have a look to the new challenge given by “big proofs”.

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{<\alpha};$ the exact proof-theoretic ordinals of these systems are presented.

Diagonalization is a transversal theme in Logic. In this work, it is shown that there exists a common origin of several diagonalization phenomena — paradoxes and Löb's Theorem. That common origin comprises a common reasoning and a common logical structure. We analyse the common structure from a philosophical point-of-view and we draw some conclusions.

We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory".

In this paper we summarize some results about sets in Frege structures. The resulting set theory is discussed with respect to its historical and philosophical significance. This includes the treatment of diagonalization in the presence of a universal set.

In this paper we introduce applicative theories which characterize the polynomial hierarchy of time and its levels. These theories are based on a characterization of the functions in the polynomial hierarchy using monotonicity constraints, introduced by Ben-Amram, Loff, and Oitavem.

In 2000, a draft note of David Hilbert was found in his Nachlass concerning a 24th problem he had consider to include in the his famous problem list of the talk at the International Congress of Mathematicians in 1900 in Paris. This problem concerns simplicity of proofs. In this paper we review the traces of this problem which one can find in the work of Hilbert and his school, as well as modern research started on it after its publication. We (...) stress, in particular, the mathematical nature of the problem.1. (shrink)

In 2000, Rüdiger Thiele [1] found in a notebook of David Hilbert, kept in Hilbert's Nachlass at the University of Göttingen, a small note concerning a 24th problem. As Hilbert wrote, he had considered including this problem in his famous problem list for the International Congress of Mathematicians in Paris in 1900.

In 2000, Rüdiger Thiele [1] found in a notebook of David Hilbert, kept in Hilbert's Nachlass at the University of Göttingen, a small note concerning a 24th problem. As Hilbert wrote, he had considered including this problem in his famous problem list for the International Congress of Mathematicians in Paris in 1900.