Published: 27th January 2011 DOI: 10.4204/EPTCS.47 ISSN: 2075-2180 |
Invited Presentation:
Analyzing proofs based on weak sequential compactness Ulrich Kohlenbach | 1 |
Invited Presentation:
Epsilon Substitution for Predicate Logic Grigori Mints | 3 |
Interactive Learning Based Realizability and 1-Backtracking Games Federico Aschieri | 6 |
On Various Negative Translations Gilda Ferreira and Paulo Oliva | 21 |
Superdeduction in Lambda-Bar-Mu-Mu-Tilde Clément Houtmann | 34 |
An applicative theory for FPH Reinhard Kahle and Isabel Oitavem | 44 |
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic Luís Pinto and Tarmo Uustalu | 57 |
Dialectica Interpretation with Marked Counterexamples Trifon Trifonov | 73 |
Recent work in the 'proof mining' program of extracting effective uniform bounds from proofs in nonlinear analysis ([5]) has started to address proofs that are based on uses of weak sequential compactness in Hilbert space in an abstract setting without any use of separability ([6, 7, 8]). In this talk
[1] | Baillon, J.B., Un théorème de type ergodique pour les contractions non linéaires dans un espace de Hilbert. C.R. Acad. Sci. Paris Sèr. A-B 280, pp. 1511-1514 (1975). |
[2] | Brézis, H., Browder, F.E., Nonlinear ergodic theorems. Bull. Amer. Math. Soc. 82, pp. 959-961 (1976). |
[3] | Browder, F.E., Convergence of approximants to fixed points of nonexpansive nonlinear mappings in Banach spaces. Arch. Rational Mech. Anal. 24, pp. 82-90 (1967). |
[4] | Halpern, B., Fixed points of nonexpanding maps. Bull. Amer. Math. Soc. 73, pp., 957-961 (1967). |
[5] | Kohlenbach, U., Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. xx+536pp., Springer Heidelberg-Berlin, 2008. |
[6] | Kohlenbach, U., On the logical analysis of proofs based on nonseparable Hilbert space theory. In: Feferman, S., Sieg, W. (eds.), Proofs, Categories and Computations. Essays in Honor of Grigori Mints. College Publications, pp. 131-143 (2010) |
[7] | Kohlenbach, U., On quantitative versions of theorems due to F.E. Browder and R. Wittmann. To appear in: Advances in Mathematics. |
[8] | Kohlenbach, U., A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem. Preprint, 18pp., 2010. |
[9] | Tao, T., Soft analysis, hard analysis, and the finite convergence principle. Essay posted May 23, 2007. Appeared in: 'T. Tao, Structure and Randomness: Pages from Year One of a Mathematical Blog. AMS, 298pp., 2008'. |
An epsilon substitution method for first order predicate logic had been described and proved to terminate in the monograph "Grundlagen der Mathematik". We discuss obstacles to extension of this proof to second order logic.
In the preface to volume 2 of [1] in 1939 P. Bernays wrote:
"At present W. Ackermann is transforming his previous
proof presented in the Chapter two of this volume to employ transfinite
induction in the form used by Gentzen and cover the whole arithmetical
formalism.
When this succeeds - as there are all grounds to expect - then the
efficacy of the original Hilbert's Ansatz will be vindicated. In any case
already on the base of the Gentzen's proof one can be convinced that the
temporary fiasko of the proof theory was caused merely by too high
methodological requirements imposed on that theory. Of course the decisive
verdict about the fate of proof theory depends on the problem of proving
the consistency of the Analysis." [English translation by G. Mints].
Hilbert's Ansatz here refers to the epsilon substitution method introduced by D. Hilbert for a formulation where quantifiers are defined in terms of the ε-symbol ε x F[x] read "some x satisfying F[x] ".
The principal part of a proof (derivation) in a system based on ε-symbol is a
The goal of the epsilon substitution process for first order logic introduced in this form by W. Ackermann and described in "Grundlagen der Mathematik" [1] is to find a series of substitutions of ε-terms by other terms
It is instructive to compare this to Herbrand disjunction.
The principal step. Take the ε-term
For the Second Order Logic the language is extended by the second order ε-symbols ε XF[X] with the critical formulas
It is still possible to make one step of the previous method:
Take the ε-term
An open Problem. Extend termination proof to second order case.
Even if this substitution process terminates, the proof of termination should use different ideas, most probably from Girard's computability proof.
However there is no Tait-Girard-style computability proof in the
literature even for the first order case.
Even in the first order case strong termination fails.
First, as noticed already by Ackermann, the attempt to substitute
ε-terms of a non-maximal rank first can destroy some critical
formulas.
Second, even for maximal rank, the attempt to substitute for a term of
non-maximal degree can lead to a loop even for the first order. Define