# Project

Back to overview

## Algebraic and Logical Aspects of Knowledge Processing

 English title Algebraic and Logical Aspects of Knowledge Processing Jäger Gerhard 156061 Project funding (Div. I-III) Institut für Informatik Universität Bern University of Berne - BE Mathematics 01.10.2014 - 30.11.2017 273'096.00
Show all

### All Disciplines (2)

Discipline
 Mathematics
 Information Technology

### Keywords (6)

subsystems of set theory and second order arithmet; higher inductive types; explicit mathematics; operational set theory; theories of sets and classes; proof theory

### Lay Summary (German)

Dieses Projekt beschaeftigt sich mit der beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Arithmetik zweiter Stufe sowie von Systemen der sogenannten Explicit Mathematics und Operational Set Theory. Im Vordergrund stehen ordinalzahltheoretische Fragestellungen und Aspekte einer Abstract Computability.
Lay summary

Den allgemeinen Rahmen dieses Projekts bilden beweistheoretische Untersuchungen von Teilsystemen der Mengenlehre, der Arithmetik zweiter Stufe sowie Systemen der Explciit Mathematics und Operational Set Theory. Wir untersuchen speziell Wohlordnungsbeweise im Zusammenhang mit hoeheren Typen und geeigneten induktiven Definitionen. Ein weiterer Aspekt besteht in der Untersuchung einer "Abstract Computability Theory" in einem operationellen Rahmen mit dem Ziel, in Richtung einer operationellen deskriptiven Mengenlehre zu gehen.

 Direct link to Lay Summary Last update: 30.09.2014

### Responsible applicant and co-applicants

Name Institute
 Jäger Gerhard Institut für Informatik Universität Bern
 Strahm Thomas Institut für Informatik Universität Bern

Name Institute

### Publications

Publication
Probst Dieter (2017), A modular ordinal analysis of metapredicative subsystems of second order arithmetic, Habilitation - Selbstverlag, Bern.
Gopal TV, Jäger Gerhard, Steila Silvia (ed.) (2017), Theory and Applications of Models of Computation TAMC 2017, Springer, Cham.
Jäger Gerhard (2016), Relativizing operational set theory, in The Bulletin of Symbolic Logic, 22, 332-352.
Buchholtz Ulrik, Jäger Gerhard, Strahm Thomas (2016), Theories of proof-theoretic strength $\psi$($\Gamma_{\Omega+1}$), in Probst Dieter, Schuster Peter (ed.), De Gruyter, Berlin, 115-140.
Sato Kentaro, Zumbrunnen Rico (2015), A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP, in Annals of Pure and Applied Logic, 166, 121-186.
Jäger Gerhard, Probst Dieter (2015), A proof-theoretic analysis of theories for stratified inductive definitions, in Rathjen Michael, Kahle Reinhard (ed.), Springer, Cham, 425-454.
Eberhard Sebastian (2015), Applicative theories for logarithmic complexity classes, in Theoretical Computer Science, 585, 115-135.
Ranzi Florian (2015), From a Flexible Type System to Metapredicative Wellordering Proofs, Selbstdruck Dissertation, Bern.
Sommaruga Giovanni, Strahm Thomas (ed.) (2015), Turing's Revolution: The Impact of His Ideas about Computability, Birkhäuser, Basel.
Eberhard Sebastian, Strahm Thomas (2015), Unfolding Feasible Arithmetic and Weak Truth, in Achourioti T., Galinon H., Fujimoto K., Martínez Fernández J. (ed.), Springer, Heidelberg, 153-167.
Ranzi Florian, Strahm Thomas (2014), A note on the theory $\mathsf{SID}_{{<}\omega}$ of stratified induction, in Mathematical Logic Quarterly, 60, 487-497.
Jäger Gerhard, Zumbrunnen Rico (2014), Explicit mathematics and operational set theory: some ontological comparisons, in The Bulletin of Symbolic Logic, 20, 275-292.

### Collaboration

Group / person Country
Types of collaboration
 Prof. Dr. S. Feferman, Department of Mathematics, Stanford University United States of America (North America)
 - in-depth/constructive exchanges on approaches, methods or results
 Prof. Dr. George Metcalfe, Mathematisches Institut, Universität Bern Switzerland (Europe)
 - in-depth/constructive exchanges on approaches, methods or results
 Prof. Dr. W. Buchholz, Prof. Dr. H. Schwichtenberg, Mathematisches Institut, Universität München Germany (Europe)
 - in-depth/constructive exchanges on approaches, methods or results- Exchange of personnel

### Scientific events

#### Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
 Axiomatic Thinking Talk given at a conference Axiomatic Systems: An Operational Perspective 15.09.2017 Zürich, Switzerland Jäger Gerhard;
 Humboldt Kolleg Proof Theory as Mathesis Universalis Talk given at a conference Kripke-Platek and Friends 24.07.2017 Loveno di Menaggio, Italy Jäger Gerhard;
 Solomon Feferman Symposium Talk given at a conference Conceptual Expansions 05.06.2017 Stanford, United States of America Jäger Gerhard;
 CUNY Seminar Individual talk From Operations to Sets and Back 30.05.2017 New York, United States of America Jäger Gerhard;
 Logic Seminar Individual talk Operations and Sets: a Historical Perspective 31.03.2017 Florenz, Italy Jäger Gerhard;
 Operations, Sets, and Types OST17 Talk given at a conference Recursion theory in applicative theories 08.03.2017 Bern, Switzerland Rosebrock Timotej Alexander;
 Operations, Sets, and Truth Talk given at a conference Weak theories of operations, types, and truth 16.12.2016 Florenz, Italy Strahm Thomas;
 Operations, Sets, and Truth Talk given at a conference About Fixed Points 16.12.2016 Florenz, Italy Jäger Gerhard;
 Logic Seminar Individual talk Metapredicativity 10.03.2016 Bologna, Italy Jäger Gerhard;
 Trends in Proof Theory Talk given at a conference A Feferman-style type system for the small Veblen ordinal 20.09.2015 Hamburg, Germany Strahm Thomas;
 Trends in Proof Theory Talk given at a conference Recent Developments in Operational Set Theory 20.09.2015 Hamburg, Germany Jäger Gerhard;
 Utrecht Workshop on Proof Theory Talk given at a conference Unfolding schematic systems – with an emphasis on inductive definitions 16.04.2015 Utrecht, Netherlands Strahm Thomas;
 Arbeitstagung Bern-München Talk given at a conference Semi-Decidability in Explicit Mathematics 18.12.2014 München, Germany Rosebrock Timotej Alexander;
 Arbeitstagung Bern-München Talk given at a conference A flexible type system for the small Veblen ordinal 18.12.2014 München, Germany Ranzi Florian;
 Mathematical Logic: Proof Theory, Constructive Mathematics Talk given at a conference A flexible type system for the small Veblen ordinal 16.11.2014 Oberwolfach, Germany Strahm Thomas;

#### Self-organised

Title Date Place
 Theory and Applications of Models of Computation TAMC 2017 20.04.2017 Bern, Switzerland
 Operations, Sets, and Types OST17 08.03.2017 Bern, Switzerland
 Arbeitstagung Bern-München 25.05.2016 Bern, Switzerland

### Associated projects

Number Title Start Funding scheme
 149680 Operational Set Theory 01.02.2014 Research semester
 162321 Function algebras and theories for computational complexity 01.06.2015 International short research visits
 137678 Algebraic and Logical Aspects of Knowledge Processing 01.10.2011 Project funding (Div. I-III)

### Abstract

The general framework of this project is the proof-theoretic analysis of systems of second order arithmetic and set theory, of explicit mathematics, of type theories, and of theories of truth. We are particularly interested in determining the proof-theoretic and consistency strength of standard systems that play an important role in the foundations of mathematics and (to a certain extent) in computer science and in developing novel formal frameworks tailored for specific needs.We continue the research done in the previous years, in particular in connection with the prede- cessor project SNSF 200020-137678. However, also two new perspectives will be brought in:• Higher type well-ordering proofs, the metapredicativity of the Bachmann-Howard ordinal and beyond (taking up an old topic from a new angle).• A class extension of operational set theory.In grouping our prospective research activities, we follow conceptual criteria that apply to various systems and try to discuss them from a higher-level perspective. Keeping this in mind the project is structured in three streams as follows.The first stream is about higher dimensional inductions, as we call them and addresses the following topics:• Higher type accessible part well-ordering proofs as a means in metapredicative proof theory.• Weak well-orders in theories of sets and classes as crucial tool of lifting proof-theoretic results from systems of second order arithmetic to strong set theories.The second stream studies the several foundationally relevant axiomatic frameworks from an operational perspective. One important aspect has to do with an abstract computability theory and activities in the direction of an operational descriptive set theory. A further open probem deals with attempts to formulate operational set theory with classes and natural reflection principles. The last stream of the project is devoted to various feasible and subrecursive proof and type systems. In particular, the focus is put on the following questions:• Study various operational versions of Weak König’s Lemma and determine their proof-theoretic strength.• Develop weak arithmetical truth theories in the style of Kripke-Feferman and Friedman-Sheard whose strength is significantly below that of Peano arithmetic PA.• Define and analyze various weak set theories, ranging from operational set theories to so-called safe set theories.
-