Arbeitstagung Bern–München–Verona 2024
29–30 November 2024
LMU Munich: Department of Mathematics
Theresienstraße 39, Room B 349
Programme
Thursday, 28 November
19:00 Welcome dinner at Café Puck, Türkenstraße 33
Friday, 29 November
09:00 – 09:45 Klaus Mainzer: From Computing to AI. Logical, Mathematical, Technical, and Philosophical Foundations
09:45 – 10:30 Gerhard Jäger: Explicit Mathematics: Universes and Ordinals
10:30 – 11:00 Coffee break
11:00 – 11:45 Takako Nemoto: (not weak) Konig’s lemma and fan theorem
11:45 – 12:30 Thomas Studer: Simplicial Models for Epistemic Logic
12:30 – 14:00 Lunch break
14:00 – 14:45 Valentin Müller: Higher-Level Natural Deduction and Subformula Property for Kreisel-Putnam Logic
14:45 – 15:30 Borja Sierra-Miranda: Cut elimination for a non-wellfounded system for the master modality
15:30 – 16:00 Coffee break
16:00 – 16:45 Elio La Rosa: Epsilon Terms and Lambda Binders
16:45 – 17:30 Eduardo Skapinakis: A recursion-theoretic characterization of monotone NP
17:30 – 18:15 Luis Gambarte: Categorical constructions on computability models
19:00 Dinner at Los Faroles, Nordendstraße 26
Saturday, 30 November
09:00 – 09:45 Iosif Petrakis: Apart algebras
09:45 – 10:30 Ingo Blechschmidt: Modal operators for a constructive account of well-quasi-orders
10:30 – 11:00 Coffee break
11:00 – 11:45 Franziskus Wiesnet: Material Interpretation – A Case Study
11:45 – 12:30 Giulio Fellin: Conservation for nuclei over substructural entailment relations
Abstracts
Ingo Blechschmidt (University of Antwerp)
Modal operators for a constructive account of well quasi-orders
Well quasi-orders are a combinatorial notion with featureful applications in graph theory, termination checking, commutative algebra and other subjects. However, their classical definition, though concise and elegant, poses significant challenges in constructive mathematics and frameworks that lack function sets. In response, several constructive substitutes have been developed, most recently an implicational definition by Stefano Berardi, Gabriele Buriola and Peter Schuster. In this talk, we investigate how a modal approach can reinterpret classical proofs involving transfinite methods as blueprints for constructive proofs grounded in these alternatives, thereby combining the best of both worlds: Short and abstract proofs, but with constructive content. We also indicate how the modal approach allows us to compare the implicational definition with an earlier inductive one. Annotated slides available.
Giulio Fellin (University of Brescia)
Conservation for nuclei over substructural entailment relations
Glivenko’s theorem has been studied in an abstract setting, where double negation is replaced by arbitrary nuclei, and classical and intuitionistic propositional logics are generalised to abstract entailment relations. This paper extends that framework to substructural logics, focusing on cases where structural rules such as weakening, contraction, and exchange are restricted. We show that while the absence of weakening or contraction has minimal impact; the absence of the exchange rule introduces significant and nontrivial distinctions. This is a joint work with Tarmo Uustalu and Cheng-Syuan Wan.
Luis Gambarte (LMU Munich)
Categorical constructions on computability models
The notion of a computability model was introduced by Longley as a way to abstract different concepts in theoretical computer science and logic like typed partial combinatory algebras or λ-calculus. We explore the existence (or lack thereof) of standard categorical constructions in the category of these computability models and compare them to the same constructions in related categories. Furthermore we give a brief exposition of categories with computability bases and how they can be related to computability models.
Gerhard Jäger (University of Bern)
Explicit Mathematics: Universes and Ordinals
We show how an ordering of specific universes may lead to a sort of ordinals. Afterwards we present two ways how to extend Explicit Mathematics by ordinals in a natural and powerful way.
Elio La Rosa (LMU Munich)
Epsilon Terms and Lambda Binders
Hilbert's epsilon terms are strictly more expressive than first-order quantifiers. This is because the formula in the scope of the epsilon operator denotes the extension from which a witness, if any, is chosen from. On the other hand, epsilon terms cannot unambiguously replicate quantifiers' scoping mechanism. This is because, being terms, they only occur in the atoms of a language. As a result, when added to Intuitionistic logic, epsilon terms are not conservative over Intuitionistic quantifiers, which are sensible to quantifiers shifts. Similarly, it is hard to define analytic rules handling epsilon terms, since there is no direct way to single out newly introduced terms in a sequent. In this talk, I extend the language of epsilon calculus by lambda binders. In one of his earliest papers, Melvin Fitting uses such a language with modalities to develop an S4 extension of epsilon calculus. I show that this approach results in an overlooked extension of the S4 embedding of Intuitionistic logic with epsilon terms which is conservative over Intuitionistic quantification. In this case, lambdas are treated as predicate abstraction operators. I show that this approach is not enough for defining analytic rules, where it seems that lambda binders should subsume the epsilon ones as well.
Klaus Mainzer (TUM, CFvWZ Center)
From Computing to AI. Logical, Mathematical, Technical, and Philosophical Foundations
Technical-practical limits of today's computers and AI depend on the theoretical foundation of digital computability. On the basis of digital computability, symbolic AI was initially oriented towards the logical reasoning of symbolic logic. Statistical learning from big data led to machine learning, which dominates the techno-economic breakthroughs of AI today. Some limits of digital computability, decidability and solvability of problems can be theoretically overcome beyond Turing computability with real computing. Novel analog computer architectures orientated towards the human brain enable its technical-practical realization. An extension to hybrid AI is requested for, combining digital, analog and real computing in neuromorphic computing structures. These tendencies of research and innovation demonstrate that we need more integrated research in the foundations of logic, mathematics, physics, engineering sciences, cognitive science, and philosophy. References: K. Mainzer, *The Digital and the Real World. Computational Foundations of Mathematics, Science, Technology, and Philosophy,* World Scientific Singapore 2018; K. Mainzer, *Artificial Intelligence. When do Machines take over?* Springer: Berlin 2nd edition 2019 (Chinese: Tsinghua University Press: Beijing 2022); K. Mainzer, R. Kahle, *Limits of AI – theoretical, practical, ethical*, Springer: Berlin 2024 (German: Springer: Berlin 2022); K. Mainzer, *Artificial Intelligence of Neuromorphic Systems*, World Scientific Singapore 2024; K. Mainzer, P. Schuster, H. Schwichtenberg (eds.), *Proof and Computation I-II*, World Scientific Singapore 2018-2022.
Valentin Müller (University of Bern)
Higher-Level Natural Deduction and Subformula Property for Kreisel-Putnam Logic
We introduce a new natural deduction system for Kreisel-Putnam logic. Our system is based on Schroeder-Heister's calculus of higher-level rules, an extension of ordinary natural deduction in which not only formulas, but also rules can act as assumptions that may be discharged in the course of a derivation. We will establish a normalization theorem, i.e., we will show that every deduction in our system can be converted into a deduction without "detours". The method used for this is new and might also be applied to other non-classical logics. As a consequence of this result, we will obtain an unrestricted subformula property and a separation theorem for our system.
Takako Nemoto (Tohoku University)
(not weak) Konig’s lemma and fan theorem
In [1], it is proved that weak Konig's lemma with uniqueness condition WKL! is equivalent to the decidable binary fan theorem. Analogously, we can prove that KL! implies the decidable (non-binary) fan theorem, but the converse seems difficult. In this talk, we will show these analogy and difficulty, and related principles. [1] Josef Berger and Hajime Ishihara. Brouwer's fan theorem and unique existence in constructive analysis. Math. Log. Quart., 51(4):360–364, 2005.
Iosif Petrakis (University of Verona)
Apart algebras
Sambin and Ciraulo developed the theory of overlap algebras as an algebraic generalisation of the overlap relation between subsets. Overlap algebras correspond classically to complete Boolean algebras and intuitionistically to complete Heyting algebras. We introduce apart algebras as an algebraic generalisation of the apart relation between subsets. The duality between the overlap and the apart relation between subsets is extended to the duality between the theory of overlap and apart algebras. While overlap algebras induce a canonical positivity predicate and are formal topologies, apart algebras induce a canonical negativity predicate and are formal cotopologies. While the regular elements of an overlap topology form an overlap algebra, the coregular elements of an apart topology form an apart algebra.
Borja Sierra-Miranda (University of Bern)
Cut elimination for a non-wellfounded system for the master modality
In [1], we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method to proofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides a cut-elimination method using only basic tools of structural proof theory and corecursion, which is needed due to working in a non-wellfounded setting. We will employ our method to obtain syntactic cut-elimination for K+, a system of modal logic with the master modality. [1]: Borja Sierra Miranda, Thomas Studer and Lukas Zenger. "Coalgebraic Proof Translations of Non-Wellfounded Proofs". In Agata Ciabattoni, David Gabelaia and Igor Sedlár (eds). (2024) Advances in Modal Logic, Vol. 15. College Publications.
Eduardo Skapinakis (University of Tübingen)
A recursion-theoretic characterization of monotone NP
Part of the research in circuit complexity since the 1970s has been devoted to proving lower bounds in restricted circuit classes. A famous example is Razborov's lower bound for monotone circuits, where only AND and OR gates are allowed. To give a unified theory of monotone computation, Grigni and Sipser extended the notion of monotonicity beyond circuits and defined monotone non-deterministic Turing machines. These are non-deterministic Turing machines which are monotone on their input tape, but are allowed to perform negative operations on their work tapes and non-deterministically generated bits. Under this formalism, Razborov's result can be stated as "monotone P is strictly contained in monotone NP". In this talk, I will introduce a new computational model of monotone non-determinism, where only monotone operations are allowed, and show that, with polynomial time bounds, one still obtains Grigni and Sipser's monotone NP. Based on this model, I will present a characterization of monotone NP as the closure of a set of basic functions under three operators.
Thomas Studer (University of Bern)
Simplicial Models for Epistemic Logic
Simplicial models originated in distributed computing, serving as a tool to study task solvability. They also provide a fresh view of the semantics of multi-agent epistemic logic. The main building blocks of simplicial models are local states of agents instead of (global) possible worlds. This change of perspective leads to novel logical operators and makes new applications possible. In this talk, we will provide an introduction to simplicial models and present recent developments.
Franziskus Wiesnet (TU Wien)
Material Interpretation – A Case Study
We explore the constructive characterization of all maximal ideals in ℤ[X], which serves as a case study for the concept of the "Material Interpretation". Starting with a classical proof, we demonstrate how it can be transformed into a constructive proof, potentially leading to stronger statements. The Material Interpretation provides an alternative proof interpretation, transforming statements of the form A → B into ¬A ∨ B, where ¬A represents a constructively stronger form of the negation of A. We will discuss the theoretical foundations of this approach as well as its formalization in the proof assistant Agda, which is still a work in progress. Furthermore we highlight Agda's capabilities for automating the Material Interpretation and share improvements to its library through the addition of valuable theorems.
Accommodation
Pension Josefine (Nordendstraße 13)
Hotel Antares (Amalienstraße 20)
Contact
Helmut Schwichtenberg
Daniel Misselbeck-Wessel
Last update: Thursday, 28 November 2024