Project

Back to overview

Algebraic and Logical Aspects of Knowledge Processing

English title Algebraic and Logical Aspects of Knowledge Processing
Applicant Jäger Gerhard
Number 156061
Funding scheme Project funding (Div. I-III)
Research institution Institut für Informatik Universität Bern
Institution of higher education University of Berne - BE
Main discipline Mathematics
Start/End 01.10.2014 - 30.11.2017
Approved amount 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)

Lead
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

Employees

Publications

Publication
A modular ordinal analysis of metapredicative subsystems of second order arithmetic
Probst Dieter (2017), A modular ordinal analysis of metapredicative subsystems of second order arithmetic, Habilitation - Selbstverlag, Bern.
Theory and Applications of Models of Computation TAMC 2017
Gopal TV, Jäger Gerhard, Steila Silvia (ed.) (2017), Theory and Applications of Models of Computation TAMC 2017, Springer, Cham.
Relativizing operational set theory
Jäger Gerhard (2016), Relativizing operational set theory, in The Bulletin of Symbolic Logic, 22, 332-352.
Theories of proof-theoretic strength $\psi$($\Gamma_{\Omega+1}$)
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.
A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP
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.
A proof-theoretic analysis of theories for stratified inductive definitions
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.
Applicative theories for logarithmic complexity classes
Eberhard Sebastian (2015), Applicative theories for logarithmic complexity classes, in Theoretical Computer Science, 585, 115-135.
From a Flexible Type System to Metapredicative Wellordering Proofs
Ranzi Florian (2015), From a Flexible Type System to Metapredicative Wellordering Proofs, Selbstdruck Dissertation, Bern.
Turing's Revolution: The Impact of His Ideas about Computability
Sommaruga Giovanni, Strahm Thomas (ed.) (2015), Turing's Revolution: The Impact of His Ideas about Computability, Birkhäuser, Basel.
Unfolding Feasible Arithmetic and Weak Truth
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.
A note on the theory $\mathsf{SID}_{{<}\omega}$ of stratified induction
Ranzi Florian, Strahm Thomas (2014), A note on the theory $\mathsf{SID}_{{<}\omega}$ of stratified induction, in Mathematical Logic Quarterly, 60, 487-497.
Explicit mathematics and operational set theory: some ontological comparisons
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.
-