We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.

In this article we give a unifying approach to the theory of fundamental sequences and their related Hardy hierarchies of number-theoretic functions and we show the equivalence of the new approach with the classical one.

The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.

Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π1 1-CA) in terms of the more perspicious infinitary approach from [BS88].

In this article we prove that a certain intuitionistic version of the well-known fixed point theory \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\widehat{\rm ID}_1$\end{document} is conservative over \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\mbox{\sf HA}$\end{document} for almost negative formulas.

In the framework of ethical social choice theory, sustainability is justified by efficiency and equity as ethical axioms. These axioms correspond to the Suppes–Sen grading principle. In technologies that are productive in a certain sense, the set of Suppes–Sen maximal utility paths is shown to equal the set of non-decreasing and efficient paths. Since any such path is sustainable, efficiency and equity can thus be used to deem any unsustainable path as ethically unacceptable. This finding is contrasted with results that (...) seem to indicate that an infinite number of generations cannot be treated equally. (shrink)

By combining the methods of two former papers of ours we develop a finitary ordinal analysis of the axiom system KPi of Kripke-P atek set theory with an inaccessible universe. As a main result we obtain an upper bound for the provably recursive functions of KPi.

We introduce a system of simply typed lambda terms and show that a rather comprehensive class of recursion equations on streams or non-wellfounded trees can be solved in our system. Moreover certain conditions are presented which guarantee that the defined functionals are primitive recursive. As a major example we give a co-recursive treatment of Mints’ continuous cut-elimination operator.

Überblicken wir noch einmal das ganze riesige Gebiet des Geistesgeschehens vor und nach der Jahrhundertwende, soweit es darwinistische Züge erkennen läßt, so können wir eines feststellen : Ausgenommen die Konservativen und die Kirchen, die beide angesichts des stürmischen Vorwärtsdrängens darwinistischer Gedankengänge in die Defensive gehen müssen, bedienen sich so gut wie alle geistigen Strömungen des Darwinismus: Die Sozialisten, weil Darwins "Naturtheorie" mit ihrer Gesetzlichkeit des biologischen Fortschritts Gewähr zu bieten scheint, daß auch im Gesellschaftlichen eherne Gesetze des Fortschritts walten, und (...) weil sie aus dem Darwinismus den Beweis für die Gleichheit aller Menschen herauslesen. Die Sozialdarwinisten, weil ihnen Darwins Lehre vom Kampf ums Dasein und von der Auslese der Lebensfähigsten angeblich den Beweis liefert für die Ungleichheit der Menschen und für die Notwendigkeit einer Menschenzucht. Nicht zufällig sprießen um 1890 so viele Zuchtvereine aus dem Boden, weil man in Charles Darwin den großen Pflanzen-, Tier- und Menschenzüchter sah. Die Atheisten, weil mit der Affenabstammung jegliches göttliche Wirken beim Werden des Menschengeschlechts widerlegt sei. Die pantheistischen Schwärmer von Friedrichshagen, weil sie ein Entwicklungsgesetz am Werk zu sehen glauben, das ganz folgerichtig zu immer Besserem, Edlerem, Vollkommnerem, Vergeistigterem führen müsse. Die Verteidiger einer "Leistungsaristokratie". (shrink)

In this paper we give a new and comparatively simple proof of the following theorem by Girard [1]:“If ∀x∈ ${\cal O}$ ∃y∈ ${\cal O}$ ψ(x,y) (where the relationψ is arithmetic and positive in Kleene's ${\cal O}$ ), then there exists a recursive DilatorD such that ∀α≧ω∀x∈ ${\cal O}$ <α∃y∈ ${\cal O}$ (...) modification of Girard's system in [1]) we construct in a uniform way for each ordinalα a derivation Tα of the formula ∀x ∈ ${\cal O}$ <α∃y∈ ${\cal O}$ ψ(x, y), and then defineD immediately from the family (Tα)α∈On. Especially we set D(α):=Kleene-Brouwer length of (Tα). (shrink)