Oberseminar Mathematische Logik

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.

Frühere Vorträge

Letzte Änderung