LogikArbeitstagung Bern, München und Verona
December 12–13, 2019
Logic and Theory Group

Program
Wednesday 11.12
19:30  Welcome Dinner at Sarovar
Fürstenstr. 12 
Thursday 12.12
09:0009:45 
Michel Marti: Reinforcement Learning

09:4510:30 
Iosif Petrakis: On the BHKinterpretation of BISH within BISH

10:3011:00 
Coffee Break

11:0011:30 
Michael Bärtschi:ATR and parameters

11:3012:30 
Masahiko Sato: Unification of the LambdaCalculus and Combinatory Logic

12:3014:00 
Lunch Break

14:0015:00 
Lorenzo Rossi: Bicontextualism

15:0016:00 
Gerhard Jäger: Some settheoretic reduction principles

16:0016:30 
Coffee Break

16:3017:30 
Matthias Eberl: A relative infinite

17:3018:30 
Thomas Powell: A new application of proof mining in the fixed point theory of
uniformly convex Banach spaces

19:30  Dinner at Los Faroles
Nordendstr. 26 
Friday 13.12
09:0010:00 
Vasco Brattka: A Brouwer algebra related to the Weihrauch lattice

10:0010:30 
Coffee Break

10:3011:30 
Makoto Fujiwara: Constructivism and weak logical principles over arithmetic

Talks
The standard BHKinterpretation of BISH is quite vague. In
this talk we explain how an explicit BHKinterpretation of BISH within
BISH would look like. For that we are using the following ingredients:
(i) The fundamental notion of a setindexed family of sets and its
corresponding ∑and ∏sets.
(ii) A proofrelevant formulation of a membershipcondition of a subset
given by an existential formula. This formulation is connected to
Feferman's notion of membershipwithevidence.
(iii) A proofrelevant formulation of an equalitycondition of a set
given by
an existential formula. This formulation is connected to MartinLoef's
identity type.
We discuss certain technical variants of arithmetical transfinite recursion (without set parameters). It is shown that a certain parameter, called "field variable", can always be included without loss of generality.
It is wellknown that the Lambda Calculus and Combinatory Logic are
two closely related theories both used to study computable functions.
In this talk, however, I will argue that they are in fact one and
the same calculus.
To show this I will unify these two systems into a single system
whose syntax naturally contains the syntax of the two systems.
The unification is carried out in three steps:
1. We start from Church's syntax Λ for λterms,
but will provide a new way of looking at these terms modulo
αequivalence.
2. We formalize Combinatory Logic by giving a completely new syntax
Δ for Combinatory Logic.
3. We obtain the ultimate system by simply taking the union of
Λ and Δ.
(Joint work with Takafumi Sakurai and Helmut Schwichtenberg.)
Can one quantify over absolutely everything? Absolutists answer positively, while relativists answer negatively. Relativists typically justify their rejection of absolute generality via an argument from paradox: given any alleged maximal domain of quantification D, a paradoxical reasoning can be devised that shows that something is not in D. So, relativists conclude, D does not contain absolutely everything. In this paper, I focus on the absolutism/relativism debate in the framework of theories of truth. In its truththeoretic incarnation, generality relativism is a form of contextualism about truth predications, and the argument from paradox is a version of the Liar Paradox. Contextualist theories of truth have a number of virtues: they provide elegant and uniform solutions to the semantic paradoxes while preserving full classical logic. However, they are forced to interpret harmless quantified sentences (such as «everything is selfidentical») in less than than absolutely comprehensive domains, thus misconstruing semantic and scientific generalizations. The purpose of this paper is to improve on this shortcoming, and to show that contextualism is compatible with absolute generality. I develop a bipartite contextualist semantics, bicontextualism for short, in which sentences are divided in two groups: the unparadoxical ones, which are given an absolutist semantics, and the paradoxical ones, which are given a relativist semantics. I then show that bicontextualism retains the virtues of (standard) contextualism, and discuss how it addresses expressive challenges (such as revenge paradoxes).
We study several reduction principles in the context of Simpson’s settheoretic version of ATR_{0} and KripkePlatek set theory KP.
We investigate how to develop mathematics with the notion of a potential infinite only, using no completed infinities. Potential infinite means that totalities are indefinitely extensible but at each stage finite. This includes Dummett's situation that a reference to a totalities of objects creates a new object of it (e.g. the set of all sets). It turns out that this approach is not a restriction, but an enrichment. This is due to the fact that an indefinitely extensible totality allows intermediate states which behave like completed infinities. These states can be called "indefinitely large" (cf. S. Lavine) or "sufficiently large". In order to describe them we will introduce a notion of a relative infinity.
Technically, the basics go back to Jan Mycielski. We will formulate it as a kind of Tarskian model theory in which the carrier set is potential infinite. That is, instead of a flat set we use a system (a family of sets). The indefinitely large states are then (relative) limits inside the system. This approach allows extensions to other logics than classical ones, mainly intuitionistic logic. In this talk we will motivate this idea and present the situation for first order logic. We will shortly discuss some metamathematical consequences and then introduce a model for STT and mention open topics.
Proof mining is a branch of mathematical logic which makes use of proof theoretic techniques to extract quantitative information from seemingly nonconstructive proofs. In this talk, I present a new application of proof mining in functional analysis, which focuses on the convergence of the Picard iterates (T^{n}x)_{n∈ℕ} for a class of mappings T on uniformly convex Banach spaces whose fixpoint sets have nonempty interior.
We prove that the Weihrauch lattice can be transformed into a Brouwer algebra by the consecutive application of two closure operators in the appropriate order: first completion and then parallelization. The closure operator of completion is a new closure operator that we introduce. It transforms any problem into a total problem on the completion of the respective types, where we allow any value outside of the original domain of the problem. This closure operator is of interest by itself, as it generates a total version of Weihrauch reducibility that is defined like the usual version of Weihrauch reducibility, but in terms of total realizers. From a logical perspective completion can be seen as a way to make problems independent of their premises. Alongside with the completion operator and total Weihrauch reducibility we need to study precomplete representations hat are required to describe these concepts. In order to show that the parallelized completed Weihrauch lattice forms a Brouwer algebra, we introduce a new multiplicative version of an implication. While the parallelized completed Weihrauch lattice forms a Brouwer algebra with this implication, the completed Weihrauch lattice fails to be a model of intuitionistic linear logic in two different ways. In order to pinpoint the algebraic reasons for this failure, we introduce the concept of a Weihrauch algebra that allows us to formulate the failure in precise and neat terms.
(Joint work with Guido Gherardi, University Bologna, Italy.)
In 1930’s, A. Heyting introduced socalled Heyting arithmetic (HA) with an informal semantics, called the BrouwerHeytingKolmogorov(BHK) interpretation, which works as a criterion for the constructive reasoning thereafter. Note that HA is based on intuitionstic logic and one can obtain classical arithmetic (PA) just by adding the law of excluded middle (A or not A) into the axioms of HA. Though the sentences provable in HA are valid in the (informal) sense of the BHK interpretation, it seems not that all the sentences valid in the BHK interpretation are provable in HA. Thus some weak fragment of the law of excluded middle seems to be contained in the arithmetic which exactly obeys the BHK interpretation. Motivated from this observation, the structure (derivability relation) of weak logical principles has been studied over Heyting arithmetic and its extension in all finite types. In fact, the weak logical principles are closely related to various kinds of realizability, which can be seen as formal treatments of the BHK interpretation. To show that one logical principle A does not imply another principle B, one typically uses appropriate forms of realizability to show that A has a certain semiconstructive interpretation which B does not. In this talk, we overview the known structure of the weal logical principles and discuss about the relation with the variations of realizability. The contents of this talk are almost the same as those of my previous talk at the workshop "Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism” held at Stockholm University during August 20–23, 2019.
Accommodation
Pension JosefineOrganizer
Franziskus WiesnetLast modified
10.12.2019