Contributed Presentations

Eldar Fischer and Johann Makowsky. Extensions and limitations of the Specker-Blatter Theorem

Abstract: The original Specker-Blatter Theorem (1983) was formulated for classes of structures of one or several binary relations definable in Monadic Second Order Logic MSOL. It states that the number of such structures on the set is modularly C-finite (MC-finite). In previous work we extended this to structures definable in CMSOL, MSOL extended with modular counting quantifiers. The first author also showed that the Theorem does not hold for one quaternary relation (2003).

In this paper we show:

1) The Specker-Blatter Theorem also holds for CMSOL when hard-wired constants are allowed. The proof method of Specker and Blatter does not work in this case.

2) The Specker-Blatter Theorem does not holds already for with one ternary relation definable in First Order Logic FOL. This was left open since 1983.

Using hard-wired constants allows us to show MC-finiteness of counting functions of
various restricted partition functions which were not known to be MC-finite till now. Among them we have the restricted Bell numbers , restricted Stirling numbers of the second kind or restricted Lah-numbers . Here is an non-negative integer and is an ultimately periodic set of non-negative integers.

Lorenz Halbeisen and Salome Schumacher. Some implications of Ramsey Choice for n-element sets

Abstract: For a positive natural number n, “Ramsey Choice for n-element sets”, denoted RC(n), is the choice-principle that every infinite set X contains an infinite subset Y such that the family of n-element subsets of Y has a choice function. The relation between RC(n) and several other choice principles for families of n-elements sets will be discussed. This is joint work with Salome Schumacher.

Vince Velkey. Game proofs of Lebesgue measurability

Abstract: Infinite games can be used to prove regularity properties from determinacy. Usually, due to the Solovay unfolding phenomenon, determinacy at some level of the projective hierarchy gives the regularity property at the next; in particular, Borel determinacy gives analytic regularity.
However, in the usual proof of the key lemma for Lebesgue measurability, we use the fact that all analytic sets are Lebesgue measurable. We discuss how to avoid this problem by moving to different games characterising Lebesgue measurability.

Vasco Brattka. Continuity and computability of functions

Abstract: We discuss the relation between computability and continuity of functions. For one, there is a well-known classical result of Addison that shows that continuity is just computability with respect to some oracle, which establishes a uniform relation between the two concepts. On the other hand, it is folklore in Weihrauch complexity that the limited principle of omniscience (LPO) is the weakest single-valued discontinuous function with respect to the topological version of Weihrauch complexity, which provides another uniform characterization of discontinuity. If combined with results by Matthias Schröder on admissible representations, then this characterization of discontinuity carries over to a wide class of topological spaces. It is also well-known that LPO parallelizes to the Turing jump function. If one combines all these results in the appropriate way, then one obtains a non-uniform characterization of continuity of single-valued functions over a wide class of topological spaces in first-order terms over Turing degrees. Essentially, this characterization states that a function is discontinuous if and only if its parallelization computes Turing jumps on a Turing cone. If written out with quantifiers, then this characterization is reminiscent of the classical epsilon-delta characterization of uniform continuity for metric spaces, where epsilon and delta are now ranging over Turing degrees, the metric is replaced by the Turing degree map and pairs of points are replaced by sequences.

Lucas Wansner. Amoeba-regularity and inaccessibles

Abstract: In 1995 Judah and Repický defined a regularity property we call amoeba-regularity. Similar to the most other regularity properties, the amoeba-regular sets form a σ-algebra containing all analytic sets. However, the statement “every set in second level of the protective hierarchy is amoeba-regular” is independent from ZFC.

In this talk, we investigate the consistency strength of this statement and show that it implies that the first uncountable cardinal in V is inaccessible in L. In fact, we show if all sets in a given level of the protective hierarchy are amoeba-regular, then all sets in the same level have the Baire property in the dominating topology.

This is joint work with Raiean Banerjee (Hamburg).

Lukas Schembecker and Vera Fischer. Partitions of Baire space into compact sets

Abstract: We define a c.c.c. forcing which adds a maximal almost disjoint family of finitely splitting trees on ω (a.d.f.s. family) or equivalently a partition of Baire space into compact sets of desired size.
Furthermore, under CH we construct a Sacks-indestructible (by countably supported iteration and product of any length) maximal a.d.f.s. family.

David Binder and Thomas Piecha. Administrative Normal Form and Focusing for Lambda Calculi

Abstract: The Curry-Howard correspondence between deductive systems and computational calculi is one of the great unifying ideas. It links purely logical investigations to practical problems in computer science, in particular the design and implementation of programming languages. Many aspects of this correspondence are widely known, such as the correspondence between natural deduction for intuitionistic logic and the simply typed lambda calculus. On the other hand, the importance of the sequent calculus in proof-theoretic investigations is not yet reflected in the study of programming languages, where languages based on the lambda calculus dominate. Our contribution is a step towards bridging this gap by introducing and discussing the correspondence between two normal forms and their respective normalization procedures: administrative normal form and ANF-transformation on the one hand, and focused normal form and static focusing on the other. Though invented for different purposes, compiler optimizations in the case of the ANF-transformation and proof search in the case of focusing, they are structurally very similar. Both transformations bring proofs into a normal form where functions and constructors are only applied to values and where computations are sequentialized. In this talk we make this similarity explicit by showing how the ANF-transformation on lambda terms corresponds to static focusing of lambda-mu-mu’tilde terms.

Marcel Ertel. Paul Bernays and the philosophical significance of independence results

Abstract: We provide a reconstruction of Paul Bernays’ assessment of the philosophical significance of independence and non-conservativity phenomena in mathematics. In the first part, we sketch a systematic presentation of Bernays’ post-1931 philosophy of mathematics, a fully worked-out account of which remains a desideratum today. Particular emphasis is laid on the relationship of formal and ‘contentual’ reasoning, the differentiation of degrees of (non-)constructivity, the open-endedness of mathematical concept-formation, and the questions of evidence and objectivity in mathematics. In the second part, we investigate on this basis Bernays’ response to the Gödel-Cohen independence results in set theory, with special emphases on Bernays’ subtle assessment of the roles of first-order logic and of schemata, and on his account of the concept of a non-standard model. In this context we also discuss Bernays’ 1961 axiomatization of class theory BL (“Bernays-Levy”) based on a reflection principle, which yields the usual axioms as well as much stronger large cardinal existence theorems (below measurable cardinals), but which incurs philosophical difficulties due to it requiring the existence of non-predicative classes, conflicting with Bernays’ own account of the set-vs.-class distinction. In the final part, the results of the earlier parts are related to contemporary debates on the justification of new axioms and on the issue of truth-value (in)determinacy in set theory.

Levin Hornischer. Dynamical Systems via Domains: Semantics for Non-symbolic Computation

Abstract: Famously, domain theory provided a mathematical semantics for symbolic computation: systematically explaining code of a programming language by assigning it to the mathematical object computed by it. We lack this kind of explainability for the non-symbolic computation performed, e.g., by neural networks in artificial intelligence. This talk, which is based on my PhD thesis, suggests an extension of domain-theoretic semantics to non-symbolic computation.

Generally, non-symbolic computation can be viewed as a dynamical system: a set of (computational) states together with a dynamics describing how to move from one state to the next (program). Thus, the task is to construct, for a given dynamical system, a `domain’ that describes the behavior of the system. Domains, i.e., the object of study of domain theory, are certain partial orders whose elements intuitively are regarded as outputs of computational processes while the order describes information containment.

To build the semantics, the high-level idea is this: Given a dynamical system X, we construct a structure D that we will call the dynamical domain of X. Intuitively, D consists of `basic’ elements that represent increasingly finer observations of the system X together with the `limits’ of these basic elements. The additional domain-theoretic structure on D is such that it induces a dynamical system on these limit elements, which we call the system modeled by D. We show that this modeled system is isomorphic to X. Categorically speaking, we then prove that the construction of the dynamical domain for a system and the construction of the system modeled by a dynamical domain are adjoint.

Matteo de Ceglie. A generalisation of the set theoretic multiverse

Abstract: Ten years ago, Hamkins, 2012 changed the landscape of the foundations of mathematics, by introducing a novel conception that tried to clarify some ambiguous notions in current set theoretic practice. In particular, he provided a revolutionary interpretation for the practice of forcing: a multiverse of different set theoretic universes. Such an idea immediately sparked an intense debate in the philosophy of set theory and the foundations of mathematics. In the following years, several crucial contributions were made.

Indeed, while the general idea behind pluralism in the philosophy of mathematics is more or less the same every time, the actual mathematical details can vary enormously from one characterisation to the other. Even though all these different set theoretic multiverses share the same, general, philosophical idea, they differ wildly from the mathematical perspective. There are some proposal of assessing all these differences, but this research field is still in its infancy. In this paper, I propose a novel, more general, framework for the set theoretic multiverse: the Universal Multiverse.

Drawing from the ideas of Universal Logic, this new framework is not a new set theoretic multiverse. Instead, it is a general theory ofthe multiverse, that investigates the various set theoretic multiverses from a common and abstract point of view. This means highlighting the common features of all multiverses, studying them as mathematical structures without any other metaphysical and ontological connotation.

The first step to carry out this program is to define a method of comparing and categorising all the different multiverses. A multiverse can be characterised in several ways: the most common one is to describe it as a set of universes. For example, Steel’s set generic multiverse is the set of all set-generic extensions of a core universe, Friedman’s Hyperuniverse is the set of all countable transitive models of ZFC, etc..

Generalising on this idea, a general theory of the set theoretic multiverse is the theory of the Multiverse Operator, Mlti. This theory is analogous to Tarski’s theory of the consequence operator as introduced in Tarski, 1928. A multiverse operator is a function defined on a stage Vκ of a set theoretic universe. A multiverse operator maps each stageVκ with the set of all universes, M, that are part of the multiverse generated using Vκ as the ground universe:

Mlti : Vκ → M.

For example, the operator Mltgeneric applied to any Vκ, written Mltgeneric(Vκ), will map to Steel’s set generic multiverse. In this way we can define in very general terms what a set theoretic multiverse is: it is an ordered couple (Vκ,Mlti), where Vκ is a stage ofV and Mlti is a multiverse operator.

The general theory of the multiverse that I propose is the study of the multiverse operator in general, without considering the special feature of each of them (e.g. the difference between Mltgeneric and Mltvlogic). From this very abstract and general perspective, I claim that the general structure ⟨Vκ,Mlt⟩ forms a Tarski structure. That is, it obeys the following axioms:

1)Vκ ⊆ Mlt(Vκ);
2)Vκ ⊆ Vλ ⇒ Mlt(Vκ) ⊆ Mlt(Vλ);
3)Mlt(Mlt(Vκ)) ⊆ Mlt(Vκ).

In this paper, I will expand on the meaning of these axioms for the multiverse operator, and sketch the road forward in this research field.

Christine Gaßner. Second-Order Henkin Semantics and the Axiom of Choice

Abstract: Inspired by questions raised by Paolo Mancosu and Stewart Shapiro (2018), we will examine in more detail the meaning of the Axiom of Choice in second-order predicate logic. First, we give an overview of second-order predicate logic with comprehension axioms for predicates and briefly compare different well-known variants of the Henkin interpretation which have been described in detail by Henkin (1950), Shapiro (1991), Väänänen (2019), and others. The model-theoretic semantics mainly discussed here is based on so-called predicate structures and second-order Henkin structures, as defined by Asser (1981) on the basis of a suggestion by his student and later colleague, Schreiber. The predicates are attributes in the sense of Scholz and Hasenjaeger (1961), and the language used is a many-sorted first-order language with identity. In the second part, we summarize consequences for the relationships between different formulations of the axiom of choice. In particular, we consider second-order principles of choice introduced by Ackermann (1935), Hilbert and Ackermann (1938) and Asser (1981), which we consequently call Ackermann axioms, Hilbert-Ackermann axioms, Zermelo-Asser axioms, Russell-Asser axioms, and Asser axioms, respectively. The Fraenkel-Mostowski-Specker-Asser method used to construct second-order Henkin structures allows us to provide new insights into the relationships between these principles.

References
Ackermann, W.: Zum Eliminationsproblem der mathematischen Logik. Mathematische Annalen 111, 1935, pp. 61−63.
Asser, G.: Einführung in die mathematische Logik, Teil III: Prädikatenlogik höherer Stufe. Teubner, 1981.
Gaßner, C.: The Axiom of Choice in Second-Order Predicate Logic. Mathematical Logic Quarterly, 40 (4), 1994, pp. 533−546.
Henkin, L.: Completeness in the Theory of Types. Journal of Symbolic Logic 14 (3), 1950, pp. 81−91.
Hilbert, D., and W. Ackermann: Grundzüge der theoretischen Logik. Springer, 1938.
Scholz, H., and G. Hasenjaeger: Grundzüge der mathematischen Logik. Springer, 1961.
Shapiro, S.: Foundations without foundationalism: a case for second-order logic. Oxford University Press, 1991.
Väänänen, J. A.: Second-order and higher-order logic. Stanford Encyclopedia of Philosophy. August, 2019.

Juan Miguel Lopez Munive. A defense of proof-theoretic logical pluralism

Abstract: Dicher (2016) argues that a crucial element of Restall’s (2014) proof-theoretic defense of meaning-invariant logical pluralism is mistaken, namely: the sameness claim. According to this claim, inference rules that differ only structurally are identical. In this talk, my aim is to defend Restall’s proof-theoretic pluralism by showing that Dicher’s argument is unsound. To do this I apply Mares’ and Paoli’s (2014) renewal of Avron’s (1988) distinction between internal and external consequence relation and argue that the sameness claim is to be understood as holding at the level of the former. Additionally, I defend that Dicher’s purported counterexample to the sameness claim does not concern the structure of the internal consequence relations of the rules he considers. Consequently, Restall’s proof-theoretic pluralism manages to avoid Dicher’s objection.

Pedro Pinto. A generalization via proof mining methods

Abstract: Recently, an iterative method for approximating common fixed points of two nonexpansive maps was introduced. This method alternates between the well-known Halpern-type and Mann-type definitions, and was thus dubbed the alternating Halpern-Mann iteration (HM). In [1], the (HM) method was studied in the setting of CAT(0) spaces, and asymptotic regularity and strong convergence were established. If one restricts oneself to Hilbert spaces, the proof follows standard arguments. Such arguments are not available in the nonlinear setting of CAT(0) spaces and the use of logical tools seem to be necessary.
In this talk, we will discuss the role of logical tools in obtaining this result, namely via the application of a general macro developed in [2] for the elimination of certain weak compactness arguments in the context of the proof mining program.

[1] B. Dinis, and P. Pinto, Strong convergence for the alternating Halpern-Mann iteration in CAT(0) spaces, arXiv:2112.14525 (Submitted), 2021.
[2] F. Ferreira, L. Leuștean, and P. Pinto, On the removal of weak compactness arguments in proof mining, Advances in Mathematics, 354:106728 (55pp), 2019.
[3] L. Leustean, and P. Pinto, Rates of asymptotic regularity for the alternating Halpern-Mann iteration, arXiv:2206.02226 (Submitted), 2022.
[4] H. Cheval, and L. Leuștean, Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration, Optimization Methods and Software, 2022.
[5] H. Cheval, U. Kohlenbach, and L. Leuștean, On modied Halpern and Tikhonov-Mann iterations, arXiv:2203.11003 (Submitted), 2022.
[6] U. Kohlenbach, and L. Leuștean, Eective metastability of Halpern iterates in CAT(0) spaces, Advances in Mathematics, 231(5):2526-2556, 2012.
[7] K. Schade, and U. Kohlenbach, Effective metastability for modified Halpern iterations in CAT(0) spaces, Fixed Point Theory and Applications, 2012:191 (19pp), 2012.
[8] R. I. Boț, E. R. Csetnek, and D. Meier, Inducing strong convergence into the asymptotic behaviour of proximal splitting algorithms in Hilbert spaces, Optimization Methods and Software, 34(3):489-514, 2019.

Bernhard Fisseni, Deniz Sarikaya and Bernhard Schröder. Recent Advances in Frame Modelling of Mathematical Proofs

Abstract: The frame concept, developed in Artificial Intelligence, cognitive science and linguistics, has recently regained interest in philosophy and philosophy of science. There have also been attempts at modelling mathematical proofs using frames, starting from a distinction between structural frames, which capture expectations about proof methods as well as constituents of proofs and their relations, and ontological frames, which capture the mathematical structures and typical referring linguistic and formulaic expressions.

We will illustrate two points about using frames to model mathematical proofs: First, how frames can be used to explain aspects of innovation in mathematics, e.g. the discovery of zero or the transfer between different subject areas. Secondly, how frame theory relates to concepts of understanding proofs, notably Avigad’s (2008) theory.

Joost Joosten. A decidable fragment of the Quantified Provability Logic of Heyting Arithmetic

Abstract: We present a nested-implication free fragment of quantified modal logic, called QRC1, that we show to be sound and complete for Heyting Arithmetic. The only allowed modality is the diamond which is to be interpreted as consistency. Our results are obtained by importing earlier results on QRC1 for Peano Arithmetic to the setting of Heyting Arithmetic using well-known conservativity results and proving that we always stay in the required complexity classes during our Solovay construction. In addition we make some observations on properties of QRC1 including interpolation and fixpoints. We close off by showing that QRC1 also defines a fragment of True Quantified Provability Logic of Heyting Arithmetic (and Peano Arithmetic). The latter shows — using results of Montagna, Artemov and Vardanyan— that going from the full logic to the fragment supposes a jump from non-arithmetical to decidable.

This is joint work with Ana Borges de Almeida, Dick de Jongh and Albert Visser.

José Antonio Pérez Escobar and Deniz Sarikaya. Purifying applied mathematics and applying pure mathematics: how a late Wittgensteinian perspective sheds light onto the dichotomy

Abstract: In this work we argue that there is no strong demarcation between pure and applied mathematics. We show this first by stressing non-deductive components within pure mathematics, like axiomatization and theory-building in general. We also stress the “purer” components of applied mathematics, like the theory of the models that are concerned with practical purposes. We further show that some mathematical theories can be viewed through either a pure or applied lens. These different lenses are tied to different communities, which endorse different evaluative standards for theories. We evaluate the distinction between pure and applied mathematics from a late Wittgensteinian perspective. We note that the classical exegesis of the later Wittgenstein’s philosophy of mathematics, due to Maddy, leads to a clear-cut but misguided demarcation. We then turn our attention to a more niche interpretation of Wittgenstein by Dawson, which captures aspects of the aforementioned distinction more accurately. Building on this newer, maverick interpretation of the later Wittgenstein’s philosophy of mathematics, and endorsing an extended notion of meaning as use which includes social, mundane uses, we elaborate a fuzzy, but more realistic, demarcation. This demarcation, relying on family resemblance, is based on how direct and intended technical applications are, the kind of evaluative standards featured, and the range of rhetorical purposes at stake.

Bernd Buldt. On Visser’s move on G2

Abstract: There is a long-running debate on Gödel’s second incompleteness theorem (G2: the unprovability of consistency) that began in the late 1950s when it became clear that any uncritical formulation of the theorem will suffer counterexamples (the so-called intensionality of G2). The discussion itself and suggestions for how to amend the situation have been dominated by Kreisel’s request to find a `canonical representation’ of mathematical theories and their notions of provability in order to dodge the specter of intensionality. Recently, Albert Visser injected a fresh, new idea into the discussion by suggesting that we should conceive of “the second incompleteness theorem, not as a statement concerning the relation of a theory and a sentence [i.e, the unprovable consistency statement], but concerning the relation between two theories” (Visser16, p.~0; emphasis in the original). In the talk I will discuss Visser’s move against the backdrop of the previous discussion and try to asses its promise and some of the challenges it faces.