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

WS 2018/19

• Kenji Miyamoto, The epsilon calculus with equality and Herbrand complexity. 17. Oktober 2018.
  Will be moved to a later date, because of illness of the speaker.
  
  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, TBA. 31. Oktober 2018
• Quirin Schroll, TBA. 7. November 2018

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

Ab SS 2006.

Letzte Änderung

17. Oktober 2018