Date: Friday, 09/12/2016 - 09:45 - 16:45
Location: Turing hall, Science Park Congress Centre, Amsterdam
Chairman: Teun Koetsier (VU)
|9:45||Welcome by Erik van den Ban, president KWG|
|9:50||Opening symposium by Jos Baeten, director CWI|
|10:00||Sergei Artemov, Intuitionism and Knowledge|
|10:35||Raf Bocklandt, Reflections on a cup of coffee|
|11:35||Mark van Atten, On two problems with the Theory of the Creating Subject|
|12:10||Alexander Dranishnikov, On topology of robot motion planning|
|13:45||Saul Kripke , Free choice sequences: A temporal interpretation compatible with acceptance of classical mathematics|
|14:20||Yiannis Moschovakis, Intuitionism and effective descriptive set theory|
|15:20||Michael Rathjen, Indefiniteness, definiteness and semi-intuitionistic theories of sets|
|15:55||Dirk van Dalen, Where did it all begin?|
|16:30||Closure and drinks|
Sergei Artemov, Intuitionism and Knowledge
We argue that in the intuitionistic format, paradigmatic Gettier counterexamples to “Justified True Belief yields Knowledge” fail. Indeed, Gettier examples provide a disjunction D = A v B of propositions A and B such that A is "justified" (falsely) and B is true but not justified, hence D is justified, believed and true, but not knowledge.
Intuitionistically, the truth of B is supported by a proof p. If the agent is aware of p then the agent knows B, since proof yields knowledge. Hence, for such an agent, truth of B yields knowledge of B, hence knowledge of D.
A fake Gettier "justification" of A is a mere distraction. If the agent is not aware of any proof of B, then we cannot claim that B is true for this agent at this stage of cognition. This argument suggests that intuitionistically, Justified True Belief yields Knowledge.
These and similar observations lead to Intuitionistic Epistemic Logic, IEL (developed in collaboration with Tudor Protopopescu), with new intuitionistic epistemic principles, intuitive Kripke semantics, completeness theorems, etc. In IEL, co-reflection A -> KA and intuitionistic reflection KA->~~A hold, but the classical reflection KA -> A fails, since there might be verifications of A (hence KA) that do not produce an explicit proof of A.
Raf Bocklandt, Reflections on a cup of coffee
Allegedly Brouwer discovered this famous fixed point theorem while stirring a cup of coffee and noticing that there is always at least one point that does not move. In this talk we will tell how Brouwer's ideas about this phenomenon spilt over in a lot of different areas of mathematics and eventually led to an intriguing geometrical theory we now know as Mirror Symmetry.
Mark van Atten, On two problems with the Theory of the Creating Subject
Kreisel introduced the Theory of the Creating Subject to isolate and formulate explicitly the properties of the thinking subject that Brouwer used in certain arguments. Characteristic of these arguments is their exploitation of the fact that the activity of making mathematical constructions has itself a mathematical structure. In this talk, I will discuss two problems that have arisen with this theory. The first, perceived by Kreisel himself, lies in the fact that the Creating Subject's activity is supposed to proceed in an omega-sequence of steps, yet Brouwer also accepted proofs of transfinite length. The second, Troelstra's Paradox, suggests that there is too much self-reflexivity in the Theory of the Creating Subject. I will argue that Kreisel's objection is mistaken, and present a new solution to Troelstra's Paradox.
This paper presents a way of supplementing classical mathematics with a motivation for a Brouwerian theory of free choice sequences. The idea is that time is unending, so that one can never come to an end of time, but also indeterminate, so that in a branching time model only one branch represents the ‘actual’ one. This can be random or subject to various restrictions imposed by the creating subject. The fact that the underlying mathematics is classical makes such perhaps delicate issues as the fan theorem no longer problematic. On this model, only intuitionistic logic applies to the Brouwerian free choice sequences, not because of any skepticism about classical mathematics, but because there is no ‘end of time’ when everything about them can be decided.
Alexander Dranishnikov, On topology of robot motion planning>
The topological complexity TC(X) of a configuration space X of a robot was defined by M. Farber as a numerical invariant that measures stability of robot's motion planning algorithms. Computation of TC is a difficult problem. In the talk we will discuss how TC can be computed for surfaces. Also we demonstrate how ideas from the classical dimension theory can bring estimates of upper bounds for TC(X).
Yiannis Moschovakis, Intuitionism and effective descriptive set theory
We identify and analyze some common basic themes, problems and results of intuitionistic analysis and effective descriptive set theory, including applications of each of these fields to the other. The technical results include justifying inductive definitions with universally quantified clauses in the basic fragment B of Kleene's formal intuitionistic analysis which is classically sound, which then allows us to define rigorously in B the class of Borel sets and prove that they are all analytic. This, however, is primarily an expository paper, aiming to make available these simple ideas to mathematicians and logicians who are familiar with only one - perhaps neither- of the two research areas in the title.
Michael Rathjen , Indefiniteness, definiteness and semi-intuitionistic theories of sets
Brouwer argued that limitation to constructive reasoning is required when dealing with "unfinished" totalities. As a complement to that, the predicativists such as Poincaré and Weyl (of Das Kontinuum) accepted the natural numbers as a "finished" or definite totality, but nothing beyond that. In addition, the "semi-intuitionistic" school of descriptive set theory (DST) of Borel et al. in the 1920s took both the natural numbers and the real numbers as definite totalities and explored what could be obtained on that basis alone.
From a metamathematical point of view, these and other different levels of indefiniteness/definiteness can be treated in the single framework of semi-intuitionistic theories of sets, whose basic logic is intuitionistic, but for which the law of excluded middle is accepted for bounded formulas.