Skip to main content
main-content

Über dieses Buch

The aim of this volume is to collect original contributions by the best specialists from the area of proof theory, constructivity, and computation and discuss recent trends and results in these areas. Some emphasis will be put on ordinal analysis, reductive proof theory, explicit mathematics and type-theoretic formalisms, and abstract computations. The volume is dedicated to the 60th birthday of Professor Gerhard Jäger, who has been instrumental in shaping and promoting logic in Switzerland for the last 25 years. It comprises contributions from the symposium “Advances in Proof Theory”, which was held in Bern in December 2013.

​Proof theory came into being in the twenties of the last century, when it was inaugurated by David Hilbert in order to secure the foundations of mathematics. It was substantially influenced by Gödel's famous incompleteness theorems of 1930 and Gentzen's new consistency proof for the axiom system of first order number theory in 1936. Today, proof theory is a well-established branch of mathematical and philosophical logic and one of the pillars of the foundations of mathematics. Proof theory explores constructive and computational aspects of mathematical reasoning; it is particularly suitable for dealing with various questions in computer science.

Inhaltsverzeichnis

Frontmatter

A Survey on Ordinal Notations Around the Bachmann-Howard Ordinal

Various ordinal functions which in the past have been used to describe ordinals not much larger than the Bachmann-Howard ordinal are set into relation.

Wilfried Buchholz

About Truth and Types

We investigate a weakening of the classical theory of Frege structures and extensions thereof which naturally interpret (predicative) theories of explicit types and names à la Jäger.

Andrea Cantini

Lindenbaum’s Lemma via Open Induction

With Raoult’s Open Induction in place of Zorn’s Lemma, we do a perhaps more perspicuous proof of Lindenbaum’s Lemma for not necessarily countable languages of first-order predicate logic. We generally work for and with classical logic, but say what can be achieved for intuitionistic logic, which prompts the natural generalizations for distributive and complete lattices.

Francesco Ciraulo, Davide Rinaldi, Peter Schuster

Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory

Until the 1970s, proof theoretic investigations were mainly concerned with theories of inductive definitions, subsystems of analysis and finite type systems. With the pioneering work of Gerhard Jäger in the late 1970 s and early 1980s, the focus switched to set theories, furnishing ordinal-theoretic proof theory with a uniform and elegant framework. More recently it was shown that these tools can even sometimes be adapted to the context of strong axioms such as the powerset axiom, where one does not attain complete cut elimination but can nevertheless extract witnessing information and characterize the strength of the theory in terms of provable heights of the cumulative hierarchy. Here this technology is applied to intuitionistic Kripke-Platek set theories $$\mathbf{IKP }({\mathcal {P}})$$IKP(P) and $$\mathbf{IKP }({\mathcal {E}})$$IKP(E), where the operation of powerset and exponentiation, respectively, is allowed as a primitive in the separation and collection schemata. In particular, $$\mathbf{IKP }({\mathcal {P}})$$IKP(P) proves the powerset axiom whereas $$\mathbf{IKP }({\mathcal {E}})$$IKP(E) proves the exponentiation axiom. The latter expresses that given any sets A and B, the collection of all functions from A to B is a set, too. While $$\mathbf{IKP }({\mathcal {P}})$$IKP(P) can be dealt with in a similar vein as its classical cousin, the treatment of $$\mathbf{IKP }({\mathcal {E}})$$IKP(E) posed considerable obstacles. One of them was that in the infinitary system the levels of terms become a moving target as they cannot be assigned a fixed level in the formal cumulative hierarchy solely based on their syntactic structure. As adumbrated in an earlier paper, the results of this paper are an important tool in showing that several intuitionistic set theories with the collection axiom possess the existence property, i.e., if they prove an existential theorem then a witness can be provably described in the theory, one example being intuitionistic Zermelo-Fraenkel set theory with bounded separation.

Jacob Cook, Michael Rathjen

Machine-Checked Proof-Theory for Propositional Modal Logics

We describe how we machine-checked the admissibility of the standard structural rules of weakening, contraction and cut for multiset-based sequent calculi for the unimodal logics S4, S4.3 and K4De, as well as for the bimodal logic $$\mathrm {S4C}$$S4C recently investigated by Mints. Our proofs for both S4 and S4.3 appear to be new while our proof for $$\mathrm {S4C}$$S4C is different from that originally presented by Mints, and appears to avoid the complications he encountered. The paper is intended to be an overview of how to machine-check proof theory for readers with a good understanding of proof theory.

Jeremy E. Dawson, Rajeev Goré, Jesse Wu

Intuitionistic Decision Procedures Since Gentzen

Gentzen solved the decision problem for intuitionistic propositional logic in his doctoral thesis [31]; this paper reviews some of the subsequent progress. Solutions to the problem are of importance both for general philosophical reasons and because of their use in implementations of proof assistants (such as Coq [4], widely used in software verification) based on intuitionistic logic.

Roy Dyckhoff

The Operational Perspective: Three Routes

Let me begin with a few personal words of appreciation, since Gerhard Jäger is one of my most valued friends and long time collaborators.

Solomon Feferman

Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic

We investigate the (multiagent) infinitary version $$\mathbf {K}_{\omega _1}$$Kω1 of the propositional modal logic $$\mathbf {K}$$K, in which conjunctions and disjunctions over countably infinite sets of formulas are allowed. It is known that the natural infinitary extension $$\mathbf {LK}_{\omega _1}^{\Box }$$LKω1□ (here presented as a Tait-style calculus, $$\mathbf {TK}^{\sharp }_{\omega _1}$$TKω1♯) of the standard sequent calculus $$\mathbf {LK}_p^{\Box }$$LKp□ for $$\mathbf {K}$$K is incomplete with respect to Kripke semantics. It is also known that in order to axiomatize $$\mathbf {K}_{\omega _1}$$Kω1 one has to add to $$\mathbf {LK}_{\omega _1}^{\Box }$$LKω1□ new initial sequents corresponding to the infinitary propositional counterpart $$ BF _{\omega _1}$$BFω1 of the Barcan Formula. We introduce a generalization of standard Kripke semantics, and prove that $$\mathbf {TK}^{\sharp }_{\omega _1}$$TKω1♯ is sound and complete with respect to it. By the same proof strategy, we show that the stronger system $$\mathbf {TK}_{\omega _1}$$TKω1, allowing countably infinite sequents, axiomatizes $$\mathbf {K}_{\omega _1}$$Kω1, although it provably does not admit cut-elimination.

Pierluigi Minari

From Subsystems of Analysis to Subsystems of Set Theory

To honor a part of Gerhard Jäger’s contributions to proof theory we give a non technical, personally biased account of how we got from the proof theory of subsystems of Analysis to the proof theory of subsystems of set theory.

Wolfram Pohlers

Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut

In logical sequent calculi, initial sequents expressing the axiom of identity can be required to be atomic, without affecting the deductive strength of the system. When extending the logical system with right- and left-introduction rules for atomic formulas, one can analogously require that initial sequents be restricted to “uratoms”, which are undefined (not even vacuously defined) atoms. Depending on the definitional clauses for atoms, the resulting system is possibly weaker than the unrestricted one. This weaker system may however be preferable to the unrestricted system, as it enjoys cut elimination and blocks unwanted derivations arising from non-wellfounded definitions, for example in the context of paradoxes.

Peter Schroeder-Heister

Higman’s Lemma and Its Computational Content

Higman’s Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman’s Lemma from a computational and comparative point of view. We give a proof of Higman’s Lemma that uses the same combinatorial idea as Nash-Williams’ indirect proof using the so-called minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proof was given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary well-quasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Gödel’s system T) expressing its computational content.

Helmut Schwichtenberg, Monika Seisenberger, Franziskus Wiesnet

How to Reason Coinductively Informally

We start by giving an overview of the theory of indexed inductively and coinductively defined sets. We consider the theory of strictly positive indexed inductive definitions in a set theoretic setting. We show the equivalence between the definition as an indexed initial algebra, the definition via an induction principle, and the set theoretic definition of indexed inductive definitions. We review as well the equivalence of unique iteration, unique primitive recursion, and induction. Then we review the theory of indexed coinductively defined sets or final coalgebras. We construct indexed coinductively defined sets set theoretically, and show the equivalence between the category theoretic definition, the principle of unique coiteration, of unique corecursion, and of iteration together with bisimulation as equality. Bisimulation will be defined as an indexed coinductively defined set. Therefore proofs of bisimulation can be carried out corecursively. This fact can be considered together with bisimulation implying equality as the coinduction principle for the underlying coinductively defined set. Finally we introduce various schemata for reasoning about coinductively defined sets in an informal way: the schemata of corecursion, of indexed corecursion, of coinduction, and of corecursion for coinductively defined relations. This allows to reason about coinductively defined sets similarly as one does when reasoning about inductively defined sets using schemata of induction. We obtain the notion of a coinduction hypothesis, which is the dual of an induction hypothesis.

Anton Setzer

Pointwise Transfinite Induction and a Miniaturized Predicativity

The basis of this work is Leivant’s [6] theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people; for example, Spoors and Wainer [13] built a hierarchy of ramified theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, in terms of a predicatively generated infinitary calculus with stratifications of numerical inputs up to and including level $$\omega $$ω. The autonomous ordinals are those below $$\Gamma _0$$Γ0, but they are generated according to a weak (though quite natural) notion of transfinite induction whose computational strength is “slow” rather than “fast” growing. It turns out that the provably computable functions are now those elementary recursive in the Ackermann function (i.e. Grzegorczyk’s $$\omega $$ωth level). All this is closely analogous to recent works of Jäger and Probst [5] and Ranzi and Strahm [9] on iterated stratified inductive definitions, but their theories have full, complete induction as basis, whereas ours have only a weak, ramified form of numerical induction at bottom.

Stanley S. Wainer
Weitere Informationen

Premium Partner

Neuer Inhalt

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Product Lifecycle Management im Konzernumfeld – Herausforderungen, Lösungsansätze und Handlungsempfehlungen

Für produzierende Unternehmen hat sich Product Lifecycle Management in den letzten Jahrzehnten in wachsendem Maße zu einem strategisch wichtigen Ansatz entwickelt. Forciert durch steigende Effektivitäts- und Effizienzanforderungen stellen viele Unternehmen ihre Product Lifecycle Management-Prozesse und -Informationssysteme auf den Prüfstand. Der vorliegende Beitrag beschreibt entlang eines etablierten Analyseframeworks Herausforderungen und Lösungsansätze im Product Lifecycle Management im Konzernumfeld.
Jetzt gratis downloaden!

Bildnachweise