# Oberseminar Mathematische Logik

Veranstalter: J. Berger, W. Buchholz, H.-D. Donder, H. Osswald, I. Petrakis, P. Schuster, H. Schwichtenberg## Zeit und Ort

Mi 16:30-18, B252## SS 2024

- Pierluigi Minari, 17. July 2024.
Proof-Theoretical Methods in Equational Theories of Untyped
Operations: A Survey

Abstract: This talk surveys the ideas, results, and applications of a proof-theoretical approach to equational theories of untyped operations, including combinatory logic and lambda calculus, which I have developed over the years. This approach is based on the introduction and proof-theoretical investigation of "analytic" proof systems for such theories. Analyticity is achieved through a key result of transitivity elimination, which results in a significant streamlining of the proof theory of the corresponding theories and enables various applications. Notably, this includes a positive solution to an open problem in the theory of combinatory strong reduction, originally posed by H.B. Curry approximately 60 years ago.

## Frühere Vorträge im SS 2024

- Hajime Ishihara, 10. July 2024.
Constructive uniform spaces, topological vector lattices and integration

Abstract: We introduce the constructive notion of a uniform space with the spirit of Sambin's notion of a basic pair, and construct a completion of a uniform space and a product of uniform spaces. We show some natural properties of the completion and the product. Then we define topological linear spaces and topological vector lattices as linear spaces and vector lattices equipped with uniform structures, and show that these algebraic and topological structures are preserved under the completion. We introduce the notion of an abstract integration space consisting of a vector lattice and a positive linear functional. By defining two uniform structures on an abstract integration space, we define corresponding topological vector lattices, and spaces of integration and measurable functions as the completion of these topological vector lattices. Finally, we show some convergence theorems on these spaces such as Lebesgue's monotone and dominated convergence theorems and Fatou's lemma. - Yannick Ehrhardt, 3. July 2024. Categories with 2-dependent arrows

Abstract. Category Theory allows for the generalization of (non-dependent) functions between sets. However, in Martin Löf Type Theory, other kinds of objects, like families of types, Σ-types, dependent functions, and maps between families, play a fundamental role. These cannot be captured by the regular notion of a category and thus require additional structure to be presented categorically. In this talk, we first present the structures introduced in [3] to put families, Σ-objects, and dependent functions into a common categorical language, extending in this way the work of Pitts in [2]. These are fam-, (fam,Σ)- and dep-categories, which add fam-arrows, Σ-objects and dep-arrows respectively, as well as (dep,Σ)-categories, which combine the notions of (fam,Σ)- and dep-categories. In [1] we extend these by adding a structure that aims to generalize maps between families of types, namely 2-fam-arrows, which are arrows between family arrows. This leads to our study of 2-fam-, (2-fam,Σ)-, 2-dep- and (2-dep,Σ)-categories. [1] Y. Ehrhardt: 2-dep Categories, Bachelor Thesis, LMU, 2024. [2] A. M. Pitts: Categorical logic, in S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (Eds.) Handbook of Logic in Computer Science, Vol.~5, Clarendon Press, Oxford, 2000, 39-128. [3] I. Petrakis: Categories with dependent arrows, arXiv:2303.14754v1, 2023 - Francesco Paoli, 22. May 2024. Sequent calculi for first-order ST

Abstract. Strict-Tolerant Logic (ST) underpins a theory of truth that includes a fully disquotational truth predicate without jettisoning any classically valid law. The classical sequent calculus without Cut is sometimes advocated as an appropriate proof-theoretic presentation of ST. Unfortunately, there is only a partial correspondence between its derivability relation and the semantic relation of ST-validity: these relations coincide only upon the addition to the calculus of elimination rules and only within its propositional fragment, due to the non-invertibility of the quantifier rules. In this paper, we present three calculi for first-order ST with an eye to recapturing this correspondence in full. The first calculus is close in spirit to the Epsilon calculus. The other two calculi include rules for the discharge of sequent-assumptions; moreover, one of them is normalisable and admits interpolation.

## WS 2023/24

- Matthias Eberl, 7. Februar 2024. Formalizing the Potential Infinite.

Abstract: We present a formalization of the potential infinite as a dynamic, extensible model of a fragment of simple type theory. This fragment allows the interpretation of (a version of) classical higher-order logic. The model is based on a generalization of direct and inverse systems and their limits, which can be regarded as "dynamic sets". To deal with higher-order objects, one needs dynamic objects as well. The model requires the formalization of (i) the notion that these (dynamic) sets and objects have "indefinitely many" states and (ii) the notion of a state of an object that is "indefinitely large" relative to a context of other stages. An indefinitely large state of a set will be formalized as a limit of a system, which is, from a consequent finitistic reading, inside the system itself. One main difference to common models is that equality is no longer an equivalence relation on a single set, but a relation between different states of an object. We will show that this notion of equality, based on the understanding of infinity as extensibility, leads to different models than domain theoretic models. These differences are significant for functions of type 2. - Luca Maio, 17. Januar 2024, 14:00-15:30 (!), Raum B349 (!).
Bishop's Compilation Theorem.

Abstract: Erret A. Bishop is well known in the community of constructive mathematicians for his work on informal constructive set theory and informal constructive analysis. However among his unpublished work, manuscripts have been found that, along some of his published work, concern themselves with formal foundations of mathematics. In this Thesis we Present two systems from this unpublished work. First a simply typed one called System *Σ* for which we have also provided Bishop's concept of compilation, a re-discovery of core concepts of realizability theory, we show that *Σ* is sound through polishing the proof Bishop gives himself. Second we discuss his draft for a dependently typed system, which is built to reflect all of Bishop Set Theory. - Hajime Ishihara, 17. Januar 2024, 16:30-18, B252. Constructive uniform spaces.
- Ioannis Andreou, 22. November 2023. Categorical Aspects of Quantum
Lambda Calculus.

Abstract: Quantum computers intrinsically differ from classical ones and consequently the theory of classical computations can not be applied to them. Therefore here a lambda calculus for quantum computation is presented. As an introduction the fundamentals of quantum computation are being explained, afterwards we analyze the mathematics of quantum mechanics categorically and use the findings to draw connections to logic. For that matter light is also shed on linear logic and its properties. Finally a quantum lambda calculus is presented, with a typing system based on linear logic. The calculus is analyzed thoroughly and its operational semantics are clarified. Additionally a comparison of its categorical semantics to the categories found in quantum mechanics is made. - Jasmin Blanchette, 15. November 2023. Lambda-Superposition:
From Theory to Trophy. (Joint work with Alexander Bentkamp, Simon
Cruanes, Visa Nummelin, Stephan Schulz, Sophie Tourret, Petar
Vukmirović, and Uwe Waldmann)

Abstract: Lambda-superposition is a new proof calculus for higher-order logic. To a large extent, the calculus is a graceful generalization of standard superposition, which is a highly successful calculi for first-order logic. On the theory side, we proved lambda-superposition refutationally complete. On the practical side, we implemented it in the E and Zipperposition provers. Zipperposition finished first in the higher-order theorem division of the CADE ATP System Competition in 2020, 2021, and 2022, suggesting that superposition is a valuable approach also in a higher-order setting.

## SS 2023

- Giulio Fellin, 19. Juli 2023. Modal logic for induction:
from chain conditions to arithmetic.

Abstract: We use modal logic to obtain syntactical, proof-theoretic versions of transfinite induction as axioms or rules within an appropriate labelled sequent calculus. While transfinite induction proper, also known as Noetherian induction, can be represented by a rule, the variant in which induction is done up to an arbitrary but fixed level happens to correspond to the Gödel–Löb axiom of provability logic. To verify the practicability of our approach in actual practice, we sketch a fairly universal pattern for proof transformation and test its use in several cases. Among other things, we give a direct and elementary syntactical proof of Segerberg’s theorem that the Gödel–Löb axiom characterises precisely the (converse) well-founded and transitive Kripke frames. We then show that, by adding appropriate rules, this approach allows us to obtain a calculus for a bounded version of Peano Arithmetic. Finally, we observe that, by slightly modifying the rules, we can do the same for arithmetic in ordinals other than ω. - Dmytro Bondarenko, 10. Mai 2023. Completion of a uniform space
by means of the notion of a net.

Abstract: In this lecture, we will give a predicative completion of a uniform space with pseudometric. To this end, we generalise the notion of a sequence into a notion of a net, explore it’s properties and characterise constructed completion - Yoan Geran, 8. Februar 2023, Exporting first-order proofs using
Dedukti: the example of Geocoq.

Abstract: The proofs of the proposition in Euclid Book I have been formalised in the Coq library GeoCoq. We translate them into the Logical Framework Dedukti (based on the Lambda-Pi-Calculus modulo rewriting). Then, we simplify these proofs to express them in an encoding of the Predicate Logic and translate them in Coq, HOL Light, Matita, Lean, Open Theory and PVS (as proof terms). It is a great example of proof systems interoperability. Moreover, we have been able to translate back the proofs to the tactic language of Coq, which is a promising step towards exporting into other proof assistants using their own tactic language. - Daniel Wessel, 7. Dezember 2022, Towards free radical theory.

Abstract: There ought to be a "free" radical theory that accounts for a plethora of intersection principles in algebra, lattice theory and beyond. We employ basic concepts from (impredicative) point-free topology to obtain a rather broad perspective, and try to read the latter in the context of dynamical algebra: the universal property of radical operators sheds light on why the dynamical method must draw certain conclusions. We will thus carry on a discussion about Krull's Fundamentalsatz, held in Fischbachau during the Proof & Computation autumn school 2022.

This talk is partly based on joint work with Peter Schuster. - Iosif Petrakis, 30. November 2022, Categories with dependent arrows.

Abstract: An arrow is the abstract, categorical version of a function. What is the abstract, categorical version of a dependent function? To answer this question, we first present the notion of fam-Category, a category with family-arrows. A (fam, Sigma)-Category is a fam-Category with Sigma-objects, where a (fam, Sigma)-Category with a terminal object is exactly a type-category of Pitts, or a category with attributes of Cartmell. We introduce categories with dependent-arrows, or dep-Categories, and we show that every (fam, Sigma)-Category is a dep-Category in a canonical way. The notion of a Sigma-object in a dep-Category is affected by the existence of dependent-arrows, and we show that every (fam, Sigma)-Category is a (dep, Sigma)-Category in a canonical way. All these notions of categories have a dual counterpart.

## Frühere Vorträge im SS 2022

- Steve Awodey, 21. September 2022, Algebraic type theory.

Abstract: A type theoretic universe E —> U bears an algebraic structure resulting from the type-forming operations of unit type, identity type, dependent sum, and dependent product, which may be generalized to form the concept of a "Martin-Löf algebra". A free ML-algebra is then a model of type theory with special properties. The general theory of such ML-algebras can be seen as a proof-relevant version of the theory of Zermelo-Fraenkel algebras from the algebraic set theory of Joyal-Moerdijk. (This is work in progress.) - Helmut Schwichtenberg, Verified algorithms via proofs
(j.w.w. Nils Köpp), 17. August 2022, 17:00 (!)

Abstract: Real numbers in [-1,1] can be represented by streams of signed digits -1,0,1. Algorithms operating on such streams can be extracted from formal proofs involving a unary coinductive predicate CoI on (standard) real numbers x: a realizer of CoI(x) is a stream representing x. We address the question how to obtain bounds for the lookahead of such algorithms: how far do we have to look into the input streams to compute the first n digits of the output stream? We present a proof-theoretic method how this can be done. The idea is to replace the coinductive predicate CoI(x) by an inductive predicate L(x,n) with the intended meaning that we know the first n digits of a stream representing x. - Ihsen Yengui, Algorithms for computing syzygies over V[X_1,…,X_n],
V a valuation ring, 15. Juni 2022.

Abstract: I will present a general algorithm for computing a finite generating set for the syzygies of any finitely generated ideal of V[X_1,...,X_k] (V a valuation domain) which does not use Gröbner bases. This algorithm is based on a notion of "echelon form" which ensure its correctness. Its termination proof is combinatorial. - Edi Pavlović (MCMP) 8. Juni 2022, Proof theory of free logics

Abstract: Free logics are a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that (i) the domain of interpretation is not empty, (ii) every name denotes exactly one object in the domain and (iii) the quantifiers have existential import. Free logics reject the claim that names need to denote in (ii), and positive free logic concedes that some atomic formulas containing non-denoting names (including at least self-identity) are true, negative free logic treats them as uniformly false, and neutral free logic as taking a third value. These various logics also have complex and varied axiomatizations and semantics, and the present work is a part of an ongoing project to offer, using primarily sequent calculi, an orderly examination of the various systems and their mutual relations. - Norbert Gratzl (MCMP), 27. April 2022, Extensional Saturation

## Frühere Vorträge im WS 2021/22

- Iosif Petrakis, Computability models over categories and presheaves,
16. März 2022

Abstract: Generalising slightly the notions of a strict computability model and of a simulation between them, which were elaborated by Longley and Normann, we define canonical computability models over certain categories and appropriate presheaves on them. We study the canonical total computability model over a category C and a covariant presheaf on C, and the canonical partial computability model over a category C with pullbacks and a pullback preserving, covariant presheaf on C. These computability models are shown to be special cases of a computability model over a category C with a so-called base of computability and a pullback preserving, covariant presheaf on C. In this way Rosolini's theory of dominions is connected with the theory of computability models. - Iosif Petrakis, On the right notion of negation in constructive
mathematics, 23. Februar 2022

Abstract: In standard constructive logic negation is treated as in classical logic in a negativistic and weak way. This is in contrast to the use of a positive and strong "or" and "exists". In constructive mathematics however we often find a positive and strong approach to negation. This fact motivates a clear distinction between a positive and strong negation and the standard weak negation. Bringing together older ideas of Griss and Nelson and recent work of Shulman [2] and ours [1], we investigate the role of a positive and strong negation in constructive mathematics and constructive logic.

[1] I. Petrakis: Proof-relevance in Bishop-style constructive mathematics, submitted, 2021.

[2] M. Shulman: Affine logic for constructive mathematics, arXiv:1805.07518v2, 2021 - Peter Schuster, Maximale Ideale in abzählbaren Ringen - konstruktiv, 26. Januar 2022
- Jan Belle, A Variation of the Theory of Computable Functionals,
8. Dezember 2021

Abstract: Based on an article by T. Hagino on a typed lambda calculus with categorical type constructors, we consider a variation of the theory of computable functionals, the underlying theory of the proof assistant Minlog. In particular, we distinguish at the type level between algebras with constructors and recursion and coalgebras with destructors and corecursion. Further, we introduce some new notation for coinductive predicates to match the notation for these coalgebras. Finally, using this additional information in the type system, we prove within this theory the totality of the terms in the calculus. - Anne Michaelis, Categorical aspects of complemented subsets.
1. Dezember 2021

Abstract: Regarding the fundamental differences between set and category theory, the translation of ideas and concepts from Bishop set theory into category theory is an especially interesting topic. In this talk we focus on the translation of set-theoretic terms, within Bishop-style constructive mathematics, to categorical notions. After a short presentation of Bishop set theory we turn to the categorical aspects of complemented subsets and present the category of complemented subsets. Bishop's definition of a subset of a set is related to the notion of a subobject in category theory. In order to translate the notion of a subset and complemented subset to the language of categories, we need to capture equality and apartness categorically. Following Klein we first present the definition of a binary relation and then define the categorical notion of an equality and apartness relation. We then give the definition of a complemented subobject of an object with respect to a given pair of equality and apartness. This allows us to define the category of complemented subobjects, which can be seen as the categorical translation of the category of complemented subsets. At last we give a brief outlook on which further research still needs to be done. - Luis Gambarte, Chu categories. 3. November 2021

Abstract: Chu categories were first introduced to generate *-autonomous categories from closed symmetric monoidal categories. A special case of the Chu construction, so called Chu spaces were used later on in other areas of mathematics, e.g game theory or quantum logic. In this talk we present an overview of the theory of Chu categories, as well as a few examples in which the Chu construction actually relates to topics that are not related at first sight. Furthermore we examine the relation of the Chu construction to other categorical notions, especially whether the existence of certain objects, like for example products, in the base category implies the existence of such objects in the Chu category. Another important tool in category theory are so-called Grothendieck constructions, which have already been examined in relation to Chu categories. We strengthen this relationship by giving a Grothendieck construction that can be associated to any Chu category and is in fact equivalent. At last we present a few generalizations of Chu categories, e.g. the generalized Chu category which has its origin in the examination of the category of predicates.

## SS 2021

Abstract: If C is a closed symmetric monoidal category (CSMC) and γ is an object of C, the Chu category Chu(C, γ) over C and γ was defined by Chu in [1], as a *-autonomous category generated from C. In [2] Bishop introduced the (thin) category of complemented subsets of a set X, in order to overcome the problems generated by the use of negation in constructive measure theory. In [3] Shulman remarked that Bishop's complemented subsets correspond roughly to the Chu construction. In this talk we explain this correspondence by showing that there is a Chu representation (a full embedding) of the category of complemented subsets of a set X into Chu(Set, X x X). A Chu representation of the category of Bishop spaces into Chu(Set, Real) is shown, as the constructive analogue to the standard Chu representation of the category of topological spaces into Chu(Set, 2). In order to represent the category of predicates (with objects pairs (X, A), where A is a subset of X) and the category of complemented predicates (with objects pairs (X, A), where A is a complemented subset of X) we generalise the Chu construction by defining the Chu category over a CSMC C and an endofunctor Γ : C -> C. [1] M. Barr: *-Autonomous Categories, LNM 752, Springer-Verlag, 1979. [2] E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967. [3] M. Shulman: Linear Logic for Constructive Mathematics, arXiv:1805.07518v1, 2018.

Aus bekanntem Anlass findet der Vortrag via zoom statt. Zoom-Meeting beitreten:

https://lmu-munich.zoom.us/j/97956769629?pwd=MXB5d01kaXNkRS9ibUlIamNyUHRaUT09

Meeting-ID: 979 5676 9629

Kenncode: 975943

Zusammenfassung: Nach einer kurzen Einführung in die LT(;)-Theorie und das ParseDag-Modell als Berechnungsmodell betrachten wir drei Sortieralgorithmen, die alle sogenannte divide-and-conquer-Algorithmen sind. Diese Algorithmen enthalten je einen nicht-linearen Term. In der LT(;)-Theorie können wir das RS-Eliminationslemma beweisen, das besagt, dass sich alle LT(;)-Terme (die nach Definition linear sind) in polynomieller Zeit bzgl. einer Grössenfunktion des ParseDag-Modells normalisieren lassen. Im Zuge der Arbeit erweitern wir diese Aussage um die nicht-linearen Terme der Sortieralgorithmen, indem wir zeigen, dass sie im ParseDag-Modell in linearer Zeit berechnet werden können. Im Rahmen des Vortrages werden wir uns dafür speziell einen der drei Sortieralgorithmen anschauen: den QuickSort. Als Ausblick gibt es am Ende eine Verallgemeinerung der vorherigen Ergebnisse.

Aus bekanntem Anlass findet der Vortrag via zoom statt. Zoom-Meeting beitreten

https://lmu-munich.zoom.us/j/94383369551?pwd=cTZmUm9ZYkJIcXpYdnZ6TDdIVXdzdz09

Meeting-ID: 943 8336 9551

Kenncode: 748297

## Frühere Vorträge im WS 2020/21

- Helmut Schwichtenberg, Proof and computation with infinite data.
(j.w.w. Franziskus Wiesnet). 4. November 2020

Abstract: Continuing earlier work with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.

Aus bekanntem Anlass findet der Vortrag via zoom statt. Zoom-Meeting beitreten:

https://lmu-munich.zoom.us/j/95237468434?pwd=N1BBOHBKNkNleTdGeFRRRFpTM1JwQT09

Meeting-ID: 952 3746 8434

Kenncode: 021128

## Frühere Vorträge im SS 2020

- Franziskus Wiesnet,
A case study in constructive algebra: Zariski's lemma.
2. September 2020

Abstract: This presentation is useful for everyone who is interested in using constructive proofs to generate algorithms. Zariski's lemma is a well-know statement in algebra and was used by Oskar Zariski to prove Hilbert's Nullstellensatz. But there may be related approaches in many other areas of constructive mathematics and the presentation only requires a basic knowledge of algebra. We discuss proof interpretation in algebra by the example of Zariski's lemma. Our approach is divided in to three steps. As a starting point we formulate a constructive proof of Zariski's lemma. As second step we formulate a computational interpretation of the statement and the used lemmas. Finally, we use the proof of the first step to establish an algorithm which realises the interpretation of the second step. In particular, we highlight on which objects the algorithm operates, which objects are needed for the hole computational interpretation, and how one can obtain this by using the constructive proof. - Makoto Fujiwara, The conservation results on semi-classical arithmetic.
26. August 2020

Abstract: We carry out some generalization of a well-known result that classical arithmetic PA is Pi_2-conservative over intuitionistic arithmetic HA with respect to semi-classical arithmetic. In particular, we show that PA is Pi_{k+2}-conservative over HA + Sigma_k-LEM where Sigma_k-LEM is the low-of-excluded-middle scheme for formulas of Sigma_k form. This is a joint work with Taishi Kurahashi.

## Frühere Vorträge im WS 2019/20

- Makoto Fujiwara, Parallelizations in Weihrauch reducibility and
constructive reverse mathematics. 29. Januar 2020

Abstract: There are several corresponding results between constructive reverse mathematics and computability-theoretic investigations on parallelizations (also called sequential versions in classical reverse mathematics). For example, the weak Koenig's lemma WKL is equivalent to the lesser limited principles of omniscience LLPO in Bishop's constructive mathematics while WKL is Weihrauch reducible to the parallelization of LLPO. In general, it seems to be believed that constructive equivalences of two existence statements in Bishop's constructive mathematics (which accepts the use of a countable choice principle) correspond to Weihrauch equivalences of their parallelizations. In this talk, we verify that this experimental belief is plausible by showing some meta-theorems in the framework of finite-type arithmetic with inspecting some concrete examples including the above mentioned facts. - Martin Ruckert, Tex für's Handy - ein reflow-fähiges Output
Format für Tex. 20. Novenber 2019

Zusammenfassung: Das "normale" Output Format für TeX ist heute das PDF Format. Das PDF Format eignet sich aber wenig für mobile Endgeräte oder allgemein für elektronisches Lesen, wenn die verfügbare Fläche klein ist und dynamisch zwischen Hoch- und Querformat gewechselt wird. Das HINT Projekt definiert ein neues reflow-fähiges Output Format, das den Anforderungen mobiler Endgeräte besser gerecht wird. Der Vortrag berichtet über den Verlauf, die Problemstellung und den gegenwärtigen Stand des HINT Projekts. - Daniel Wessel, Ideal objects in the shades of finite trees.
23. Oktober 2019

Abstract. A form of Krull's Lemma asserts that a multiplicative subset of a commutative ring R contains the zero element precisely if the set in question meets every prime ideal. We attempt a constructive interpretation by relating the Zariski lattice of R to a certain inductively generated class of finite rooted binary trees. The acid test is the well-known theorem that every nonconstant coefficient of an invertible polynomial is nilpotent, for which a new and straightforward elementary argument will be given. We'll then take a step back to throw a rather conceptual glance at the method, and we will zoom in again to carry it over to a possible treatment of maximality. The research presented in this talk is based on joint work with Peter Schuster (University ofi Verona) and Ihsen Yengui (University ofe Sfax).

## Frühere Vorträge im SS 2019

- Paulo Oliva, Unifying Functional Interpretations Revisited. 7. August 2019, 16:30 - 18:00
- Makoto Fujiwara, Weihrauch and constructive reducibility between
existence statements.
7. August 2019, 15:15 - 16:00

Abstract. We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical with the formal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas. In addition, we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics. - Ryota Akiyoshi, On Gaisi Takeuti's philosophy of mathematics.
7. August 2019, 14:30 - 15:15

Abstract. Gaisi Takeuti (1926-2017) is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He furthered the realization of Hilbert's program by formulating Gentzen's sequent calculus for higher-oder logics, conjecturing the cut-elimination theorem holds for it (Takeuti's conjecture in 1953), and obtaining several stunning results in the 1950--60's towards the solution of his conjecture. For example, he proved the consistency of PiOneOne-CA0 (in 1958) and PiOneOne-CA+BI (in 1967) in a modern terminology. For proving the termination of his cut-elimination steps, he introduced a new system of ordinals called "ordinal diagrams" in 1957. Though he has been chiefly known as a great mathematician, he published many papers in English and Japanese in which he expressed his philosophical views about the foundations of mathematics. Moreover, he used several keywords such as "active intuition" and "self-reflection" from Kitaro Nishida's philosophy in Japan. In this talk, we aim to describe a general outline of our project to investigate Takeuti's philosophy of mathematics. In particular, after reviewing Takeuti's proof-theoretic results very briefly, we explain some key elements in Takeuti's texts and point out that there is a crucial difference between Takeuti's program and Hilbert's program. If time is permitting, we explain an influence of Nishida's philosophy on Takeuti's philosophical ideas. This is joint work with Andrew Arana in University of Paris 1 and IHPST (Paris). - Chuangjie Xu, Various structures of T-definable functions via a
Gödel-Gentzen-style translation.

Montag, 5. August 2019, 14:30 - 16:00

Abstract: We introduce a notion of nucleus relative to Gödel's System T to parametrize a monadic translation of T in the spirit of the Gödel-Gentzen negative translation of classical logic: types of T are translated in the same way of the formula translation, and the term translation corresponds to the soundness proof of the negative translation. Working with different nuclei, we can reveal various structures of functions that are definable in T directly via the monadic translation. In the talk, I will present some examples of nuclei and their applications, including those for majorizability, continuity and bar recursion. - Max Zeuner, Families of sets in constructive measure theory.
31. Juli 2019.

Abstract: The presentation of the Bishop-Cheng measure theory in chapter 6 of Bishop and Bridge's '85 book contains a number of impredicative definitions that are quite problematic from a constructive viewpoint. Three problems in particular block a direct formalization of this theory in constructive set theory or in Martin-Löf type theory: (i) The totality of partial functions X -> Y is treated as a set. (ii) The definition of a measure space tacitly uses the powerset of X as a set. (iii) The definition of L_1 is impredicative, as it rests on the use of the powerset of X as a set. In his first book, Bishop was much more cautious to avoid the impredicativities (i) and (ii), by invoking set-indexed families of sets and subsets, which recently have been studied by Petrakis. Building on Petrakis' definition of families of sets and families of subsets of a set, we study the corresponding notions of families of complemented subsets and partial functions. Using these tools we describe how the basic concepts of an integration space and of a measure space, together with central parts of the Bishop-Cheng measure theory can be reformulated, avoiding the aforementioned impredicativities. The talk is based on my Master's thesis supervised by Iosif Petrakis. - Andreas Abel. 17. Juli 2019
- Anton Freund,
On derivatives of normal functions. 19. Juni 2019.

Abstract. I will show that the statement ``every normal function has a derivative" is equivalent to \Pi^1_1-bar induction. More precisely, the equivalence is established in ACA_0, relying on a representation of normal functions in terms of dilators. The talk is based on a joint paper with M. Rathjen (arXiv:1904.04630). - Hajime Ishihara,
Extended frames and separations of logical principles. 26. Juni 2019.

Abstract. Many omniscience principles, which appear in constructive (reverse) mathematics, are obtained by substituting propositional variables in propositional formulae by simply existence formulae. We propose the notion of an extended (Kripke) frame, and give a systematic way of separating those ommniscience principles using extended frames. This is a joint work with Makoto Fujiwara, Takako Nemoto, Nobu-Yuki Suzuki and Keita Yokoyama. - Hans Leiss,
An Algebraic Generalization of the Chomsky-Schützenberger-Theorem.
22. Mai 2019.

The theorem of Chomsky and Schützenberger says that each context-free language L over a finite alphabet X is the image of the intersection of a regular language R over X+Y and the context-free Dyck-language of balanced strings over X+Y under the bracket-erasing homomorphism from the monoid of strings over X+Y to that of strings over X, where Y is a finite set of bracket pairs.

Within Hopkins' algebraization of formal language theory we show that the algebra C(X) of context-free languages over X has an isomorphic image in a suitable tensor product of the algebra R(X) of regular languages over X with a quotient of R(Y) by a congruence describing bracket matches and mismatches. It follows that all context-free languages over X can be defined by regular(!) expressions over X+Y where the letters of X commute with the brackets of Y, thereby providing a substitute for a fixed-point-operator.

This generalizes the theorem by Chomsky and Schützenberger and extends to a characterization of the algebraic or fixed-point closure C(M) of the algebra R(M) of regular subsets of a monoid M by algebraic means, and perhaps to the fixed-point closure of a *-continuous Kleene algebra.

## Frühere Vorträge im WS 2018/19

- Masahiko Sato,
Reflections on the role of the eta-rules in the lambda-calculus.
27. Februar 2019

Abstract. In the traditional lambda-caculus, the eta-rules (eta-reduction rule and eta-expansion rule) are studied as rules of the lambda_beta_eta calculus. Thus, eta_rules are usually introduced after the beta-conversion rule is studied and the Church-Rosser theorem is proved for the lambda_beta calculus. In this talk, however, we will argue that eta-rules, or more precisely, the eta-equivalence relation on the lambda-terms (generated by the eta-rules) should be introuced and studied even before we introduce and study beta-converion rules. This approach is based on our observation that lambda-terms modulo alpaha-equivalence can be seen as extended cobinatory logic terms. We extend this observation and will study lambda-terms modulo alpha-eta-equivalence. - Chuangjie Xu
(joint work with Fredrik Nordvall Forsberg and Nicolai Kraus),
Two type-theoretic approaches to ordinals in Cantor normal form,
20. Februar 2019

Abstract: We construct two data structures to directly represent ordinals in Cantor normal form: (1) decreasing sequences, using induction-recursion, and (2) finite multisets, using higher inductive types. Both have been easily and neatly implemented in the Agda proof assistant. - Yong Cheng, The current state of research on incompleteness.
23. Janar 2019

Abstract. Gödel's incompleteness theorem is the most profound and important theorem in foundations of mathematics. There are still some open problems related to incompleteness. In this talk, firstly I will classify some misinterpretations of Gödel's incompleteness theorem and give an overview of the current state of research on incompleteness from the following aspects: (1) The property of provability and truth; (2) The generalization of Incompleteness theorem to arithmetical definable theory; (3) The classification of proofs of the incompleteness theorem; (4) Proving incompleteness via logical paradox; (5) The intensionality problem of G2; (6) Incompleteness and provability logic. Finally, I will talk about some recent progress on the open problem of finding the limit of incompleteness for subsystems of PA. - Philipp Scheufele,
The Fundamental Theorem of Asset Pricing in constructive mathematics.
21. November 2018

Abstract. We consider different versions of the FTAP in the context of constructive reverse mathematics. In particular we will show that the two standard FTAPs (existence of an arbitrage strategy <-> absence of an equivalent martingale measure, and vice versa) are equivalent to LPO. Moreover, we will develop different modifications of these standard FTAPs and examine their relation to Markov?s Principle and LPO. Finally, we will provide a guide for obtaining constructive formulations of the FTAP from the non-constructive ones and provide some explicit examples. - Kenji Miyamoto, The epsilon calculus with equality and Herbrand
complexity. 14. November 2018

Abstract. Hilbert's epsilon-calculus is an extension of elementary or predicate calculus by a term-forming operator \(\varepsilon\) and initial formulas involving such terms. The fundamental results about the epsilon-calculus are so-called epsilon theorems, which have been proven by means of the epsilon substitution method. It is a procedure of transforming a proof in epsilon-calculus into a proof in elementary or predicate calculus through getting rid of those initial formulas. One remarkable consequence is a proof of Herbrand's theorem by Bernays and Hilbert which comes as a corollary of extended first epsilon theorem. Our contribution is the upper and lower bounds analysis of the length of Herbrand disjunctions in extended first epsilon theorem for epsilon-calculus with equality. It is an extension of the results by Moser and Zach including the complexity analysis in epsilon-calculus without equality, where extended first epsilon theorem was the main target for analysis, since the epsilon substitution method shows its general figure in the proof of this theorem. - Martin Escardo, Ordinals in constructive univalent mathematics.
31. Oktober 2018

Abstract. We consider ordinal codes (certain countably branching trees) and ordinals (types equipped with transitive, extensional, well founded relations) and two interpretations of codes into ordinals. One of them gives discrete ordinals. The other one gives "compact" ordinals (also called "searchable"). These two interpretations are classically equivalent, but constructively very different, and have some interesting relationships. The ordinals in the image of the compact interpretation satisfy the property that every detachable inhabited subset has a least element. For the ordinals in the image of the discrete interpretation this fails (or, more, precisely, is equivalent to LPO).

## Frühere Vorträge im SS 2018

- Peter Schuster (Univ. Verona), Das Zornsche Lemma als bloss heuristisches Prinzip. Dienstag (!), 19. Juni 2018, 12.30 Uhr, B252.
- Ingo Blechschmidt, Without loss of generality, any reduced ring
is a field, 11. April 2018, 15:15-16:45 (!), B349 (Sitzungszimmer) (!)

Abstract. We present a semantics which allows to pretend that any reduced ring is a field, as long as we restrict to constructive reasoning. We illustrate the usefulness of this general technique by giving a constructive proof of Grothendieck's generic freeness lemma. Because the lemma is trivial for fields, the new proof is short and simple; in contrast, all previously known proofs were somewhat convoluted and employed classical logic, such that it came as a surprise that the lemma admits a constructive proof. Some aspects are related to Dickson's lemma, which was analyzed by Berger and Schwichtenberg.

## Frühere Vorträge im WS 2017/18

- Toshiyasu Arai, Proof-theoretic strengths of weak theories
for positive inductive definitions. 21. Februar 2018, 16:30, B349
(Sitzungszimmer)

Abstract. In this paper the lightface \Pi^{1}_{1}-Comprehension axiom is shown to be proof-theoretically strong even over RCA_{0}^{*}, and we calibrate the proof-theoretic ordinals of weak fragments of the theory ID_{1} of positive inductive definitions over natural numbers. Conjunctions of negative and positive formulas in the transfinite induction axiom of ID_{1} are shown to be weak, and disjunctions are strong. Thus we draw a boundary line between predicatively reducible and impredicative fragments of ID_{1}. - Ryota Akiyoshi, "Proofs as Programs" Revisited, and Chuangjie
Xu, An Agda implementation of Oliva & Steila's proof of the Bar
Recursion Closure Theorem. 14. Februar 2018, 16:00, B349
(Sitzungszimmer) (!)

Abstract Xu: Oliva and Steila [2] present a direct proof of Schwichtenberg's theorem that the System T definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels 0 and 1. We implement it in the Agda proof assistant to convert bar recursive definitions to Agda programs under the conditions of Schwichtenberg's theorem. In particular, we make use of Escardo's construction of dialogue monad [1] to simplify our implementation. [1] M. Escardo, Continuity of Godel's system T functionals via effectful forcing. MFPS'2013. Electronic Notes in Theoretical Computer Science 01/2013, volume 298, pages 119-141. 2013. [2] P. Oliva and S. Steila, A direct proof of Schwichtenberg's bar recursion closure theorem. To appear in The Journal of Symbolic Logic, 2017.

Abstract Akiyoshi: Schwichtenberg has developed the program called "Proofs as Programs" by measuring the "complexity as programs" of proofs in an arithmetical system (with recursion). Technically, he used a slow growing hierarchy to "clime down" tree ordinals, which are introduced by Buchholz. This observation is due to Arai and is going back to Girard's "Hierarchy comparison theorem". In this talk, we sketch another approach to this program by focusing on parameter-free subsystems of Girard's F. There are at least two advantages in this approach. (i) Our approach is simpler and smoother than the original one. (ii) It is relatively easy and uniform to extend our results to stronger fragments (corresponding to iterated inductive definitions) though the theory analysed by Schwichtenberg has the strength of Peano Arithmetic. This work is based on discussions with Schwichtenberg. - Nils Köpp, Program extraction from coinductive proofs in Minlog
applied to some constructive analysis, 24. Januar 2018

Abstract: We review the theory underlying the proof assistant Minlog, which allows for automatically verified program extraction from (co)inductive proofs. We will apply these methods to some constructive analysis, especially the representation of constructive cauchy-reals by sd-code. - Philipp Schlicht, Class forcing and reverse mathematics of
second-order set theory. 20. Dezember 2017

Abstract: The forcing theorem, the most fundamental result about set forcing, states that every set forcing admits forcing relations for all formulas and the truth lemma holds: statements true in the corresponding forcing extensions are forced and forced statements are true. Unlike for set forcing, the forcing theorem for class forcing can fail in models of Gödel-Bernays class theory GBC with global choice. We show that the class forcing theorem is equivalent over the base theory GBC to the principle ETR_Ord of class recursion of length Ord; the existence of Ord-length iterated truth predicates relative to any class; the statement that every separative class partial order has a set-complete class Boolean completion; and the principle of determinacy for clopen class games of rank at most Ord+1. This situates the class forcing theorem in an emerging hierarchy of reverse mathematics of second-order set theory. This is joint work with Victoria Gitman, Joel Hamkins, Peter Holy and Kameryn Williams. - Chuangjie Xu, Using function extensionality in Agda,
(non-)computationally. 6. Dezember 2017

Abstract: I implemented my thesis [2] in the Agda proof assistant to compute moduli of uniform continuity. The main difficulty is the lack of function extensionality (i.e., two functions are equal if they are pointwise equal) in Agda. If it is directly postulated, then the implementation fails to compute. We developed a few approaches to use function extensionality in a non-computational way to address this problem. Cubical Type Theory [1] proves function extensionality. Recently it was implemented as a part of the beta version of Agda. We ported our original development to this cubical Agda and the computation correctly produced zero, while it was a 367-lines long normal-form term in the development where functional extensionality was postulated. [1] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical type theory: a constructive interpretation of the univalence axiom (2016). To appear in the proceedings of TYPES 2015. [2] C. Xu, A continuous computational interpretation of type theories, doctoral dissertation, the University of Birmingham, 2015. - Hajime Ishihara, The Hahn-Banach theorem, constructively revisited.
15. November 2017

Abstract: We review known constructive versions, such as the separation theorem and continuous extension theorem, of the Hahn-Banach theorem and their proofs, and consider new versions including the dominated extension theorem and their proofs. - Matthias Eberl, It's a Matter of Dependency, Not of Size.
25. Oktober 2017

Abstract: We develop a finitistic point of view based on an interpretation with reflection principle. The basic idea is that of a potential infinite set, which leads to the replacement of infinite collections by unbounded, indefinitely extensible collections. A universal quantifier referring to such indefinitely large domains ranges over a sufficiently large finite part of it. - Michael Beeson (Joint work with Julien Narboux and Freek Wiedijk),
Proof-checking Euclid. 11. Oktober 2017

Abstract: We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid's gaps and correcting errors. Then we checked those proofs in the well-known and trusted proof checkers HOL Light and Coq. The talk will contain many geometrical diagrams and discuss both the geometry and the proof-checking.

## Frühere Vorträge im SS 2017

- Auke Booij, Analysis in univalent type theory. 20. Sep. 2017

Abstract: It is not possible to exhibit information about real numbers such as Dedekind reals or (quotiented) Cauchy reals (as opposed to Bishop-style Cauchy reals), because, for example, there are no non-constant functions into observable types such as the booleans or the integers. We overcome this by considering real numbers that have additional structure, which we call strong locatedness. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy approximation. Such constructions are reminiscent of computable analysis. However, the main point is that instead of working with a notion of computability, we simply work constructively to extract observational information. - Franziskus Wiesnet, Signed Digit Code of Reals. 23. August 2017

Abstract: This speech is about an insight in the master theses "Constructive Analysis with Exact Reals". This paper deals with three subjects: - An introduction to the theory of computable functionals (TCF) - A tutorial about the handling of the prove assistent Minlog - Real numbers and their signed digit code (SD code) There will be an overview of all three parts but especially we will take a look at the third part. Here the object is, that we get form the SD code of the reals x,y the SD code of (x+y)/2 and under certain conditions the SD code of x/y. Therefore we use the method of program extraction from proves, which is object of the first chapter. In so doing we gain the correctness of our algorithm for free. For an efficient implementation we use the prove assistent Minlog. The prove itself is done by coinduction and thus the extracted term will use corecursion. We will see how efficient it is. - Paulo Oliva, Bar recursion over finite partial functions. 16. August 2017

Abstract: We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional of [4]. The recursion takes place over finite partial functions u, where the control parameter omega, used in Spector's bar recursion to terminate the computation at sequences s satisfying omega(hat{s})<|s|, now acts as a guide for deciding exactly where to make bar recursive updates, terminating the computation whenever omega(hat{u}) in dom(u). We begin by exploring theoretical aspects of this new form of recursion, then in the main part of the paper we show that demand-driven bar recursion can be directly used to give an alternative functional interpretation of classical countable choice. We provide a short case study as an illustration, in which we extract a new bar recursive program from the proof that there is no injection from N -> N to N, and compare this with the program that would be obtained using Spector's original variant. We conclude by formally establishing that our new bar recursor is primitive recursively equivalent to the original Spector bar recursion, and thus defines the same class of functionals when added to Gödel's system T. - Makoto Fujiwara, Weak fragments of double negation shift and related
principles in arithmetic. 9. August 2017

Abstract: We investigate two weak fragments of the double negation shift schema, which are motivated respectively from Spector's consistency proof of ACA_0 and from the negative translation of RCA_0 (both of which are well-known axiom systems in reverse mathematics), as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved. This is a joint work with Ulrich Kohlenbach. - Andreas Franz, Wedge sum and smash product in homotopy type theory.
2. August 2017

Abstract: Martin-Löf's intensional type theory can be extended with higher inductive types (HITs), which generalize ordinary inductive types, since, in addition to point constructors, constructors that output (higher) paths are allowed. We focus on a specific class of HITs, the so-called pushout types, which define important types from the geometric point of view. In order to show that pushouts are invariant under homotopy, and thus feasible in the framework of homotopy type theory, we develop a tool-set to induce the right morphisms between them. We elaborate two fundamental examples of puhsouts types, the wedge sum and the smash product of pointed types. Using our tool-set we show that these two pushouts correspond to the coproduct and tensor product, respectively, in the subcategory of pointed types and base-point preserving functions. - Christoph Mussenbrock, tba. 19. Juli 2017. Fällt aus; verschoben aus das Wintersemester.
- Thomas Powell, Some applications of monads in proof theory. 12. Juli 2017

Abstract. During the last year I ended up thinking a little about monads, as they appear in functional programming. In this talk I would like present two applications of monads in proof theory: The first concerning the complexity analysis of higher-order functionals, and the second a variant of Goedel's functional interpretation with a global state. - Alexander Leitsch, CERES: automated deduction in proof theory.
5. Juli 2017

Abstract. CERES (cut-elimination by resolution) is a method of cut-elimination which strongly differs from cut-elimination a la Gentzen. Instead of reducing a proof p stepwise (and thereby simplifying the cuts) CERES computes a formula CL(p) represented as so-called characteristic clause set. CL(p) encodes the structure of the derivations of cuts in p and is always unsatisfiable. In classical logic any resolution refutation r of CL(p) can be taken as a skeleton of a CERES normal form p* of p (in p* all cuts are atomic); p* can be constructed from r by inserting proof projections in the leaves of r (a proof projections p' of a proof p of F |- G is a cut-free proof of A,F |- G,B where A |- B is an element of CL(p) and p' is constructed from p by skipping inferences going to a cut). CERES was mainly designed as a computational tool for proof analysis and for performing cut-elimination in long and complex proofs (an implementation of the method was successfully applied to Fürstenberg's proof of the infinitude of primes). There is, however, also an interesting theoretical aspect of the CERES method: reductive cut-elimination based on the rules of Gentzen can be shown to be ``redundant'' with respect to CERES in the following sense: if p reduces to p' then CL(p) subsumes CL(p') (subsumption is a principle of redundancy-elimination in automated deduction). This redundancy property can be used to prove that reductive methods (of a specific type) can never outperform CERES. But subsumption also plays a major role in proving the completeness of intuitionistic CERES (CERES-i). If CERES is applied to an intuitionistic proof p of S its CERES normal form p* is typically a classical proof of S which (in general) cannot be transformed into a cut-free intuitionistic proof of S; in particular it turns out that some resolution refutations of CL(p) do not admit constructions of intuitionistic proofs at all. CERES-i solves this problem by introducing the concept of proof resolution, a generalization of clausal resolution to resolution of cut-free proofs. The completeness of CERES-i can then be proven via a subsumption property for cut-free proofs and a subsumption property for proof projections under reductive cut-elimination. The results demonstrate that principles invented in the area of automated deduction can be fruitfully applied to proof theory. - Benedikt Hoeltgen, Explizite Berechnung von gemeinsamen Kontrakta
durch einen neuen Beweis des Satzes von Church Rosser. 7. Juni 2017

Zusammenfassung: Mithilfe des Beweises von Ken-etsu Fujita lässt sich ein "gemeinsames Kontrakum" von zwei beta-gleichen Lambda-Termen berechnen. Dieser Beweis soll auf die alternative Darstellung des Lambda-Kalküls angewendet werden, welche Masahiko Sato in seinem Vortrag vorgestellt hat. - Kenji Miyamoto,
Computational interpretation and complexity analysis in epsilon-calculi.
31. Mai 2017

Abstract: I am going to give a progress report of the research project for computational interpretation and complexity analysis in epsilon-calculi. This is joint work with Georg Moser. One benefit of using epsilon-calculus is that some proofs can be remarkably shorter than the case in first-order predicate logic. An objective of our research is to make use of this advantage in computational interpretation of proofs and applications. Proof complexity is also the main issue as it is a computational metric of analyzing proofs. I firstly talk about existing results in intuitionistic epsilon calculus, and present my observation about what would be possible and what would not be. I secondary talk about a result in complexity analysis in classical epsilon calculus with the equality. - Masahiko Sato,
A common notation system for both lambda calculus and combinatory logic.
24. Mai 2017

Abstract: We present a notation system which can be used to faithfully represent both the terms of lambda calculus and combinatory logic. We show the faithfullness of the representations by observing that the representations respect the beta and eta reduction rules. We also argue that Curry's Last Problem (J.R.Hindley, Curry's Last Problem: Imitating lambda-beta-reduction in Combinatory Logic) in its original form is an ill-posed problem, and can be solved naturally by expressing the problem in our notation system. - Dirk Schlimm, Frege's Begriffsschrift notation: Design principles and trade-offs. 17. Mai 2017
- Anton Freund, A Well-Ordering Principle of Higher Type. 3. Mai 2017

Abstract: A construction which transforms well-orderings into (stronger) well-orderings is called a well-ordering principle. Many set existence axioms of complexity Pi^1_2 have been characterized in terms of well-ordering principles (e.g. arithmetical comprehension, arithmetical transfinite recursion, existence of omega-models of bar induction). I will present a well-ordering principle of higher type, which takes well-ordering principles as input and transforms them into well-orderings. This "higher Bachmann-Howard principle" is equivalent (over Simpson's set theoretic version of ATR_0) to the existence of admissible sets, and thus to Pi^1_1-comprehension (preprint available as arXiv:1704.01662). - Besprechung mit Examenskandidaten, 10. Mai 2017
- Konstantin Schlagbauer, A syntactic approach to extension theorems. 26. April 2017

### Frühere Vorträge im WS 2016/17

- Ryota Akiyoshi, Strong normalization for the parameter-free subsystem
of system F based on the Omega-rule and

Makoto Fujiwara, Constructive reverse mathematics of weak fragments of bar induction,

22. Februar 2017

Abstract Akiyoshi: In this talk, we present a proof of the strong normalization of the parameter-free subsystem of Girard's system F using the Omega-rule due to Buchholz. This is joint work with Kazushige Terui.

Abstract Fujiwara: Bar induction is a principle which is accepted in Brouwer's intuitionistic mathematics. In the context of constructive reverse mathematics, we investigate the interrelation between weak fragments of bar induction and the negative translation of weak countable choice which comes from Goedel-Spector reduction of classical subsystem ACA of second-order arithmetic. - SunYoung Kim, An overview of the state of the art of the formalisation of
linear algebra using Coq, 8. Februar 2017

Abstract: In this talk, we discuss the state of the art of the formalisation of linear algebra related with our recent project. The main goal of the project is to develop a library for Coq which suffices for a semester course in the undergraduate level. - Gyesik Lee, Towards an efficient implementation of real algebraic numbers,
Freitag, 2. Februar 2017, 10:15-11:45, B349 (Sitzungszimmer)

Abstract: This talk gives an introduction to a new project on exact real number arithmetic. We explain first our motivation and intention, then introduce a work we currently study, which is done by Cyril Cohen as a part of the Mathematical Components library for the proof assistant Coq. - AG Normalisierung und Dekoration, 25. Januar 2017
- Hans Leiss, $\mu$-Continuous Chomsky Algebras:
Equational Theory and Closure under Matrix Ring Formation, 11. Januar 2017

Zusammenfassung: In the course of providing an (infinitary) axiomatization of the equational theory of the class of context-free languages, N.Grathwohl, D.Kozen and F.Henglein (2013) have introduced the class of $\mu$-continuous Chomsky algebras. These are idempotent semirings where systems of polynomial inequations (i.e.~context-free grammars) have least solutions -although they are not CPOs- and where multiplication is continuous with respect to the least fixed point operator $\mu$. We review their equational theory and prove that the matrix ring of a $\mu$-continuous Chomsky algebra also is a $\mu$-continuous Chomsky algebra. - Arbeitsgemeinschaft Bern München (ABM), Donnerstag und Freitag, 8. und 9. Dezember 2016. Program
- Wieslaw Kubis, Generic objects and infinite games, 26. October 2016.

Abstract. Let $F$ be a fixed class of `small' mathematical structures (e.g. finite graphs, finite-dimensional normed spaces, etc.) and assume that a notion of `embedding' has been defined so that we can say that one structure is an extension of another. We say that a structure is `big' if it can be build as the union (or, more formally, colimit) of a chain of embeddings in $F$. Fix a big structure $U$. We consider the following infinite game for two players: Player I chooses a structure $S_0$ from $F$. Player II responds by its extension $S_1$, again in $F$. Player I responds by an extension $S_2$ of $S_1$. And so on. We say that Player II wins if the union of the infinite chain of $S_n$'s is isomorphic to $U$, otherwise Player I wins. We say that $U$ is generic, if Player II has a winning strategy. In the talk I will present examples of generic objects in several areas of mathematics. Further, I will show some of their basic properties and relations to the theory of universal homogeneous models. - Imme van den Berg, Nonstandard Analysis, external numbers and the Sorites paradox, Friday 21. October 2016, 10-12 (!), B132 (!)

Abstract. The Sorites paradox says that a heap of sand remains a heap by removing one grain, while adding a grain to a set of individual grains remains a set of individual grains. The paradox can be consistently modeled within nonstandard analysis: the successor of a standard integer is a standard integer, while the predecessor of a nonstandard integer is a nonstandard integer.

More in general, intuitive orders of magnitude of numbers have the Sorites property. Within classical analysis they can be modeled only functionally, by O^{\prime }s and o^{\prime }s, but in nonstandard analysis they can be modeled by external sets, and give rise to the notions of \emph{neutrices} and \emph{external numbers}. A neutrix is a convex additive subgroup of the nonstandard real numbers. Obvious neutrices are \pounds, the external set of limited numbers and \oslash, the external set of infinitesimals, as external sets they are not of the same logical nature. An external number \alpha is the sum \alpha =a+A of a nonstandard real number a and a neutrix A.

The external set E of external numbers has strong algebraic properties; distributivity has to be handled with some care, but it can be completely characterized [1]. Also, E is totally ordered and Dedekind completeness holds if the underlying nonstandard structure is sufficiently saturated for Nelson's reduction algorithm [3], [2] to hold.

Some applications are given in mathematical modeling of vague concepts and error analysis.

Finally we present a first-order axiomatics for the calculus of external numbers. It is formulated in the language \{+,\cdot ,\leq \}, using schemes for the Dedekind property and induction. In a sense the axiomatics gives an approach to the nonstandard reals, which, like in the case of the classical reals, is based on algebraic, analytic and arithmetical axioms.

[1] B. Dinis, I. P. van den Berg, Algebraic properties of external numbers, J. Logic and Analysis 3:9 (2011) 1--30.

[2] F. Koudjeti, I.P. van den Berg, Neutrices, external numbers and external calculus, in: Nonstandard Analysis in Practice, F. and M. Diener (eds.), Springer Universitext (1995) 145-170.

[3] E. Nelson, Internal Set Theory, an axiomatic approach to nonstandard analysis, Bull. Am. Math. Soc., 83:6 (1977) 1165-1198.