Oberseminar Mathematische Logik

Veranstalter: J. Berger, W. Buchholz, H.-D. Donder, H. Osswald, P. Schuster, H. Schwichtenberg

Zeit und Ort

Mi 16:30-18, B252

WS 2017/18

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.
Michael Beeson, Proof-checking Euclid. 11. Oktober 2017

Frühere Vorträge im SS 2017

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.
Workshop "Logic and its Applications", Wednesday 12. October 2016, Room B349 (!)

09:00-09:45 Sam Sanders, On the interplay between Nonstandard Analysis and computability theory
09:50-10:35 Chuangjie Xu, Extracting computer programs from nonstandard proofs
11:00-11:45 Kenji Miyamoto, Progress report on Minlog's soundness proof generator
11:50-12:35 Iosif Petrakis, Constructive uniformities of pseudometrics

14:30-15:15 Hajime Ishihara, Versions of the weak Koenig lemma and the disjunctive dependent choice
15:20-16:05 Takako Nemoto, Non-deterministic inductive definitions and Fullness
16:30-17:15 Tatsuji Kawai, Localic completion of uniform space
17:20-18:05 Masahiko Sato, Proof theory of the lambda-calculus

Abstracts can be found on the website http://www.mathematik.uni-muenchen.de/~schwicht/la16.php