Oberseminar Mathematische Logik: Frühere Vorträge
Veranstalter: W. Buchholz, H.-D. Donder, H. Osswald, P. Schuster, H. SchwichtenbergSS 2016
- Cameron Freer, Three problems in computable probability theory,
Friday, 8. April 2016, 14-16 (!)
Abstract: We examine the computable content of three key objects in probability theory: the mixing measure in de Finetti's theorem, the Aldous-Hoover-Kallenberg representation of an exchangeable array, and the disintegration map used to form conditional distributions. Joint work with Nathanael Ackerman, Jeremy Avigad, Daniel Roy, and Jason Rute. - Maarten McKubre-Jordens, Material Implications over Minimal Logic,
13. April 2016
Abstract: The ''atrocities'' of material implication have motivated the development of many non-classical logics over the years. In this talk, we outline some of these paradoxes and classify them over minimal logic. We provide some proofs of equivalence and semantic models separating the paradoxes where appropriate. A number of equivalent groups arise, all of which collapse with unrestricted use of double negation elimination. Principles weaker than ex falso quodlibet turn out to be distinguishable, even with a logic so little ''mutilated'' as minimal logic. This can be seen in at least two ways: even minor changes to the logic underpinning mathematical reasoning allow many more distinctions than the classical understanding; and supporting motivation for adopting minimal logic as the ambient logic for mathematical reasoning in the possible presence of inconsistency. - Hans Leiss, On Equality of Contexts and
Completeness of the Indexed Epsilon-Calculus, 20. April 2016
Abstract: G.E.Mints and D.Sarenac (2003) introduced the "indexed epsilon calculus" as a simplification of a higher-order theory of natural language semantics in which contexts are represented by choice functions and the evaluation of an expression in a given context may update the context. The indexed epsilon calculus has epsilon operators epsilon_i indexed by choice functions i, quantifiers over choice functions and an equality predicate for choice functions. Mints and Sarenac proved a completeness theorem with respect to generalized second-order structures where function quantifiers range over a subset of all choice functions for the universe of individuals. We point out a gap in the proof, provide a counterexample, and give a modified completeness proof for the indexed epsilon calculus without equality between choice functions. - Makoto Fujiwara,
Uniform and intuitionistic provability of existence statements, 4. May 2016.
Abstract: Uniform provability of existence statements, which motivates the investigation of sequential versions in reverse mathematics, requires an effective procedure to obtain witnesses from instances of the problem. In [1], we have provided an exact formalization of uniform provability in (finite-type) arithmetic and have shown that for any existence statement of some syntactical form, it is uniformly provable in the base system RCA of reverse mathematics if and only if it is provable in elementary analysis EL, which is the intuitionistic counterpart of RCA. Our formalization of uniform provability in RCA roughly states that there is an effective procedure as required and it is verified in RCA. With the aim of illustrating the relationship between the provability of existence statements in effective (computable) mathematics and that in constructive mathematics, we consider uniform provability verified in further stronger systems and characterize it by (semi-)intuitionistic provability.
[1] M. Fujiwara, Intuitionistic provability versus uniform provability in RCA, Lecture Notes in Computer Science, vol. 9136, pp. 186-195, 2015. - Hannes Diener, Constructive Reverse Mathematics, 18. Mai 2016
- Christoph-Simon Senjak, An Implementation of Deflate in Coq, 8. Juni 2016
- Chuangjie Xu, The inconsistency of a Brouwerian continuity principle
with the Curry-Howard interpretation, 15. Juni 2016
Abstract: If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intuitionistic type theory, with existence in the formulation of continuity expressed as a Sigma-type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N. - Christian Reitwiessner und Christoph Mussenbrock, Formale Verifikation von Smart Contracts, 13. Juli 2016
- Ulrik Buchholtz, Proof theory of homotopy type theory: what we know so far, Friday 15 July. 14-16(!), B251 (!)
- Tatsuji Kawai, Bar inductions and continuity on Baire space,
20. Juli 2016
Abstract: We introduce a uniform continuity principle for Baire space which says that any pointwise continuous function from Baire space to the set of natural numbers is induced by a Brouwer-operation. We show that this principle is equivalent to a version of Bar Induction whose strength is between that of monotone Bar Induction and decidable Bar Induction. Moreover, we characterise monotone Bar Induction and decidable Bar Induction by similar uniformly continuity principles. These characterisations give rise to a new proof of decomposition of principle of Bar Continuity into Continuous Choices and Bar Inductions. - Basil Karadais, Density by compacts, 10. August 2016
Abstract: On an intuitive level, the known Kleene--Kreisel density theorem says that if we're presented with a description of a finite part of a computation, then we can always complete this into a terminating one. In the language of Scott information systems we say: every (formal) neighborhood extends to a total ideal. We reestablish the density theorem for finite types interpreted over nonflat Scott--Ershov domains, by breaking it into two steps: we extend the given neighborhood to a "total neighborhood", which we then close in a simple and canonical way to obtain a total ideal. If time and blackboard space permit, we will also raise issues concerning the relation of "totality" of objects to such notions as "almost maximality", "transitivity" (see oberseminar talk of 28/10/15), and "cototality" of objects.
WS 2015/16
- Hajime Ishihara, A note on the independence of premiss rule,
30. September 2015, 16:30-17:15
Abstract: We prove that certain theories of (many-sorted) intuitionistic predicate logic is closed under the independence of premiss rule (IPR). As corollaries, we show that HA and HA^omega extended by some non-classical axioms and non-constructive axioms are closed under IPR.
Takako Nemoto, Independence of premiss rule and independence of premiss axiom 30. September 2015, 17:15 - 18:00
Abstract: In [1], we considered the systems closed under independence of premiss rule (IPR). In this talk, we consider what kind of systems are closed under IPR but not prove the following independence of premiss axiom. We also give several examples of systems which are not closed under IPR. [1] Hajime Ishihara and Takako Nemoto, A note on the independence of premiss rule, to appear in Mathematical Logic Quarterly - Stanislav Speranski,
On invariants of probability spaces and their theories,
21. Oktober 2015
Abstract: I develop a theory of invariants of probability spaces. This work addresses a range of foundational issues, such as: - Can we get rid of all structurally irrelevant information in the (standard) representation of probability spaces? - Can we formalise a substantial amount of (non-discrete) probability theory in the language of second-order arithmetic? In effect, for every space, its invariant is a countable object which may be viewed as a "structural representation" of that space. Hence the answers to both questions will be affirmative. I shall start by describing one very natural language for reasoning about probability spaces, denoted by QPL. As a matter of fact, QPL extends a variant of the well-known quantifier-free logic of "polynomial weight formulas" (studied by Fagin, Halpern and Megiddo) by adding quantifiers over events. It turns out that two spaces have the same invariant if and only if their QPL-theories coincide. Moreover, using invariants, we can obtain an adequate translation of the satisfiability relation for QPL (between spaces and formulas) into the language of second-order arithmetic. - Basil Karadais, On transitive elements, 28. Oktober 2015
- Thomas Powell,
Learning procedures arising from Goedel's functional interpretation,
4. November 2015
Abstract: Goedel's functional interpretation is a powerful tool that allows us to extract programs from proofs. Typically, these extracted programs are highly complex, as they reflect the underlying logical structure of the proof, and as such their algorithmic behaviour can be quite difficult to appreciate. In this talk I will discuss the semantics of programs extracted from classical proofs via the functional interpretation, demonstrating how these programs perform learning - a concept which, on a deep level, could be said to unite most computational interpretations of classical reasoning. Much of the talk will be quite informal in style, focusing on concrete examples in order to illustrate more general phenomena. - Hajime Ishihara, The binary expansion and intermediate value theorem
in constructive reverse mathematics,
18. November 2015, 16:00 (!) - 17:00 - Parmenides Garcia Cornejo,
A mathematics word problem answering system based in Bobrow's Student,
25. November 2015 - Dirk Pattinson, Program Equivalence is Coinductive,
16. Dezember 2015
Abstract: We describe computational models, notably Turing and register machines, as state transition systems with side effects. Side effects are expressed via an algebraic signature and interpreted over comodels. Based on a complete equational axiomatisation, we give a complete inductive / coinductive calculus of simulation between states: if the simulated state engenders a terminating computation, so does the simulating state, with the same cumulative effect on global state.
SS 2015
- Hannes Diener, Completeness is Overrated (... sometimes),
15. April 2015
Abstract: It is a common theme in constructive analysis that some propositions which are non-constructive can be made constructive by adding the assumption that the underlying space is complete. This is sometimes referred to as the ''lambda technique'', which owes its name to the common pattern of choosing a binary sequence---traditionally labelled lambda---which in turn is used to construct a Cauchy sequence. Since we are working on a complete space this converges to an element of the underlying space which often yields some desired information. In this talk we are going to give some examples (old and new) of the lambda technique in action and show that in most cases a weakening of completeness is actually sufficient. Finally we also show that there is a plethora of examples to which this generalisation applies. - Iosif Petrakis, A constructive function-theoretic notion of compactness,
22. April 2015
Abstract: Bishop's notion of a function space, here called a Bishop space, is a function-theoretic analogue to the classical set-theoretic notion of a topological space. We introduce the concept of a 2-compact Bishop space and we show that a compact metric space endowed with the Bishop topology of the uniformly continuous real-valued functions is a 2-compact Bishop space. In this way 2-compactness is a function-theoretic generalization of the metric compactness. Among other properties of 2-compact Bishop spaces we show the countable Tychonoff compactness theorem for them. All our proofs are within Bishop's informal system of constructive mathematics BISH. - Sam Sanders,
A formalisation of Osswald's local constructivity in Nonstandard Analysis.
29. April 2015
The *local constructivity of Nonstandard Analysis* is the informal observation due to Horst Osswald that the praxis of Nonstandard Analysis is constructive in the sense of Bishop's Constructive Analysis. In this talk, we formalise Osswald's observation inside (fragments of) Nelson's internal set theory. In particular, we present an algorithm which takes as input the proof of a mathematical theorem formulated solely with definitions (of continuity, convergence, etc) from Nonstandard Analysis, and outputs a proof for the constructive/computable version of the theorem. By way of example, inputting into our algorithm a theorem involving nonstandard compactness, we rediscover (depending on the formulation of the latter) either equivalences from Reverse Mathematics, or totally boundedness, the preferred notion of compactness in constructive/computable analysis. - Franziskus Wiesnet,
Higman's lemma: from a classic to a constructive proof, 6. May 2015
Higmans's lemma is frequently applied in nonfinite combinatorics. A very elegant, though nonconstructive proof has been given by Nash-Williams, for whom he employed the idea of a so called minimal bad sequence. Now we shall use his idea to form a constructive proof. As the final proof is very long we will merely sketch it, though a part of it will actually be carried out and demonstrated with the proof assistant Minlog. This will allow us to take a closer look on the computational content and also to apply it to some examples. - Informal meeting, 13. May 2015
- Informal meeting, 10. June 2015
- Hajime Ishihara, Some principles weaker than Markov's principle (joint work with Makoto Fujiwara and Takako Nemoto), 17. June 2015
- Satoshi Tojo, Belief Re-revision And Reliability Change in
Dynamic Epistemic Logic, Tuesday (!) 23. Juni 2015, 16:30-18
Abstract: The relation between belief revision and reliability is an important aspect of agent communication. That is, an agent can change his/her belief when he/she considers that the new information is reliable. In order to capture this connection, we employ several dynamic operators in terms of dynamic epistemic logic. Here, we propose the commitment and permission operators. The commitment operator is employed for agents to acquire a reliable information and to change beliefs, while the permission operator is used to restore the former beliefs. Furthermore, as side-effects of these operators, we introduce the reliability of the information source, and we can change it by the downgrade/upgrade operations, where each agent can downgrade the agents in a specific group to be equally or less reliable than the other agents. Based on these dynamic operators, we analyze an agent's belief re-revision based on a legal case. - Masahiko Sato, The L-calculus. A natural extension of the lambda calculus, 24. June 2015
- Sam Sanders, Non-standard nonstandard analysis and the
computational content of standard mathematics, 1. July 2015
The aim of this talk is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. Recently, a number of nonstandard versions of Goedel's system T have been introduced ([1-3]). In my previous talk, I discussed how the systems from [1] allow for the extraction of computational information from proofs in Nonstandard Analysis. It is a natural question if similar techniques may be used to extracted computational information from proofs not involving Nonstandard Analysis. In this talk, I provide a positive answer to this question using the nonstandard system from [2]. This system validates so-called non-standard uniform boundedness principles which are central to Kohlenbach's approach to proof mining ([4]). [1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for nonstandard arithmetic, Ann. Pure Appl. Logic 163 (2012), no. 12, 1962-1994. [2] Fernando Ferreira and Jaime Gaspar, Nonstandardness and the bounded functional interpretation, Ann. Pure Appl. Logic 166 (2015), no. 6, 701-712. [3] Amar Hadzihasanovic and Benno van den Berg, Nonstandard functional interpretations and models, arXiv (2014). Available on arXiv: http://arxiv.org/abs/1402.0784. [4] Ulrich Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008. - Douglas Bridges, Some favourite theorems of mine, 8. July 2015.
Retirement presents an ideal opportunity for reflection on one's professional life. In this talk I shall look back at a number of my publications in areas of constructive mathematics, including inter alia: approximation theory; real and complex analysis; and operator theory. - Andreas Franz, Proof search in minimal implicational logic, 22. July 2015.
Bridges between Financial and Constructive Mathematics
WS 2014/15
- Matthew Hendtlass, Topological models of IZF, 26. November 2014.
Abstract: Topological models are a special case of Heyting-valued models --- the constructive counterpart to Boolean valued models --- and include both Beth and Kripke models. The beauty of topological models is that logical principles can be translated into topological properties (unfortunately, these tend to be very unnatural) and the construction of interesting models of constructive set theory can be reduced to the construction of interesting topological spaces. In this talk we discuss topological models of intuitionistic ZF set theory. In particular we look at what standard nonconstructive principles can and cannot be separated using topological models. - Hans Leiss, Learning Context-Free Grammars with the Finite
Context Property, 3. Dezember 2014
Abstract: Alexander Clark (2010) has claimed that a certain class of context-free languages is "identifiable in the limit": there is an algorithm which, for any language in the class, produces from an oracle for membership and an enumeration of the language a sequence of hypothesis grammars that gets constant in a grammar for the language. Unfortunately, Clark's algorithm may converge to a grammar that does not define the given language. We review the theoretical background, i.e. the lattice of syntactic concepts, which is based on a Galois-connection between string sets and context sets, and provide a correction of the algorithm that extracts grammars from finite approximations of the lattice. We demonstrate how the algorithm learns a grammar for simple languages like the Dyck language of well-bracketed strings.
SS 2014
- Masahiko Sato, A Name-Free Lambda Calculus. 24. September 2014
- Hideki Tsuiki, Bottomed sequence representations derived from
dynamical systems. 30. Juli 2014
Abstract. One of the natural ways of writing a real-number program is to use infinite sequences of digits like the signed digits representation. However, it is known that such a representation requires much redundancy in order that enough large class of functions are realizable. In this talk, we first explain another approach to real number computation, that is, representing each real number as a 'unique' (or at most three) infinite sequence with at most one bottom [T. 2002]. Here, a bottom means a cell whose evaluation does not terminate, and one can embed the unit interval in the space of infinite sequences of {0,1} with at most one bottom. through what we call the modified Gray expansion. Since we also have a notion of a machine (i.e. programming mechanism) to input/output such bottomed sequences, one can write and execute a program which inputs and outputs real numbers. Then, we discuss how this mechanism can be extended to other topological spaces. One feature of the modified Gray expansion is that this coding has a recursive structure, which would be important for computational purposes. Therefore, we are interested in codings with recursive structures. One can observe that the recursive structure is closely related to the fact that this expansion coincides with the itinerary of the dynamical system of the tent function. Therefore, we introduce the notion of a dynamical system f:X ¥to X on a compact Hausdorff space X such that the itineraries induce a coding of X. We call such a map an exact full-foldging map. The tent function is the only exact full-folding map on the unit interval modulo conjugacy of dynamical systems. Through the study of exact full-folding maps of other spaces, the author observed that we need more conditions on the dynamical system so that the bottomed-sequence coding has a recursive structure. We call this condition the regularity condition. Finally, we study the two-dimensional case and try to characterize regular exact full-folding maps on the unit disk. We study them through complex dynamical systems and show that full-folding maps are semi-conjugate to quadratic rational maps and that regular exact full-folding maps are obtained through this semi-conjugacy from post-critically-finite quadratic rational maps. - Dirk Pattinson. Continuous Functions on Non-Wellfounded Types
(joint work with Neil Ghani and Peter Hancock).
9. Juli 2014
The well-known representation of real numbers as infinite streams of digits is a well-studied instance of the use of coinductive types to represent continuous data types. The fact that also (total) continuous functions may be represented as a coinductive type suggests that this analogy can be carried over to a larger variety of structures and spaces usually found in analysis, with the main benefit of being able to use coinduction both as a definition and a proof principle on representatives. We argue that indeed many types of spaces found in analysis can be represented coinductively by generalising known representation theorems for function spaces from infinite streams to infinite trees, and subsequently to spaces of higher-order functions. The main challenge is to adequately capture the topology on the represented spaces, which leads to an information-theoretic interpretation. - Klaus Mainzer. Computability beyond Turing Computability? Perspectives of Constructive Analysis. 25. Juni 2014.
- Douglas Bridges. Operators, singly, in bunches, and
constructively. 4. Juni 2014
Abstract. I shall discuss a variety of results and conjectures in the constructive theory of operators and operator spaces. In particular, I shall consider how to locate the range of an operator between Banach spaces, how to locate the closure of Rx when R is a subspace of the space B(H) of bounded operators on a Hilbert space H and x in H, and how to characterise weak-operator continuous linear functionals on linear subsets of B(H). If time permits, I may also talk about relatively recent work with Ishihara and McKubre-Jordens, on reflexivity in Banach spaces. - Maarten McKubre-Jordens. Analysis of Three Different Flavours.
A story of examples, counterexamples, and viewpoints. 28. Mai 2014.
Abstract. In this talk, which surveys at least two viewpoints both about and within mathematics, work is presented in three areas: (i) Constructive partial differential equations (''applied'' constructive mathematics); (ii) Reverse constructive mathematics; (iii) Paraconsistent mathematics. A (very) brief introduction to Bishop-style constructive mathematics will be given. In the first topic, we provide sufficient conditions for *constructive* existence of solutions to Dirichlet-type problems, and outline where the classical existence proofs fail to be constructive. A corollary will be that there cannot be a universal algorithm that computes solutions to the Navier-Stokes equations of fluid flow. In the second topic, we show a direct proof of a known result: that compactness properties (of a certain kind) follow from a non-constructive omniscience principle. The direct proof highlights the decision procedure that has to be made for those compactness properties. The third topic ventures into the little-known realm of mathematics where contradictions may be allowed (yet sensible conclusions can still be drawn)---and surprisingly find that proofs can be very *constructive* in that setting. As a hint at the riches that may be established paraconsistently, we take a look at compactness of closed bounded intervals in the real line. - Iosif Petrakis. On Bishop's function spaces. 21. Mai 2014.
Abstract. The theory of Bishop's function spaces is the least developed approach to constructive topology. Bishop introduced function spaces in [1], he and Bridges added some comments on them in [2], while much later in [3] Bridges revived the subject. Directly after that in [4] Ishihara studied the categories of function spaces and of neighborhood spaces. We try to show that the theory of Bishop's function spaces is an appropriate framework to study constructively parts of the classical theory of the rings of continuous functions.
[1] E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967.
[2] E. Bishop and D. Bridges: Constructive Analysis, Springer-Verlag, 1985.
[3] D. Bridges: Reflections on function spaces, Annals of Pure and Applied Logic 163, 2012, 101-110.
[4] H. Ishihara: Relating Bishop's function spaces to neighborhood spaces, Annals of Pure and Applied Logic 164, 2013, 482-490. - Peter Schuster.
Über die Metamathematik kommutativer Ringe (d'apres Scarpellini).
14. Mai 2014
Zusammenfassung: Eine auf Krull zurüueckgehende Variante des Zornschen Lemmas besagt, dasz ein Element eines kommutativen Ringes dann (und nur dann) nilpotent ist, wenn es in allen Primidealen liegt. Durch Interpolation einer von Scarpellini angegeben algebraischen Charakterisierung der Beweisbarkeit in kommutativen Ringen und Integritätsringen können wir nun ein rein syntaktisches Gegenstück zeigen: Die Theorie der Integritätsringe ist bezüglich Horn-Klauseln eine konservative Erweiterung der Theorie der reduzierten Ringe, d.h. beide Theorien beweisen dieselben Horn-Klauseln.
WS 2013/14
- Luca Chiarabini, 29. Januar 2014
Thema noch offen - Josef Berger, 5. Februar 2014
On the fundamental theorem of asset pricing - Am Donnerstag dem 2. Januar 2014 findet eine Blockveranstaltung des Oberseminars Mathematische Logik statt.
- Masahiko Sato, 30. Oktober 2013
Essence of Normalization by Evaluation
SS 2013
- Davide Rinaldi, Sondertermin am Donnerstag, dem 19. September 2013, 14:30
Basic Pairs, Information Systems and Compact Density - Steve Awodey, 17. Juli 2013
Advances in Univalent Foundations
Abstract: I will show how to compute some homotopy groups of spheres in homotopy type theory, including pi_3(S^2). These new logical proofs of classical theorems from algebraic topology make essential use of higher inductive types and the Univalence Axiom. - Sam Sanders, 12. Juni 2013
Nonstandard Analysis, Higher-order Reverse Mathematics, and Local constructivity
Abstract: Local constructivity (due to Horst Osswald, LMU) is an informal property of mathematical proofs. A proof is locally constructive if the core, the essential part, of a proof is constructive, though the whole is not. We show that a large class of proofs in Nonstandard Analysis is locally constructive, and how proofs in this class can be converted into constructive ones. Ulrich Kohlenbach's so-called Higher-order Reverse Mathematics plays an important role. - Andrew Swan, 29. Mai 2013
Non Definability in Intuitionistic Logic
Abstract. For a theory, T, suppose that T \vdash \exists x \phi(x). Then we say \chi(x) defines a witness for \phi(x) if T \vdash \exists ! x \chi(x) and T \vdash \forall x \chi(x) \rightarrow \phi(x). I will show a simple technique using Kripke models for proving that sentences in intuitionistic logic lack definable witnessess, illustrated with an example from intuitionistic ordered fields. I will then outline how the technique can be developed to show that certain sentences in the set theory CZF lack definable witnesses. This includes defining Kripke realizability models, which incorperate realizability into the definition of Kripke models. - Pedro Valencia, 8. Mai 2013
Classical principles in Minimal Logic
Abstract: We explore the implicational relations between some classical principles in a framework for Minimal Logic.
WS 2012/13
- Hajime Ishihara, 13. March 2013.
Classical propositional logic and decidability of variables in intuitionistic propositional logic
Abstract: We consider a problem: what set V of propositional variables suffices for deriving D_V, G |- A intuitionistically whenever G |- A is classically derivable, where D_V is the set of p v ~p for p in V.
Three proofs from modern unprovability theory
Abstract: This will be a moderately technical talk on modern metamathematics. I will start with the quickest and simplest known proof of the Paris-Harrington theorem and a recent extension of this proof to obtain models of Pi^1_1-CA_0 without set-parameters. All proofs here are model-theoretic, in the style of Paris's indicator theory. Then I will present a sketch of the Phase Transition proof for the planar graph minor theorem. This research is in the spirit of Weiermann's phase transition programme. Finally, I will speak of prefixed polynomial equations, the project of obtaining unprovable expressions of this form and the set of methods and tricks used in this research.
Titel: Goodstein Sequences, Fast Growing Functions and Arithmetical Independence Results.
Zusammenfassung: Formalized arithmetical theories, that supply logical foundations for large parts of mathematics, have ordinals associated with them, measuring their consistency strength. Important examples are Peano Arithmetic and (much stronger) Pi-1-1 Comprehension. Furthermore, up to the given ordinal, the so-called Fast Growing Hierarchy of number-theoretic functions serves to measure the theory's computational power. In addition, these functions turn out to be closely connected with certain known theorems of combinatorial mathematics, which then become independence results (true but not provable) for the given theories. In this way, certain mathematical results serve to calibrate the logical strengths of the theories concerned. This talk will give a brief survey of the role of the Fast Growing Hierarchy in this area, beginning with Goodstein Sequences and the independence from PA (first proved by Kirby and Paris in 1982) of Goodstein's result (1944) that they always terminate.
Copatterns -- Programming Infinite Structures by Observations
(joint work with Brigitte Pientka, David Thibodeau, and Anton Setzer).
Inductive datatypes provide mechanisms to define finite data such as finite lists and trees via constructors and allow programmers to analyze and manipulate finite data via pattern matching. In this talk, we develop a dual approach for working with infinite data structures such as streams. Infinite data inhabits coinductive datatypes which denote greatest fixpoints. Unlike finite data which is defined by constructors we define infinite data by observations. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to synthesize infinite data. This leads to a symmetric language design where pattern matching on finite and infinite data can be mixed.
We present a core language for programming with infinite structures by observations together with its operational semantics based on (co)pattern matching and describe coverage of copatterns. Our language naturally supports both call-by-name and call-by-value interpretations and can be seamlessly integrated into existing languages like Haskell and ML. We prove type soundness for our language and sketch how copatterns open new directions for solving problems in the interaction of coinductive and dependent types.
Infinitary propositional theories and set-generated classes
Abstract: We introduce infinitary propositional theories over a set and their models which are subsets of the set, and define a generalized geometric theory as an infinitary propositional theory of a special form. The main result is that the class of models of a generalized geometric theory is set-generated. Here a class X of subsets of a set is set-generated if there exists a subset G of X such that for each element a of X and finitely enumerable subset t of a there exists a subset b in G containing t and contained in a. We show the main result in the constructive Zermelo-Fraenkel set theory (CZF) with an additional axiom, called the set generation axiom which are derivable from the relativized dependent choice and a regular extension axiom, respectively. We give some applications of the main result to algebra, topology and formal topology. This is a joint work with Peter Aczel, Takako Nemoto and Yasushi Sangu.
Polylogarithmic Cuts in Models of Bounded Arithmetic and Implications to Proof Complexity
Abstract: In Proof Complexity, various complete propositional proof systems are investigated with respect to their efficiency. This is a lively field of research and closely related to the P=NP question. There are several approaches to determining what a proof system can efficiently prove and what it cannot. One of these approaches is by Bounded Arithmetic. That is, if a statement is provable in some arithmetic theory with a weak induction axiom, we can infer the efficient provability of a family of related propositional statements in some propositional proof system. In this talk we will investigate polylogarithmic cuts of models of a certain weak bounded arithmetic theory and show that a formalized version of Nepomnjascij's Theorem holds with respect to them. This shows some interesting properties of these cuts and, using a standard algorithm for formula evaluation, also shows that these cuts are models of a bounded arithmetic theory that corresponds to stronger propositional proof systems. The last fact implies a weak simulation result between these proof systems.
SS 2012
- Oliver Deiser, 18. Juli 2012
Fundierung der Mathematik.
Wir stellen eine äquikonsistente Alternative zur Zermelo-Fraenkel Axiomatik ZFC der Mengenlehre vor, die den Wohlordnungsbegriff an die Spitze stellt. Anschliessend vergleichen wir das System mit ZFC und diskutieren weitere Möglichkeiten zur Fundierung der Mathematik im Umfeld des Ansatzes.
- Fredrik Nordvall Forsberg, 11. Juli 2012
Inductive-inductive definitions in Martin-Löf Type Theory
Abstract: Martin-Löf's dependent type theory can be seen both as a foundational framework for constructive mathematics, and as a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will describe one class of such data types, where a type A is formed inductively, simultaneously with a second type B : A -> Type which depend on it. Both types are formed inductively, hence we call such definitions inductive-inductive definitions. Examples of inductive-inductive definitions - e. g. sorted lists, Conway's surreal numbers and the syntax of dependent type theory - will be given, in order to demonstrate the usefulness of the notion. I will then give a finite axiomatization of the theory, and discuss what is known about its proof theoretical strength.
- Konstantinos Panagiotou, 4. Juli 2012
Catching the k-NAESAT Threshold
Abstract: The best current estimates of the thresholds for the existence of solutions in random constraint satisfaction problems ('CSPs') mostly derive from the first and the second moment method. Yet apart from a very few exceptional cases these methods do not quite yield matching upper and lower bounds. According to deep but non-rigorous arguments from statistical mechanics, this discrepancy is due to a change in the geometry of the set of solutions called condensation that occurs shortly before the actual threshold for the existence of solutions. To cope with condensation, physicists have developed a sophisticated but non-rigorous formalism called Survey Propagation, which yields precise conjectures on the threshold values of many random CSPs. In this talk I will discuss a new Survey Propagation inspired method for the random k-NAESAT problem, which is one of the standard benchmark problems in the theory of random CSPs. This new technique allows us to overcome the barrier posed by condensation rigorously, and prove very accurate estimates for the k-NAESAT threshold; in particular, we verify the statistical mechanics conjecture for this problem. This is joint work with Amin Coja-Oghlan.
- Thomas Forster, Universtät Cambridge, 16. Mai 2012
On Quine's axiomatic set theory "New Foundations"
Abstract: There are rumours circulating that Quine's axiomatic set theory "New Foundations" has been proved consistent. If these rumours are correct the set theoretic landscape will have its most radical revamp for more than half a century, and we will all need to re-tool. This talk will provide historical background and glimpse into how the result might be proved.
- Albert Ziegler, 9. Mai 2012
What ordinals are and why that is all you ever need to know
WS 2011/12
- Matthias Eberl, 31. Januar 2012,
A logic of point of views
Abstract. In this logic objects depend in a fundamental way on the subject. The subject is formulated as a "point of view". Each of these point of views defines a collection of observed objects and a couple of methods to operate on these objects. An object is primarily seen as a "fixation" and it can also represent a method or a point of view. By this, a point of view can be of second order and additionally operate on itself. All point of views form a net of different perspectives without any absolute ground. Each comparison of point of views is inside another one which can use reductions, reflections or relativizations to set point of views into relation.
- Masahiko Sato, 24. Januar 2012,
A first-order theory of lambda-terms
- Nikolaos Rigas, 13. Dezember 2011,
Recent results in the analysis of reducibility.
Abstract. Since its introduction by W. Tait, reducibility (or computability) has found numerous applications in the study of reduction in functional systems, especially in proofs of various normalisation and confluence properties. One trend in the analysis of reducibility, pioneered by J. Gallier, aims to make the reducibility content of such proofs explicit, by eliminating the particular property being proved while preserving the general structure of the argument; this process leads to metatheorems stating sufficient conditions for a property to hold for all terms of a given set. It turns out that such conditions are closure conditions, with the corresponding metatheorems being induction principles, useful for proving properties of reduction, but also interesting in their own right.
A recently formulated reducibility proof, originally discovered in the realm of labelled reduction, has given rise to an induction principle which has been found to scale up to infinitary systems, such as \omega-arithmetic and systems with infinitary connectives. This induction principle offers a natural generalisation of strong normalisation to such infinitary systems.
- Douglas Bridges, 15. November 2011,
Recent work in constructive reverse mathematics.
Abstract. The anti-Specker property (for [0;1]),
AS[0;1]: For each sequence z in [0;1] union {2}, if z is eventually bounded away from each point of [0;1], then z_n = 2 eventually,
is known to be equivalent, over Bishop-style constructive mathematics, to Brouwer's fan theorem FTc for c-bars, and has shown promise as an interesting intuitionistic substitute for the classically equivalent sequential compactness property of the interval. Recent joint work by Dent, McKubre-Jordens and me has connected the weakest variant of AS[0;1] with, on the one hand, the omniscience principle WLPO, and, on the other, a weak form of FTc. This work has led us to new analyses of the connections between antitheses of fan theorems, the existence of Specker sequences in [0;1], and the existence of uniformly continu- ous, positive-valued functions on [0;1] that have infimum 0 (a phenomenon that arises in recursive constructive analysis).
- Parmenides Garcia Cornejo, 25. Oktober 2011,
Investigations on the structural properties of Carlson's <_1- relation.
- Erwin Engeler, 18. Oktober 2011,
Combinatory algebra and neural computing.
SS 2011
- Christoph Senjak, 13. Juli 2011,
Minimal logic with stable relations.
- Hajime Ishihara, Jaist, 22. Juni 2011.
Supergeometric theories and set-generated classes.
Abstract: We introduce supergeometric theories over a set S and their models which are subsets of S. Then we show that the class M(T) of models of a supergeometric theory T is set-generated in CZF, that is, there exists a subset G of M(T) such that each set a in M(T) is the union of sets in G which are subsets of a. We also present some applications to algebra and formal topology.
-
Workshop "Computations, Logic, Algebra, and Categories (CLAC)", 25. Mai 2011,
16-18 (B251) and 18-20 (B045)
Speakers: Peter Aczel, Henri Lombardi, Steve Awodey, Hervé Perdry
- Gunther Schmidt, UniBW München, 4. Mai 2011.
Relationale Mathematik
Zusammenfassung: Verschiedenste Ingenieurwissenschaften haben enorm gewonnen als man lernte, Probleme zu Gleichungsauflösungen und Eigenwertaufgaben herunterzubrechen und rechnerisch zu lösen. Für die Informationswissenschaften sollte analog versucht werden, mit Relationen zu rechnen.
WS 2010/2011
- Iosif Petrakis, München, 2. Februar 2011.
The construction of concepts: from Euclid's geometric concepts to Brouwer's species
Zusammenfassung: Section 1: A reconstruction of Euclid's parallel construction is given, which attributes to the Fifth Postulate a genuine constructive role, contrary to its standard uniqueness interpretation. In that way it is shown why, within Euclid's geometric constructivism G, construction K(P) of a geometric concept P is an enterprise larger than proving (ex a)P(a). Bolyai's construction of a limiting parallel is also shown why it is problematic from the point of view of G.
Section 2: An account is given of Brouwer's conception of mathematical properties or species. In Brouwer's intuitionistic analysis, BIA, we also find, as in G, the need to construct all necessary concepts under some construction principles. A reconstruction of such a list of principles is proposed. We also discuss Brouwer's development of the concept of intuitionistic function and his proof of Fan theorem with respect to these principles. Results of Kleene, Veldman and Martino-Giaretta are included.
- Hannes Leitgeb, München, 12. Januar 2011.
The Logic of Belief: Qualitative and Quantitative.
- Vasco Brattka, Kapstadt, 22. Dezember 2010.
Zur Komplexität der Auswahl in der Berechenbaren Analysis
Zusammenfassung: In der Berechenbaren Analysis kann man mit Auswahlprinzipien verschiedene natürliche Klassen von nicht berechenbaren Funktionen beschreiben. Wir verwenden dazu einen Verband, der von der Weihrauch-Reduzierbarkeit induziert wird. Diese Reduzierbarkeit ist für mehrwertige Funktionen definiert und anschaulich gesprochen ist eine Funktion f dabei reduzierbar auf eine Funktion g, wenn es eine berechenbare Transformation gibt, die jede Implementierung von g in eine Implementierung von f überführt. In diesem Verband betrachten wir Auswahlprinzipien zu verschiedenen Räumen X. Das Auswahlprinzip zu einem Raum X ist im wesentlichen eine Operation, die als Eingabe eine negative Beschreibung einer abgeschlossenen Menge A von X erwartet und als Ausgabe einen Punkt in A liefert. D.h. grob gesprochen, dass eine Beschreibung der unzulässigen Lösungen in eine Lösung konvertiert wird. Bestimmte Auswahlprinzipien spielen dabei eine ausgezeichnete Rolle. Zum Beispiel repräsentieren die Auswahlprinzipien zur leeren und einpunktigen Menge bestimmte Grade 0 und 1 im Verband, wobei 0 der kleinste Grad ist und 1 vollständig für alle berechenbaren Funktionen ist. Das Auswahlprinzip zum zweipunktigen Raum stellt sich als äquivalent zum Lesser Limited Principle of Omniscience (LLPO) heraus, wie es in der konstruktiven Analysis betrachtet wird. Das Auswahlprinzip zu den natürlichen Zahlen ist vollständig für die Klasse derjenigen Funktionen, die mit endliche vielen Meinungsänderungen berechenbar sind, eine Klasse die z.B. in der algorithmischen Lerntheorie untersucht wird. Gleichzeitig charakterisiert das Auswahlprinzip der natürlichen Zahlen auch die berechenbarkeitstheoretische Komplexität vieler Sätze aus der Funktionalanalysis, wie etwa des Baireschen Kategoriensatzes, des Banachschen Satzes von der Inversen, des Satzes vom abgeschlossenen Graphen usw. Analog ist das Auswahlprinzip vom Cantorraum äquivalent zum schwachen Lemma von König (WKL) und zum Hahn-Banach Satz. Gleichzeitig ist dieses Auswahlprinzip auch vollständig für die Klasse der schwach berechenbaren Funktionen, welches genau jene Funktionen sind, die auf einer nichtdeterministischen Turingmaschine berechenbar sind, die eine Null-Eins-Folge raten kann. Das Auswahlprinzip im Baire-Raum charakterisiert analog die Klasse der effektiv Borel-messbaren Funktionen. Falls die Zeit ausreicht, besprechen wir noch verschiedene Abschlussoperationen im Weihrauch-Verband und eine Sprungoperation, die wir auch Ableitung nennen. Diese Operation hat ähnliche Eigenschaften im (starken) Weihrauch-Verband, wie die Turing-Sprungoperation im Turing-Halbverband. Es stellt sich heraus, dass die Ableitung des Auswahlprinzips eine Raumes X genau das Häufungspunktproblem (für Folgen) dieses Raumes ist. Unter anderem folgt, dass die Ableitung des schwachen Lemmas von König genau dieselbe Berechnungskraft hat, wie der Satz von Bolzano-Weierstrass.
Prof. Brattkas Vortrag ist Teil eines von DFG und NRF finanzierten Kooperationsprojektes (Von der Stetigkeit zur Berechenbarkeit).
- Thilo Weghorn, Muenchen, 8. Dezember 2010.
Monaden in der Logik
- Dirk Pattinson, Donnerstag 18. November 2010, 16:15,
RaumB047.
Semantics and Proof Theory of Conditional Logics
Abstract: Conditional Logics are extensions of propositional logic with an additional binary connective. Depending on the context and the particular application, this connective can be read as default implication, counterfactual conditional or relevant implication. We only outline these various flavours briefly and then discuss the semantics and proof theory of various systems of conditional logics. The discussion of the semantics of conditional logics is grounded on the observation that all systems discussed in the literature arise by extending a basic system with so-called `shallow axioms' and we present a generic completeness result for a Hilbert-style system. On the proof theoretic side, we show how to design equivalent (unlabelled) sequent systems and derive previously unknown complexity bounds for various systems studied in the literature.
SS 2010
- Hannes Diener, 10/11. August 2010.
- Matt Hendtlass, 21. Juli 2010.
The intermediate value theorem: when you don't have (a) choice.
- Christof Senjak, 14. Juli 2010.
Induktive Definitionen in Minlog.
- Simon Huber, 23. Juni 2010.
On the computational content of choice axioms
- Henri Lombardi, 16. Juni 2010.
Constructive semantics for nonconstructive principles.
Abstract: Deciphering a computational content for idealistic objects and nonconstructive principles in classical mathematics can be understood as the search for constructive semantics hidden in abstract tricks. We will try to compare through examples two such possible semantics.
- Parmenides Garcia Cornejo, 12. Mai 2010.
k-closed unbounded classes and Carlsons <_1 relation
WS 2009/2010
- Stan Wainer, 24. Februar 2010.
The independence from $\Pi^1_1-CA_0$ of Friedman's miniaturised Kruskal theorem for labelled trees
-
Miriam Kertai (1) und Veronika Köberlein (2), 13. Januar 2010.
(1) Über Beweise des formalen Hilbertschen Nullstellensatzes und (2) Über den konstruktiven Beweis des Satzes von Eisenbud-Evans-Storch
(1) Der formale Hilbertsche Nullstellensatz stellt die Verbindung zwischen einem kommutativen Ring A und der von Joyal angegebenen punktfreien Darstellung seines Zariski-Spektrums als distributiven Verband L(A) dar. Aus ihm folgt, dass L(A) zum Verband der endlich erzeugten Radikalideale isomorph ist. Ein konstruktiver Beweis nutzt die universelle Eigenschaft von L(A) aus. Diesen Beweis wollen wir kurz vorstellen.
(2) Ein Satz, den Eisenbud, Evans und Storch 1973/74 bewiesen, sagt aus, dass sich jede algebraische Menge im n-dimensionalen, affinen Raum als Schnitt von n Hyperflächen darstellen lässt. Der konstruktive Beweis dieses Satzes verwendet die Aussage, dass jeder von Neumann-reguläre, kommutative Ring bereits Bezout Ring ist. Diese Aussage soll hier mit Hilfe eines konstruktiven Lokal-Global-Prinzips bewiesen werden.
- Peter Schuster, 4. November 2009.
Lösungen von Gleichungen mit Eindeutigkeitsvoraussetzungen.
- Dieter Probst, 28. Oktober 2009.
A "simple" proof that $\Sigma^1_1-DC_0$ is conservative over $\Pi^1_0-CA_{\omega^\omega}$ for $\Pi^1_2$ sentences.
I show how a variant of Schütte's Boundedness Lemma leads to a simple proof of the statement in the title.
- Trifon Trifonov, 21. Oktober 2009.
Efficiency refinements in the Dialectica interpretation.
In this talk we will present examples in which Gödel's Dialectica interpretation can be improved to extract more efficient programs. We will discuss the relation of such inefficiencies with modified realisability and the use of classical logic. Variants of the interpretation will be defined in which some of the presented problems can be generally avoided.
- Peter Koepke, Freitag, 16. Oktober 2009, 16:15 (Sondertermin)
Understanding Natural Language Mathematical Proofs.
Usual mathematical proofs are semiformal: they may contain strictly formal derivations in some calculus, but more often they consist of informal natural language argumentations and explanations. The Naproche project (Natural Language Proof Checking) proposes to understand proofs using methods of formal and computational linguistics. The language of mathematics is viewed as an extension of natural language by mathematical terms and formulas. Proof texts possess a formal first-order semantics that may be related to an underlying fully formal proof. Some of these ideas are being implemented in the Naproche system: the system accepts texts written in a mathematical controlled natural language; it analyses and transforms them into first-order presentations. The presentations can be checked for logical correctness by automatic proof checkers and theorem provers. Combining strong tools from computational linguistics, proof checking and also mathematical typesetting, some nontrivial mathematical texts have been reformulated in the Naproche language so that they are simultaneously understandable to human readers and the computer system. In my talk I shall present details of the Naproche system and example texts and discuss some facets of the central question "What is a mathematical proof?".
- Stefan Hetzl, 30. September 2009.
On the form of witness terms.
This talk is about the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The main result is a characterization of the form of witness terms in cut-free proofs by a regular tree grammar that is read off from, and has the size of the original proof. From the theoretical point of view this provides an upper bound on the set of Herbrand-disjunctions reachable from a fixed proof with cuts and from the algorithmic point of view, we obtain a method for computing witness terms that circumvents cut-elimination.
- Kenji Miyamoto, 16. September 2009, 11-13, B251.
A calculus for secure information flow and its logical aspects
WS 2008/2009
- Vivek Nigam, 25. Februar 2009.
Focusing in linear meta-logic.
It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof systems. Here, we show that if we adopt different {\em focusing} annotations for such linear logic specifications, a range of other proof systems can also be specified. In particular, we show that natural deduction (normal and non-normal), sequent proofs (with and without cut), tableaux, and proof systems using general elimination and general introduction rules can all be derived from essentially the same linear logic specification by altering focusing annotations. By using elementary linear logic equivalences and the completeness of focused proofs, we are able to derive new and modular proofs of the soundness and completeness of these various proofs systems for intuitionistic and classical logics. More details in a joint paper with Dale that appeared at IJCAR 08.
- Florian Ranzi, 19. November 2008. Recursion and PCF-definability over
the partial continuous functionals.
- Henri Lombardi, 29. Oktober 2008. Grothendieck schemes,
a constructive view (joint work with Thierry Coquand and Peter Schuster)
Abstract: We explain how to understand most of Grothendieck schemes in finite terms.
- Daniel Bembe, 22. Oktober 2008. Constructive real algebra
Abstract: I would like to introduce the constructures of the real closure of an ordered field by Hollkott resp. Lombardi / Roy and explain how the order enables to calculate in algebraic extensions of a given field without irreducible polynomials. Besides I will speak about algeraic certificates which are (in)equalities that express some assertion. One example is Stengle's Positivstellensatz which is difficult to approach constructively. An other one is a new existence proof of a certificate for Budan's theorem which could be a first step to a different construction of the real closure.
- Josef Berger, 15. Oktober 2008. Classifying varieties of the weak
König lemma.
Abstract: The weak König lemma (WKL) says that every infinite binary tree has an infinite path. Commonly, the tree predicate is a quantifier-free formula. We consider the following generalisations of this axiom: - the WKL for Sigma-0-n trees, - the WKL for Pi-0-n trees, - the WKL for arithmetical trees. On the base of intuitionistic logic, we compare these versions of WKL in view of their logical strength and their strength as choice axioms.
SS 2008
- Russell O'Connor, 16. Juli 2008, Sondertermin 10-12.
Implementation and Applications of Complete Metric Spaces.
This talk will give an overview of my work on implementing complete metric spaces in the Coq proof assistant. Completing the rationals creates the real numbers, which can used in transcendental computations. Completing the step functions creates integrable functions, which can be integrated. Completing the finite sets creates the compact sets, which can be rendered on screen. All these operations have been formally verified by Coq.
- Hajime Ishihara, 9. Juli 2008.
A completion of a uniform space in constructive set theory.
There are several (classically equivalent) definitions of a uniform space, for example, a set with a family of entourages and a set with a family of pseudometrics. We define, in constructive set theory (CZF), a uniform space as a set with a base of uniformity, and a complete uniform space as a uniform space on which every Cauchy filter converges. Then we show that we can construct a completion of a $T_1$ uniform space as a set in CZF.
- Alexey Ostrovskiy, 2. Juli 2008.
Das Problem von Hausdorff.
Hausdorff bewies das folgende Theorem: Sei f: X -> Y, eine offene stetige Abbildung und X vollständig metrisierbarer Raum, dann ist Y auch vollständig metrisierbar und stellte die Frage der Verallgemeinerung dieses Theorems. Er bewies darüber hinaus, dass jeder separabel und vollständig metrisierbare Raum X das Bild der Menge von irrationalen Zahlen P ist, bei einer offenen stetigen Abbildung f. Deswegen können wir alles in P betrachten. Im Rahmen des Vortrags wird ein Überblick über die Entwicklung der Frage von Hausdorff in drei Richtungen gegeben: 1) Die Verbindung zu anderen Klassen der stetigen Abbildungen, z.B. zur Theorie der mehrdeutigen stetigen Abbildungen; 2) Die Verbindung zu anderen Klassen von Borelschen Mengen; 3) Die Verbindung zu der folgenden Eigenschaft (FII) von Hausdorff: (FII) Jede geschlossene Teilmenge in X ist in sich selbst von 2. Baire-Kategorie. Das Ziel des Vortrags ist eine neue Verallgemeinerung des Theorems von Hausdorff. Definition. Eine stetige Abbildung f: X -\-> Y ist eine halboffene Abbildung, wenn das Bild f(U) von jeder geschlossenen und gleichzeitig offenen Menge U, eine Vereinigung von zwei Mengen ist, wobei eine davon offen und die andere geschlossen ist. Theorem 1. Sei f eine halboffene Abbildung, dann: a) ist X (FII)- Raum --\-> Y ist (FII)- Raum; b) ist X vollständig metrisierbar Raum --\-> Y ist vollständig metrisierbarer Raum.
- Bernhard Irrgang, 25. Juni 2008.
Höherdimensionales Forcing.
- Bahareh Afshari, 25. Juni 2008, Sondertermin: 14:15 - 15:45, B040.
An ordinal analysis of iterated positive inductive definitions.
Abstract: In 1963, G. Kreisel initiated the study of formal theories featuring inductive definitions. Subsystems of the theories of iterated inductive definitions (ID_n) such as the fixed point theories I^D_n were investigated by Aczel and Feferman in connection with Hancock's conjecture about the strength of Martin-Löf type theories with universes. Another interesting type of theory lying between I^D_n and the usual ID_n is ID*_n. To illustrate this in the case n = 1, in contrast to I^D_1, ID*_1 has an induction principle for the fixed points but it is restricted to formulas in which other fixed points occur only positively. Results about the theories ID*_n were obtained by Friedman, Feferman, and Cantini. However, they did not settle the proof-theoretic strength of the theories ID*_n . I would like to talk about our recent results revealing the strength of these theories.
- Martin Ochoa, 18. Juni 2008.
Code-based cryptographic proofs.
A "proof" in cryptography is often a reduction of a security definition to some computationally hard problem. The security definition consists of a game (which can be thought as a probabilistic imperative program) between an unknown polynomial-time adversary and a challenger. The reduction is usually done by constructing a probabilistic program that uses the output of the adversary to solve the computationally hard problem, and it is called a "simulation". We present an informal method to organize a simulation-based proof as a sequence of game transformations. We apply this technique to prove the security of the Identity Based Encryption (IBE) scheme of Boneh and Boyen and to show its similarities with the IBE scheme of Waters. A relational probabilistic Hoare-like logic to perform code-based transformations in a rigorous way is introduced.
- Anthony Morphett, 11. Juni 2008.
Randomness, oracles and effective measure.
We work in the Cantor space of infinite binary strings. In this talk, we will describe Martin-Löf's definition of randomness, in terms of effective nullsets as presented by decreasing sequences of c.e. sets. We will also describe an equivalent characterisation of Martin-Löf randomness in terms of Kolmogorov complexity. By working with oracle Turing machines, the definition of Martin-Löf randomness can be relativised; one can then study the information content of an oracle by examining the relative randomness notion that it yields. We describe one such approach, the LR-reducibility ('Low-for-random reducibility'). We discuss some recent results regarding LR-reducibility, with particular emphasis on some similarities and differences between LR- and Turing reducibilities.
- Sebastian Bauer, 21. Mai 2008.
Predicative Extensions of First-Order Logic.
Starting from first-order minimal logic in all finite types, we introduce a second-order extension in which in addition to predicate quantifiers also universal type quantifiers are allowed. In order to remain predicative, comprehension is restricted to arithmetical formulas, which means that predicate quantifiers only range over formulas of the first-order part. In this sense, first-order intuitionistic arithmetic (Heyting arithmetic) can be extended to restricted second-order intuitionistic arithmetic. For these systems our main result is that they are conservative over their first-order part. Proofs can be normalized, and proofs in normal form fulfill the subformula property. Having this result at hand, the proof of conservation is relatively easy to obtain. Furthermore, we are interested in an efficient way to obtain normal forms of proofs. We therefore introduce normalization by evaluation for a predicative polymorphic lambda-calculus which can be used to normalize proofs in predicative second-order logic.
- Juan Belo, 14. Mai 2008.
Logic setups.
I will present an abstract notion of logic theory which maintains the traditional distinction between the theory of proofs and the theory of sorts that compose a logic theory but which otherwise provides a uniform treatment of both, in particular substitution and (definitional) equality. This essentially builds on Peter Aczel's notion of a Type Setup, Peter Dybjer's Categories with Families, and John Cartmell's Generalised Algebraic Theories.
WS 2007/2008
- Rudolf Taschner, 1. Februar 2008 (Sondertermin, 14:15, im B132).
Integrale in der konstruktiven Mathematik.
Vereinbart man, dass nur Sätze gelten dürfen, die mit konstruktiven Hilfsmitteln beweisbar sind, erhält man eine Analysis, die sich in entscheidenden Gesichtspunkten grundlegend von der auf der Mengentheorie Cantors fussenden und mit formaler Logik argumentierenden Analysis unterscheidet. Die deutlichsten und spannendsten Differenzen ergeben sich, wenn man den rigorosen, von Brouwer vertretenen Standpunkt einnimmt, bei dem das Prinzip des "tertium non datur" nur im Kontext endlicher Mengen Gültigkeit besitzt. Eine der Konsequenzen hieraus ist, dass eine über einem kompakten Intervall definierte Funktion a fortiori gleichmässig stetig sein muss. Damit scheint eine Integrationstheorie von über kompakten Intervallen definierten Funktionen im besten Fall auf das bereits von Cauchy betrachtete Integral reduziert, also praktisch obsolet. Dies aber ist keineswegs der Fall. Auch für Funktionen, die nur auf dichten Teilmengen eines kompakten Intervalls definiert sind und nicht stetig sein müssen, kann man bei geeigneten Voraussetzungen ein Integral definieren, und es zeigen sich sehr reizvolle Varianten zum Satz von Lebesgue über dominierte Konvergenz.
- Paulo Oliva, 23. Januar 2008.
On modified bar recursion and its variants.
In 1969 Spector devised a new form of recursion, so-called bar recursion, which could be used to give a computational interpretation of countable choice (and hence comprehension). Spector's interpretation uses Goedel's Dialectica interpretation. Recently, a new form of bar recursion, dubbed modified bar recursion, has been suggested which does a similar job but uses Kreisel's modified realizability instead. In this talk I will discuss three variants of modified bar recursion. The first is due to Berardi, Bezem and Coquand; the second is a simplification of the BBC bar recursion by Ulrich Berger, and the third is a variant which comes from recent work of Martin Escardo on selection functionals for compact spaces. The talk will cover both the motivations for these functionals and the issues of inter-definability and the running time complexity in practical applications.
- Sebastiaan Terwijn, 16. Januar 2008.
The Medvedev lattice.
The Medvedev lattice is a structure from computability theory that was introduced in an attempt to capture the meaning of constructive logic in terms of computations. Although the attempt failed initially, the lattice was found to be interesting also for other reasons, and the notion of Medvedev reducibility turned out to be useful for the classification of sets of reals. In this talk we review the basics of the Medvedev lattice and its relation to constructive logic. We also comment on the relation to other subjects, such as the study of Pi-0-1 classes and measure theory.
- Christophe Raffalli, 20. Dezember 2007
(Mitarbeiterbesprechung, 14:15, B415).
Realizability: from definitions to the axiom of choice
We will give the basic definitions and the main application:
adequation lemma
data types and storage operators (a fundamental tool)
mixed logic and program extraction
the intentional axiom of choice
and may be, model construction for second order logic (this could be generalized to ZF) which allow to see realizability as a generalization of forcing which could allow for manipulation of the natural numbers in the future (which forcing does not allow)
- Christophe Raffalli, 19. Dezember 2007.
PML: a new kind of proof assistant using programs as proofs.
We will present PML, it's constraint checking (and not solving) type system allowing the great unification of cartesian products; the Knuth-Bendix based proof checking; the use and importance of exception in the language and many other characteristic of the project. The talk will include a demo.
- Thierry Coquand, 14. Dezember 2007 (Kolloquium, 16:15, A027).
Infinite objects in constructive mathematics.
- Thierry Coquand, 13. Dezember 2007
(Mitarbeiterbesprechung, 14:15, B415).
Geometric Logic.
- Henri Lombardi, 12. Dezember 2007.
Spectral spaces, Krull dimension, lying over, going down, going up: a constructive approach.
- Dan Hernest, 5. Dezember 2007.
Hybrid functional interpretations (Work in progress with Paulo Oliva).
We show how different functional interpretations can be combined using linear logic. A hybrid of Kreisel's modified realizability and Goedel's Dialectica thus yields out of a proof of weak existence of Fiboncacci numbers a better program than Dialectica alone. The effect is similar to Dialectica light, but mixing the non-computational quantifiers to the hybrid further strictly enhances its capabilities.
- Peter Schuster, 21. November 2007, Beginn um 16:30!
Formal Methods in Commutative Algebra.
A partial realisation of Hilbert's programme in (commutative) algebra has proved practicable in the preceding years. It means to exclusively work with finite methods, and without ideal objects such as prime ideals, whenever the data under consideration are sufficiently concrete. In other words, constructive proofs are sought, and found, during which one need not go beyond the type level on which the theorems are formulated. This approach of a point-free and syntactical flavour gained power when ideas from formal topology and from dynamical algebra were combined. As stressed by Wraith, its success is guaranteed by Barr's completeness theorem for geometric logic, in which large parts of algebra can be formulated. One of the milestones was the elementary and inductive characterisation of Krull dimension given by Coquand, Lombardi, and Roy. This made possible, among other things, a constructive proof on low type levels of the theorem of Eisenbud-Evans-Storch, which says that d+1 polynomials suffice to generate, up to radicals, any finitely generated ideal of univariate polynomials with coefficients in a ring of Krull dimension d. (This generalises the fact that every variety in dimension d is an intersection of d hypersurfaces, for which Kronecker still needed d+1 hypersurfaces.) As a typical theorem with concrete input and concrete output, the Eisenbud-Evans-Storch theorem merits a proof exclusively done by finite methods. The proof we have produced with Coquand and Lombardi further provided deeper insight into the topological character of the problem, and prompted a variant of Kaplansky's regular element property which is of some interest on its own. We take this theorem and its proof as a guiding example for our survey, and will indicate some possible future work.
- Stan Wainer, 31. Oktober 2007.
Accessible Recursive Functions.
SS 2007
- Douglas Bridges, 30. Mai 2007.
Constructive reverse mathematics.
- Peter Clote, Donnerstag. 24. Mai 2007, 14-16
(Sondertermin!)), B251
RNA: Asymptotics for minimum free energy and shapes.
Computational molecular biology consists of three overlapping fields: structural biology, computational genomics and systems biology. Structural biology concerns the algorithmic study of protein and RNA structures, their function and molecular evolution. While the goal of computational biology concerns algorithm development and implementation, there exist certain mathematical problems which lie at the heart of bioinformatics, such as the largest common subsequence (LCS) problem and a related problem concerning expected minimum free energy (MFE) of random RNA. In this talk, we describe an asymptotic limit for expected MFE of random RNA, some bounds for this limit, and apply generating function methods to compute the asymptotic number of saturated structures and of RNA shapes. Since recurrence relations and combinatorics lies at the heart of ab initio dynamic programming RNA secondary structure prediction algorithms, we describe some of the algorithmic applications of the mathematics. This talk presents results from several papers, which are joint work with E. Kranakis, D. Krizanc, W.A. Lorenz, Y. Ponty, L. Stacho, and J. Waldispuhl. Publications and web servers for algorithms are found at bioinformatics.bc.edu/clotelab/
- Dirk van Dalen, 9. Mai 2007.
Continuity versus Decidability.
- Ulrich Schoepp, 18. April 2007.
Stratified Bounded Affine Logic for Logarithmic Space.
A number of complexity classes, most notably PTIME, have been characterised by sub-systems of linear logic. In this talk I will show that the functions computable in logarithmic space can also be characterised by a restricted version of linear logic. I will introduce Stratified Bounded Affine Logic (SBAL), a restricted version of Bounded Linear Logic, in which not only the modality `!' but also the universal quantifier is bounded by a resource polynomial. Proofs of certain sequents in SBAL represent the functions computable logarithmic space. The translation of SBAL-proofs to LOGSPACE-functions is based on modelling computation by interaction dialogues in a version of the Geometry of Interaction. The purpose of this talk is to introduce SBAL, give examples and to outline how SBAL-proofs can be compiled to space-efficient programs.
WS 2006/2007
- Albert Ziegler, 22. Januar 2007.
Finding Models of Constructive Set Theory.
Like with classical ZF set theory, the understanding of constructive set theories is greatly advanced by looking at (relative) models. They foster intuition about set theoretic universes, are used to prove interesting relative consistency results and help to analyse proof theoretic strengths. Two main methods to construct such models have been Heyting algebra constructions, which are the constructive analogon of forcing with Boolean algebras, and realisability theory, which has no classical analogon and is closely connected to computability theory. By developing a machinery blending formal topology with applicative structures, it will be shown that these two constructions are actually special cases of a much more general one that has applications which could not have been obtained with one of these conventional classes of models.
- Nicola Gambino (Universite de Quebec a Montreal, UQAM),
18. Dezember 2006.
Cartesian closed categories and species of structures.
The notion of a cartesian closed categories isolates what structure is necessary in order to provide a model of the simply-typed lambda calculus. The notion of a species of structures was introduced by Andre` Joyal to provide a combinatorial counterpart of the calculus of exponential power series. The aim of the seminar is to present joint work with Marcelo Fiore, Martin Hyland, and Glynn Winskel: we introduced a generalisation of Joyal's notion, and proved that it gives rise to a cartesian closed structure.
- Paul Taylor (University of Manchester), ausnahmsweise am
Donnerstag, 14. Dezember 2006 14-16 Uhr (Raum noch offen!).
The definitive axiomatisation of ASD (maybe).
- Michael Rathjen, 11. Dezember 2006.
Noch mehr Gleichungen in der Mengenlehre lösen.
In der Mengenlehre mit dem Antifundierungsaxiom (AFA) lassen sich viele selbstbezügliche und zirkuläre Phänomene modellieren. Eine besonders attraktive Konsequenz von AFA ist das allgemeine Lösungslemma, welches besagt, dass sich sogenannte flache Gleichungssysteme in Mengen immer lösen lassen. Doch manchmal fallen diese Lösungen auch unbefriedigend aus und gewisse nichtflache Gleichungssysteme haben nachweislich keine Lösungen - zumindest klassisch. Im Vortrag soll der Frage nachgegangen werden, ob dem Mangel an Lösungen gelegentlich durch einen Wechsel zu intuitionistischer Logik aufgeholfen werden kann?
- Henri Lombardi (Universität Besancon), 27. November 2006.
Geometric theories, lazy evaluation, and constructive algebra.
- Gunnar Wilken (Universität Münster),
20. November 2006.
Elementary Patterns of Resemblance zweiter Ordnung.
Der Vortrag gibt eine Übersicht über Timothy J. Carlsons Zugang zu Ordinalzahlbezeichnungen mithilfe seiner "Elementary Patterns of Resemblance". Es wird eine Ordinalzahlarithmetik vorgestellt, die eine genaue Analyse von patterns erster und zweiter Ordnung ermöglicht. Am Ende steht die Präsentation eines Unabhängigkeitsresultates zur Kombinatorik von patterns zweiter Ordnung.
- Lev Beklemeshiev,
(Steklov Institut, Moskau), 16. Oktober 2006.
Provable and unprovable properties of polymodal provability logic GLP.
I will discuss Japaridze's logic GLP from a modal-logical point of view, give a generalized Kripke semantics for it and also formulate some modal-logical statements that are unprovable in Peano arithmetic.
SS 2006
- Jens Erik Fenstad, Universität Oslo, 17. Juli 2006.
Logic, Grammar and Models of Mind.
- Trifon Trifonov, 12. Juni 2006.
Normalization of bimachines.
- Andreas Abel, 29. Mai 2006.
Higher-Order Subtyping Revisited.
Higher-Order Subtyping is important for models of object-oriented languages (F-omega-sub) and for sized higher-kinded data types. Completeness of algorithmic higher-order subtyping is difficult to prove and usually involves a model construction. This talk presents a much simplified, purely syntactical completeness proof that exploits the fact that the type-language is essentially the simply-typed lambda-calculus and, hence, of low proof-theoretical strength.
- Peter Aczel, 15. and 22. Mai 2006.
The semantics of IPC (intuitionistic propositional logic) in CST (constructive set theory).
The talk will be motivated by the desire to prove that a strong completeness property for IPC, sigma-CP, is relatively consistent with the formal system CZF for CST. In my talk I will first formulate sigma-CP, an assertion that strongly contradicts the law of excluded middle. The main part of the talk will be a discussion, in the context of CST, of the various kinds of semantics that have been given for IPC; algebraic, topological, Kripke, Beth. My talk will end, if there is enough time, with the statement and proof, in CZF, of a strong completeness result for the topological semantics of IPC in Baire space. The result is expected to be the key lemma in showing in CZF that sigma-CP holds in the sheaf model of CZF over Baire space. Parts of the research for this talk is joint work with the PhD student, Yong Wang.
- Pavel Hrubes, 8. Mai 2006.
Lower bounds for modal logics.
I will give a brief introduction to basic problems and tools of proof complexity, namely the problem of finding lower bounds on sizes of proofs and the concept of effective interpolation. Furthermore, I sketch the proof that the basic system of modal logic, K, has a form of effective monotone interpolation, which gives an exponential lower bound on the lengths of proofs in K. Applications to other systems of modal logic will also be discussed.
- Dan Hernest, 24. April 2006.
The light Dialectica interpretation.
In some cases, a number of Contractions are redundant for Goedel's Dialectica Interpretation. We identify and isolate such redundant Contractions by means of an adaptation of Berger's non-computational-content universal and existential quantifiers. We name light Dialectica interpretation this optimization of Goedel's program extraction technique.