2021年度のセミナー

• Venue: Online via zoom.

• Time: 13:15 - 15:00.

• Abstract: This talk introduces basic results around relative interpretability and partial conservativity, which are notions related to Gödel’s incompleteness theorem. Roughly speaking, for any theories T and U, we say that T is interpretable in U if a model of T is definable in that of U. For any theories T and U, we say that T is Γ-conservative over U if any T-provable Γ sentence is provable in U. We introduce the basic properties of relative interpretability and partial conservativity and their relationships. Also, we introduce the modal investigations of them.

• Venue: Online via zoom.

• Time: 13:15 - 15:00.

• Abstract: 直観主義有限型算術体系HA^ωとゲーデルのTの中間に位置する存在量化子と選言記号を言語に含まない直観主義有限型算術体系HA^ω_efを考え，それがmodified realizability解釈と否定翻訳の両者の健全性を証明するのに十分であり，さらに，modified realizability解釈及び否定翻訳に関して閉じている体系であることを示す．
  また，ゲーデルのTの代わりにHA^ω_efを用いれば，ゲーデル及びスペクターによるダイアレクティカ解釈を用いた算術の無矛盾性証明をmodified realizability解釈を用いて模倣できることを示す

• Venue: Complex A 802 (and online via zoom).

• Time: 13:15 - 15:00.

• Abstract: Fuzzy logic allows us to use abstract truth value, between 0 and 1.  It's expected to be a framework for models of preference or others like that. By generalizing the range of value, we can formalize various preference standard, for instance, nonlinear ones. In this talk, we will seek possibilities of such frameworks. Mainly from [1], reformulated by T. Yamazaki.

[1] Schmidt, G. : Relational Measures and Integration, In R. A. Schmidt (ed.): Relations and Kleene Algebra in Computer Science, 343-357, 2006, Springer-Verlag Berlin Heidelberg

• Venue: Complex A 802 (and online via zoom).

• Time: 13:15 - .

• Abstract: An operator Ⲅ : 2^ℕ→ 2^ℕ is monotone if it is monotone increasing with respect to the inclusion order.

Any monotone operator has the least fixed point Γ^⍵1(∅) and the largest fixed point Γ^⍵1(ℕ) .

In reverse mathematics, an operator is given as a formula φ(x,X), that is, we regard φ(x,X) as the operator X |→ {x: φ(x,X) }.

We mainly consider operators defined by arithmetical formulas. Then, it is well-known that the existence of the least fixed points for these operators is equivalent to 𝝥¹₁-CA₀ over RCA₀. On the other hand, Avigad proved that the existence of fixed points is equivalent to ATR₀ [1].

In this talk, I’ll consider those equivalences from the viewpoint of Weihrauch reducibility.

[1] Avigad, Jeremy. “On the relationship between ATR0 and.” The Journal of Symbolic Logic 61.3 (1996): 768-779.

• Venue: Complex A 802 (and online via zoom).

• Time: 14:00 - .

• Abstract: The Weihrauch degree of a binary relation on Baire space measures the power of uniform computation of a problem defined on Baire space. In the recent studies of Weihrauch degrees, it is seen that its structure resembles the structure of second-order arithmetic in the sense of reverse mathematics. In this study, we will introduce the “first-order part” of a Weihrauch degree by focusing on numerical consequences and try to measure the first-order strength of degrees. Then we see that the first-order parts of degrees of arithmetical problems form a hierarchy corresponding to Kirby-Paris hierarchy of first-order arithmetic, and those can be classified with their first-order strength. This is a joint work with Damir Dzhafarov and Reed Solomon.

• Venue: Online via zoom.

• Time: 13:15 -

• Abstract: See https://math.cs.kitami-it.ac.jp/~fuchino/tmp/tohoku-fuchino-2021-12-abst.html

• Venue: Online via zoom.

• Time: 13:15 - .

• Abstract: The Weihrauch degree of a binary relation on Baire space measures the power of uniform computation of a problem defined on Baire space. In the recent studies of Weihrauch degrees, it is seen that its structure resembles the structure of second-order arithmetic in the sense of reverse mathematics. In this study, we will introduce the “first-order part” of a Weihrauch degree by focusing on numerical consequences and try to measure the first-order strength of degrees. Then we see that the first-order parts of degrees of arithmetical problems form a hierarchy corresponding to Kirby-Paris hierarchy of first-order arithmetic, and those can be classified with their first-order strength. This is a joint work with Damir Dzhafarov and Reed Solomon.

• Venue: Online via zoom.

• Time: 17:00 - .

• Abstract: In this talk, we will discuss the logical strength of two principles, which we shall call RSg and RSpo, introduced in 1980 by Rival and Sands as trade-off versions of Ramsey’s Theorem for pairs. We will show that RSg, a principle concerning graphs, is equivalent to 𝖠𝖢𝖠_０over RCA₀, but also admits some variations that turn out to be equivalent to 𝖱𝖳²₂ . We will also be able to characterize the complexity of the solutions of computable instances of RSg, by importing results coming from the study of combinatorial problems in the Weihrauch lattice.

We then move to the study of RSpo, a principle concerning posets: we will see that it is equivalent to ADS plus some induction over RCA₀, but it also admits a generalization (which seems to be a genuinely new combinatorial result) equivalent to 𝖠𝖢𝖠_０ .

This is joint work with Marta Fiori Carones, Alberto Marcone, and Paul Shafer.

• Venue: Online via zoom.

• Time: 14:30 - 16:00.

• Abstract: In computability theory, priority arguments are a useful method to construct a computably enumerable sets. In recent discussions, we use trees of strategies for priority arguments. They can realize many types of priority arguments. In this talk, we will overview how to express the constructions and compare the proofs by trees with the ones by classical method.

[1] Lempp, Steffen. "Priority arguments in computability theory, model theory, and complexity theory." Lecture notes (2012).

• Venue: Online via zoom.

• Time: 13:15 - 15:00.

• Abstract: In this talk, we shall deal with a countably based Smyth complete quasi-metric space which is studied in [1] as a quasi-Polish space. We will see a game theoretic characterization of this space based on [1].

[1] De Brecht, Matthew. "Quasi-polish spaces." Annals of pure and applied logic 164.3 (2013): 356-381.

• Venue: Online via zoom.

• Time: 13:15 - 15:00.

• Abstract: In this presentation I will sketch a few results connecting determinacy and reflection principles in Second-Order Arithmetic. These results improve and generalize a result by Kołodjzieczyk and Michalewski. I will also comment about some existing results on reflection principles in Second-Order Arithmetic.

• Venue: Online via zoom.

• Time: 13:15 - 15:00.

• Abstract: In [1], Rüede introduced some new subsystems of second order arithmetic: transfinite dependent choices and ω-model reflections with specific properties. Also, he studied relationships between them. We will see his results and some related things.

[1]Christian Rüede. Transfinite dependent choice and ω-model reflection.The Journal of Symbolic Logic, 67(3):1153–1168, 2002.

• Venue: Complex A 802 (and online via zoom).

• Time: 13:00 - 15:00.

• Abstract: In the study of models of Peano (or first-order) arithmetic, there are many results on recursively saturated models and their automorphisms. Here, we apply such an argument to models of second-order arithmetic and see that any countable (recursively saturated) model (𝑀,𝘚) of 𝖶𝖪𝖫₀^* is isomorphic to its countable coded ⍵-submodel if Σ₁-induction fails in (𝑀,𝘚). From this result, we see some interesting but weird properties of 𝖶𝖪𝖫₀^* with the absence of Σ₁-induction such as the collapse of analytic hierarchy. This argument can also be applied to the reverse mathematical study of Ramsey's theorem for pairs (RT²₂), and we see some new relations between the computability-theoretic characterizations of RT²₂ and the famous open question on the first-order part of RT²₂ +RCA₀. This work is a part of a larger project joint with Marta Fiori Carones, Leszek Kolodziejczyk, Katarzyna Kowalik and Tin Lok Wong.

• Venue: Zoom.

• Date/Time: June 4, 2021 (Friday) / 13:00 - 15:00.

• Abstract: In this presentation I will present some problems related to the μ-calculus I am currently working on. One problem is about the relation between the alternation hierarchy and generalizations of the weak alternation hierarchy. The other problems relate to the formalization of the μ-calculus inside Second Order Arithmetic.

• Venue: Online via zoom.

• Date/Time: May 14, 2021 (Friday) / 13:00

• Abstract: It is known that the collection of closed sets of a complete separable compact metric space is again a complete separable compact metric space (a hyperspace). In this talk, we will see the correspondence between compact sets and the elements of hyperspaces in the framework of second order arithmetic.

• Venue: Online with zoom.

• Date/Time: May 7, 2021 (Friday) / 13:00

• Abstract: In [STY], Simpson/Tanaka/Yamazaki showed that Weak Koenig’s lemma (WKL) is conservative over RCA₀ with respect to the formulas of the form “ for all X there exists unique Y such that A(X, Y ) ”for arithmetical A. In this talk, we will simplify the forcing argument used in [STY] and show that similar conservation results hold over RCA^∗₀ plus IΣ⁰_n or BΣ⁰_n. Besides, we see the feasibility of those conservation results; namely, they are realized by polynomial proof-transformations. This is obtained by formalizing the forcing argument in terms of Avigad [A1,A2].

[STY] S. G. Simpson, K. Tanaka and T. Yamazaki. Some conservation results on weak Konig’s lemma. Ann. Pure Appl. Logic 118 (2002), 87-114. [A1] J. Avigad, Forcing in proof theory. Bull. Symbolic Logic 10 (2004), no. 3, 305-333. [A2] J. Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic. Ann. Pure Appl. Logic 82 (1996), no. 2.

• Venue: Online with zoom.

• Date/Time: April 30, 2021 (Friday) / 13:00 - 15:00.

• Abstract: One important usage of higher order operators is to compute realizers of formulas. Roughly speaking, a realizer is a witness. Usually, formulas are inductively defined. The complexity from this inductive definition invokes the necessity of complex operators. In this talk, we overview the concept and motivation of realizability from the viewpoint of constructive math. We then observe the usefulness of the higher order setting, comparing with the first order setting when we need.

• Venue: Complex A 802 (and online via zoom).

• Date/Time: April 16, 2021 (Friday) / 13:00 - 15:00.

• Abstract: SL(Sequencial Limit) and BW(Bolzano-Weierstrass) are two types of axioms of second order arithmetic introduced by Friedman. The relation between them and some other axioms were studied by Conidis. In this talk, I'll introduce some variations of them and their relation with SL and BW.