Operations, Sets, and Types

Toshiyasu Arai — "Finitary analyses of regularities"
Let us report two results. Both are obtained through finitary analyses. First, a hydra game is introduced. The termination of the game is independent from the existence of a regular uncountable ordinal. Second, a fragment of the theory of positive inductive definitions is shown to be predicatively reducible. In the weak fragment, the transfinite induction axiom for the least fixed points is restricted to boolean combinations of positive formulas and single quantified formulas.

Kentaro Fujimoto — "Predicativity/Impredicativity and Compositionality/Non-compositionality"
A distinction is often made between theories of compositional truth and non-compositional truth. This distinction is sometimes considered to be fundamental in the axiomatic studies of truth, and some further claim that this distinction is closely related to the distinction of predicative and impredicative theories. In fact, compositional theories and non-compositional theories of truth show quite different behavior over arithmetic in a similar way that predicative and impredicative theories do, but it turns out their differences (partly) collapse when we adopt set theory as their base theory. In this talk, I will explain some of such phenomena in connection to related systems, and, if time permits, discuss some proof-theoretic bi-products of those results and further prospects of related research topics.

Hajime Ishihara — "A monad on the combinatory algebras"
There has been little investigation into structure of the category of models of combinatory logic and lambda-calculus, that is, combinatory algebras, as an algebraic structure so far. One reason is that there has not been any definite notion of a morphism between combinatory algebras, and therefore, of the category of combinatory algebras. We propose the notion of a combinatory morphism for the category of combinatory algebras, and construct a monad and a strong monad on the category.

Gerhard Jäger — "Opening - a short look at our Templeton Project"
In these introductory remarks I will present some central aspects and aims of our research project “The operational paradigm – its mathematical and philosophical frontiers”, supported by the John Templeton foundation. In particular, I will put it into the historical context and formulate a few conceptual questions, establishing some strategic guidelines of our work.

Joost Joosten — "A fine structure of reflection formulas revisited"
At the Logic Colloquium of 1978, Ulf R. Schmerl presented a paper [Schm79] on relations between various kinds of reflection formulas and iterations thereof. In this talk, we take this paper as a starting point and see how a modern presentation readily suggests generalizations and applications to proof theory and formal arithmetic.

[Schm79] U. R. Schmerl. A fine structure generated by reflection formulas over primitive recursive arithmetic. In Logic Colloquium ’78 (Mons, 1978), volume 97 of Stud. Logic Foundations Math., pages 335–350. North-Holland, Amsterdam, 1979.

Takako Nemoto — "Finitistically constructive Zermelo-Fraenkel set theory"
We define FCZF, finitistically constructive Zermelo-Fraenkel set theory, which
 (i) is classically equivalent to ZF minus Extensionality; and
 (ii) can be proved to be consistent in a finitistic way (i.e., in PRA);
by carefully choosing, among various classically equivalent formulations, an appropriate one for each axiom of ZF minus Extensionality. Here the absence of Extensionality is not a real defect in formalizing mathematical practice, because usually we manually define the equivalence relation for each mathematical structure (e.g., real numbers).
To prove (ii), we use a realizability interpretation of FCZF in an applicative theory of the strength of BΣ₁(exp), by modifying Aczel's type-theoretic interpretation of CZF [1] for the pure applicative setting. Here, the partiality of application is essential, for the empty set is represented as a totally undefined operator.
To give the lower bound, we embed BΣ₁(exp) by interpreting a natural number as a class of equinumerous hereditarily finite sets. The essence is our reflection-style formulation of the axiom of Infinity: the set of hereditarily finite sets, intended as the realm of finite objects to which even Brouwer agreed to apply LEM, reflects all the other axioms of FCZF. Especially, the reflection of subset collection guarantees the totality of exponentiation in arithmetic.

This is a joint work with Kentaro Sato. The speaker thanks Hajime Ihishara for suggesting to her the usage of Aczel's interpretation.

[1] Peter Aczel, The Type Theoretic Interpretation of Constructive Set Theory, In: Angus Macintyre, Leszek Pacholski and Jeff Paris, Editor(s), Studies in Logic and the Foundations of Mathematics, Elsevier, 1978, Volume 96, Pages 55-66.

Wolfram Pohlers — "Characteristic ordinals in generalized recursion theory and proof theory"
In generalized recursion theory there is a series of abstractly defined ordinals (GRT–ordinals) that are supposed to be characteristic for the recursion theoretic properties of abstract structures. In [1] we introduced the notion of the Π¹₁–ordinal of a countable abstract structure and showed that the GRT–ordinals of countable acceptable structures coincide with their Π¹₁–ordinal. In this talk we want to indicate that axiomatizations for countable acceptable structures possess characteristic ordinals which are counterparts of their GRT–ordinals and can be regarded as a measure for the performance of the axiomatization.

[1] W. Pohlers, Semi–formal calculi and their applications, Gentzen’s Centenary: The quest for consistency (R. Kahle and M. Rathjen, editors), Springer-Verlag, 2015, pp. 195–232.

Dieter Probst — "A modular ordinal analysis"
Consider e.g. the theory ACA₀ and a corresponding infinitary system ACA^*₀ which extends PA^* by set induction and axioms ∃X[X = {x : A(x)}] for each arithmetical A without free number variables. We say that a normal function f : Ord → Ord describes ACA₀, if
 (i) ACA^*₀ ⊢_*^<γ Γ ⇒ PA^* ⊢_*^<f(γ) Γ, (Γ a finite set of arithmetical L^*₂-formulas),
 (ii) ACA₀ ⊢ TI_◃(C_ACA0,α) → Wo_◃(f(α)), where C_ACA0 is a suitable class.
As ACA₀ ⊢ Γ entails ACA₀^* ⊢_*^<ω Γ, (i) yields PA^* ⊢_*^<f(ω) Γ, and as for each n ∈ ℕ, ACA₀ ⊢ TI_◃(C_ACA0,n), (ii) implies ACA₀ ⊢ Wo_◃(f(n)), hence |ACA₀| = f(ω). For instance, a normal function f with f(ω(1+α)) = ε_α describes ACA₀.
We discuss how to find describing functions of successively stronger theories that are obtained by iteratively applying operations to theories for which we have already found describing functions. For each n ∈ ℕ, we denote by p_n+1 the operation which maps a theory T to the theory p_n+1(T) whose main axiom claims Π¹_n+1-reflection on ω-models of T. We present type-n+2 functionals It_n+1, so that the function It_n+1(It_n(...(It₁(f)...) describes the theory p_n+1(ACA₀) in the above sense, provided f describes ACA₀.

Michael Rathjen — "On Feferman's second conjecture"
In addition to his conjecture about the indeterminacy of CH relative to semi-intuitionistic set theory, Feferman stated another conjecture concerning the relationship between two types of predicates in such set theories, namely that the collection of Δ₁ predicates and the collection of predicates for which the law of excluded middle holds should coincide. The talk will address this conjecture.

Timotej Rosebrock — "Recursion theory in applicative theories"
The basic theory of operations and numbers BON was introduced by Feferman and Jäger, similar to EON by Beeson and APP by Troelstra and van Dalen. These theories are defined over the logic of partial terms by Beeson. They are not sufficient to formalize recursion theory. Therefore, we introduce a truncation operator τ_N with
  • x ∈ N → τ_N(f,x) ≃ f(x),
  • x ∉ N → τ_N(f,x) ∉ N.
This means that τ_N(f) behaves as f on the natural numbers and that τ_N(f) applied to an object which is not a natural number cannot output a natural number. With the help of τ_N, we can formalize partial recursive functions.
In recursion theory, we have several equivalent notions of semi-decidability, namely the preimage of 0 under a partial recursive function, the projection of the preimage of 0 under a total recursive function, the domain of a partial recursive function, and the range of a partial recursive function. In the operational framework, we can show that not all are equivalent anymore. In the talk we present which equivalences are provable and for which we have a countermodel.

This is a joint work with Gerhard Jäger and Kentaro Sato.

Sam Sanders — "A predicativist chimera originating from Nonstandard Analysis"
I will introduce *the special fan functional* and discuss its ’non-standard' properties as follows: Firstly, the special fan functional is easily computed from the intuitionistic fan functional (hence its name), and its existence thus carries the same first-order strength as WKL₀. Secondly, the special fan functional cannot be computed (Kleene S1-S9) from the Suslin functional but can be computed from (3E), i.e. full second-order comprehension. Thus, the special fan functional is an object of predicativist mathematics, with no predicative way of computing it. While the special fan functional does not involve Nonstandard Analysis, it does have its origin there. In particular, the aforementioned non-computability result is a translation of the fact that the nonstandard axiom Transfer does not imply the nonstandard axiom Standard Part.

This is joint work with Dag Normann.

Kentaro Sato — "Tutorial Part I: Interpretability and Predicativity"
There have been various mathematics proposed: Logicism, Intuitionism, Predicativism, Finitism, Constructivism, Borelian mathematics, Platonism, etc., and also various formal systems to express them: Fregean system, Whitehead-Russel type theory, primitive recursive arithmetic, Peano arithmetic, second order arithmetic, Feferman's explicit methamtics, Martin-Löf type theory, Quine's new foundation, MacLane set theory, Zermelo set theory, Zermelo-Fraenkel set theory with and without choice, ZFC plus large cardinal axioms, etc.. The natural questions are:
  (i) which formal system can express (which part of) which mathematics and
  (ii) which formal system is consistent and which is not.
We could not mathematically answer these questions in the absolute sense, but we could do that in a relativized sense:
  (i') which system can simulate which system (Interpretability) and
  (ii') which system is consistent relative to which system (Relative Consistency).
Although inner model and forcing, the typical methods of establishing relative consistency in set theory, establish interpretability as well, in general interpretability is stronger than relative consistency.
After a general explanation of these notions, we will make use of them in the investigations on Predicativity in Feferman's sense and on operational theories (which include Feferman's explicit mathematics). The so-called inductive model construction, the typical way to interpret operational theories in other kinds of sysmtem, will be explained. In this example, one could see that interpretation can be said to be a (miniaturized) model construction.

Kentaro Sato — "Tutorial Part II: Double negation, forcing and realizability"
We continue the investigation on operational theories by means of the notions of interpretability and relative consistency. To interpret other kinds of systems in operational theories, we use three different kinds of interpretations: double negation translation, intuitionistic forcing, and realizability. From the perspective of a general theory of interpretation, these three are more complicated than inductive model construction (and than inner model method) in the sense that they do not preserve logical connectives. It is natural to allow such interpretations if intuitionistic theories are concerned, because the meaning of logical connectives in constructivism are said to differ from classical ones. Actually these interpretations are for intuitionistic ones by nature: intuitionistic forcing is a straightforward formalization of Kripke semantics; and realizability is that of BHK interpretation. Nonetheless, some combinations of these intuitionistic interpretations have been used to establish interpretability between classical theories: forcing method in set theory is a composition of double negation translation and intuitionistic forcing, and Krivine's classical realizability is a composition of double negation translation and realizability. We will use a composition of all the three to construct a family of interpretations in operational theories. The essnetial feature is that operational theories can naturally formalize BHK interpretation. Another use of the composition of the three intuitionistic interpretations may also be mentioned.

Anton Setzer — "The Role of the Coinduction Hypothesis in Coinductive Proofs"
When carrying out proofs by induction, we follow schemata of inductive proofs rather than arguing that the set of natural numbers is the least set closed under 0 and successor. So for proving ∀x.φ(x), we usually don't define A := {x ∈ ℕ | φ(x)} and show that it is closed under 0 and successor, but use the principle of induction. Although using A and the principle of induction amount essentially to the same, using the induction principle is much easier to use and to teach.
When carrying out proofs by coinduction, one usually argues similarly as to proving the closure of the set A as above. For instance for carrying out proofs of bisimulation, one usually introduces a relation and shows that it is a bisimulation relation. This makes proofs by coinduction cumbersome and difficult to teach.
In this talk we develop schemata for reasoning coinductively which are similar to those used for inductive proofs. Proofs will make use of the coinduction hypothesis, where certain restrictions on its use need to be observed.
The use of the coinduction hypothesis is facilitated by the fact that we will define coinductive sets not as largest sets closed under constructors, i.e. by their introduction rules, but as largest sets allowing observations, i.e. by their elimination rules. For instance the set Stream of streams of natural numbers is the largest set allowing observations head : Stream → ℕ and tail : Stream → Stream.
The schemata we introduce will be schemata for corecursive definitions of functions, for coinductive proofs of equalities on coinductively defined sets, and coinductive proofs of coinductively defined relations. A special case of the latter is the proof of bisimulation on labelled transition systems. We will give examples on how to carry out such kind of coinductive proofs.

Silvia Steila — "From equivalent forms of CH to CH-systems"
The Continuum Hypothesis (CH) enjoys a great variety of equivalent forms. In 2012 Törnquist and Weiss showed that the Σ¹₂-definable version of several equivalent forms of CH turns out to be equivalent to ℝ ⊆ L. The arguments involved to prove such equivalences (both the ones with CH and the ones with ℝ ⊆ L) are usually different. Here we introduce CH-systems to the aim of "uniformizing" such proofs.

(Part of this is an on-going work with Raphaël Carroy and Alessandro Andretta.)

Stan Wainer — "Goodstein in Ackermann"
The slow-growing function G_x collapses the Veblen-Bachmann hierarchy of normal functions below the Howard ordinal, onto a parameterized-at-x extension of the Ackermann hierarchy below ε₀. As Arai noted, this opens up the possibility of devising Goodstein-type independence results for a range of theories both below and beyond PA; e.g. Σ¹₁-DC₀, ATR₀, ID₁. We show how it works.

Joint work with T. Arai and A. Weiermann.

Jan Walker — "Finitist Truth and Reflection"
Take as a starting point the hypothesis that, if one accepts a theory about a given subject matter, then one implicitly commits oneself to the (reflection) principle that whatever is provable in the theory is true with respect to that subject matter. To make this implicit commitment explicit in the language of the theory itself, the latter has to provide the means to express the property of being true in a principled way. In this talk, I will assume that the language of the theory comprises a primitive truth predicate and that the theory is equipped with destined axioms for the truth predicate. My focus will be on how to set up reasonable axioms of truth and account for one’s commitment to reflection principles if these questions are considered against the background of a finitist theory of arithmetic.

Sean Walsh — "The Strength of Abstraction with Predicative Comprehension"
Frege's theorem says that second-order Peano arithmetic is interpretable in Hume's Principle and full impredicative comprehension. Hume's Principle is one example of an abstraction principle, while another paradigmatic example is Basic Law V from Frege's Grundgesetze. In this talk we look at the strength of abstraction principles in the presence of predicative restrictions on the comprehension schema, and in particular we study a predicative Fregean theory which contains all the abstraction principles whose underlying equivalence relations can be proven to be equivalence relations in a weak background second-order logic. We show that this predicative Fregean theory interprets second-order Peano arithmetic.