Title: High-order feedback computation
Venue: Complex A 803 (and online via zoom).
Time: 13:00-15:00.
Abstract: Feedback Turing machines are Turing machines which can query a halting oracle $h:\subseteq \omega\times\omega\to \{\downarrow,\uparrow\}$, which has information on the convergence or divergence of \emph{feedback} computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what if we iterate the feedback construction? We define $\alpha$th order feedback Turing machines for each computable ordinal $\alpha$ and describe the feedback semi-computable sets using inductive definitions and Gale--Stewart games.
Title: The Logic of Correct Models
Venue: Complex A 803 (and online via zoom).
Time: 13:00-15:00.
Abstract: We study the collection of valid formulas built from expressions of the form “\phi holds in all Sigma_n-correct models.” This is joint work with F. Pakhomov.
Title: Descriptive complexity in number theory and dynamics
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: Informally, a real number is normal in base b if in its b-ary expansion, all digits and blocks of digits occur as often as one would expect them to, uniformly at random. We will denote the set of numbers normal in base b by N (b). Kechris asked several questions involving descriptive complexity of sets of normal numbers. The first of these was resolved in 1994 when Ki and Linton proved that N (b) is Π0 3 -complete. Further questions were resolved by Becher, Heiber, and Slaman who showed that T∞ b=2 N (b) is Π0 3 -complete and that S∞ b=2 N (b) is Σ 04
complete. Many of the techniques used in these proofs can be used elsewhere. We will discuss recent results where similar techniques were applied to solve a problem of Sharkovsky and Sivak and a question of Kolyada, Misiurewicz, and Snoha. Furthermore, we will discuss a recent result where the set of numbers that are continued fraction normal, but not normal in any base b, was shown to be complete at the expected level of D2(Π0 3 ). An immediate corollary is that this set is uncountable, a result (due to Vandehey) only known previously assuming the generalized Riemann hypothesis.
Title: ML-randomnessとWWKL0のωモデルについて
Venue: Complex A 202 (and online via zoom).
Time: 15:00-16:30.
Abstract: WWKL0とWKL0のωモデルによる分離(Xiaokang Yu and Stephen G. Simpson)を, ML-randomnessを用いて説明します.
Title: 逆数学および計算可能性理論におけるラムゼイ型定理の研究
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: ラムゼイの定理は長きにわたり逆数学・計算可能性理論の研究の主要テーマのひとつであった. その研究成果として, ラムゼイ型と称されるラムゼイの定理のバリエーションである, 無限組み合わせ論の定理の分析も近年進展を見せている. 今回, ラムゼイ型定理のひとつであるTree Theoremについて, 逆数学および計算可能性理論の観点による分析を修論の内容を基に発表する. 具体的には, 逆数学はTT^1_{<\infty}と帰納法公理の関係について, 計算可能性理論はCTT^2_2の彩色とlow_2 basis theoremについて概説する.
Title: 証明可能性論理とその分類について
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: 証明可能性論理とは様相演算子$\Box$を「証明可能性」と解釈するような様相論理である．アルテモフやヴィッサーによるトレースという概念を用いた手法と，ベクレミシェフによるモデルを用いた手法により，証明可能性論理は4つの形の論理に分類されることが示されている．今回はその分類手法の概要を説明し，実際にその手法を用いて具体的な理論における証明可能性論理について調べた結果を紹介する．
Title: 証明可能性論理の多様総論理への拡張について
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: 命題論理の言語に 1 つの様相記号 P を加えたものが様相論理の言語であり, 無限個の様相記号を 加えたものが多様相論理の言語である. 様相論理の 1 つに GL があり, 様相記号を証明可能性述語と解釈 して得られるものである. GL の自然な多様相論理への拡張が GLP であり, クリプキ意味論を適切に経由することで, GL の算術的完全性の証明に用いられた Solovay の手法の拡張から, 多様相論理 GLP の算術的完全性が示される.
Title: ゲームの決定性に関する逆数学の再考
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: Σ2の差階層におけるゲーム決定性に関するこれまでの多くの結果と最近の階層崩壊について述べます．
Title: Subintuitionistic logicsの間の非可算濃度の論理の存在
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: Jankovは1968年に古典論理と直観主義論理の間に非可算濃度の論理の存在を示している. このJankovの結果は, その間に存在する論理の濃度が大きいという意味で, 古典論理と直観主義論理との間に大きな隔たりがあることを表現していると考えられる. Bezhanishvili-Colacito-de Jongは, 2020年に幾つかのsubminimal logics の間における非可算濃度の論理の存在を近傍意味論を用いて示した. この結果は, subintuitionistic logicsの間にも多くの大きな隔たりがあることを示唆している. 今回は2020年の結果を出した方法とは別の1974年のWro\’{n}skiによる代数的手法を工夫した方法を用いて, 上記の2020年の結果も含めて多くのsubintuitionistic logicsの間に非可算濃度の論理が存在することが分かったので, これを概説する.
Title: A few recent topics in reverse mathematics
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: In this talk, I will report on recent topics from the discussions at the Oberwalfach proof theory workshop this month and my current studies.
Title: Recent results in constructive reverse mathematics around WKL
Venue: Complex A 202 (and online via zoom).
Time: 15:00-16:30.
Abstract: Constructive reverse mathematics aims to characterize mathematical theorems with some combination of a fragment of choice axioms and logical principles. In this talk, we consider several variations of K\H{o}nig’s lemma and related principles and observe some examples of the following phenomena.
- Logical principle raises up the consistency strength of systems.
- Induction principles and choice principles act similarly.
Title: CTT^2_2 のインスタンスに対する low_2 解の構成について
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: ラムゼイの定理のバリエーションのひとつである tree theorem には, そのインスタン スに対する解の計算論的な複雑さにおいて, 幾つかのケースに対してラムゼイの定理と同様 の結果が得られることが知られている. 一方, ペアに対する tree theorem について, その弱い バージョンである cohesive tree theorem for pairs (CTT^2_2) においてすら, インスタンスに対 する low_2 解を構成するには, ラムゼイの定理の場合と異なる難しさが存在する. 今回は CTT^2_2 に関して, そのインスタンスの low_2 解の構成について概説する.
Title: 多様相論理 GLP, J の健全性と完全性
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: 多様相論理は様相記号が 2 個以上となるように拡張された様相論理であり, その中でも 通常の正規様相論理 GL と同様に健全性, 完全性を持つものを興味の対象としている. 中でも 多様相論理 GLP の算術的健全性・完全性について成立することが, Japaridze により示され, さらに Becklemishev によって簡略化された証明手法も確立されている. 今回は Becklemishev による多様相論理 J を経由した証明方法について紹介する.
Title: 証明可能性論理の分類
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: 理論 T の証明可能性述語を様相演算子 □ と解釈したときに，理論 U において証明可能 な様相論理式全体の集合を U における T の証明可能性論理という．ソロヴェイやヴィッサー により T = U のときの証明可能性論理は GL および GL{□n⊥} という形の論理で尽くされる ことが知られている．さらにベクレミシェフにより一般に証明可能性論理は α, β ⊆ ω（β は 補有限）について GLα，GL− β ，Dβ，Sβ という 4 つの形の論理に分類されることが示されて いる．今回はその分類方法について紹介する．
Title: Weihrauch and constructive reducibility between existence statements
Venue: Complex A 801 (and online via zoom).
Time: 16:00-17:30.
Abstract: We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical with the normal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas. In addition, we demonstrate that our meta-theorem is applicable to some concrete examples from Weihrauch and constructive reverse mathematics.
Title: How can an intuitionistic logician understand connexive constructible falsity?
Venue: Complex A 803 (and online via zoom).
Time: 15:00-16:30.
Abstract: Constructivists have usually understood negation as an implication to absurdity. Nonetheless, there have also been dissenting voices to this conception, one of the most notable among which are ones who advocate an alternative notion called constructible falsity. Nels David Nelson (1918-2003) introduced this notion as a `strong’ form of negation, which provides a direct counter-example to its negand. This `strongness’ is however often eschewed in favour of paraconsistency, making the resulting negation, severed of its relationship with intuitionistic negation, harder for intuitionistic logicians to comprehend. The issue is more serious in a variant of constructible falsity introduced by Heinrich Wansing, which validates so-called `connexive’ principles. This is due to the provability of a contradictory pair of formulas, which prohibits an interpretation of it as a `strong’ negation without bringing triviality. As a result, Wansingian negation should appear even more mysterious to the eyes of intuitionistic logicians. Another way to relate intuitionistic and Wansingian negations is to accept the law of excluded middle for the latter, as studied by Wansing and Hitoshi Omori. This move, however, compromises constructivity, and therefore is perhaps not so preferable either. In this talk, I will try to shed some lights on this issue, by discussing other ways to introduce an interaction between intuitionistic and Wansing negations. I will compare relative advantages of the interactions, which may enable intuitionistic logicians to better understand Wansingian negation and its connexivity.
Title: AND-OR木探索の乱択アルゴリズムとその均衡値
Venue: Complex A 801 (and online via zoom).
Time: 16:00-17:30.
Abstract: AND-OR木は同じ変数が1度のみ現れるようなブール関数の計算モデルであり、その計算コストは変数のクエリー回数によって定義される。本講演では主に乱択アルゴリズムを興味の対象とする。乱択アルゴリズムによるコスト均衡値、すなわち最小化された最悪計算量は、ランダムでないアルゴリズムのみを用いる場合に比べて真に小さくなることがSaksとWigderson(1986)により示されている。Saksらの手法をベースとして、最適な乱択アルゴリズムの一意性や、乱択アルゴリズムを深さ優先(depth-first)・一方向性(directional)などの条件で制限した場合の均衡値の大小関係について解説する。本研究の一部は鈴木登志雄氏との共同研究である。
Title: A constructive integration theory: a topological approach
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: We present a development of a constructive integration theory from a topological point of view, and constructively prove several convergence theorems in integration theory including Fatou’s lemma, and the monotone and dominated convergence theorems of Lebesgue in the totally topological framework.
Title: \Pi^1_1 conservation of Ramsey theorem for pairs over B\Sigma^0_2+WF(\epsilon_0).
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: Finding the first-order part of Ramsey theorem for pairs and two colors (RT^2_2) has been a long-standing question in the field of reverse mathematics. In their 2017 article, Chong, Slaman and Yang showed that RT^2_2 does not imply \Sigma_2 induction. We present here another proof of that result, by showing the \Pi^1_1 conservation of RT^2_2 over the base theory B\Sigma^0_2 + WF(\epsilon_0) where B\Sigma^0_2 denotes the bounded collection scheme for \Sigma_2 formulas and WF(\epsilon_0) the well-foundedness of the ordinal \epsilon_0.
The statement WF(\epsilon_0) is a strange base theory to consider, as it is at the same time a very strong assumption (not provable in ACA_0) but also quite weak (does not imply \Sigma_2 induction). Nevertheless, the well-foundedness of certain ordinals has been shown to be a robust and natural statement to study (see Kreuzer and Yokoyama 2013) and has already been used in various forms in the past to study Ramsey-like statements (see Chong, Slaman and Yang 2014).
This is a joint work with Ludovic Levy Patey and Keita Yokoyama.
Title: A \Pi^1_2 approximation of \Pi^1_1- CA_0.
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: In the typical study of reverse mathematics, theorems are classified into five levels: RCA_0, WKL_0, ACA_0, ATR_0 and \Pi^1_1-CA_0. On the other hand, recent studies of this area focus on the intermediate levels: theorems they are not equivalent to any of those five systems.
In this talk, we consider the intermediate structure between ATR_0 and \Pi^1_1-CA_0.
It is known that the gap of \Pi^1_1-CA_0 is very large.
More precisely, \Pi^1_1-CA_0 is not provable from any consistent \Pi^1_2 statement, and ATR_0 is axiomatizable by a \Pi^1_2 sentence.
Moreover, there are a lot of \Pi^1_2 statements provable from \Pi^1_1-CA_0 but stronger than ATR_0.
So a question arises: Can we clarify the structure of the \Pi^1_2 part of \Pi^1_1-CA_0? That is, is there a useful axiomatization of \Pi^1_2 part of \Pi^1_1-CA_0?
In this talk, we introduce a hierarchy of \Pi^1_2 statements such that it captures the \Pi^1_2 part of \Pi^1_1-CA_0. That is, any \Pi^1_2 statement provable from \Pi^1_1-CA_0 is already provable from one of the statements in the hierarchy.
Title: The Rival--Sands theorem for partial orders, ascending/descending sequences, and \Sigma_2 induction
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: In their 1980 article, Rival and Sands proved two theorems inspired by Ramsey’s theorem for pairs. The second of these theorems states that every infinite partial order P of finite width contains an infinite chain C with the property that every element of P is comparable either with no element of C or with infinitely many elements of C. We show that this theorem is equivalent to the ascending/descending sequence principle plus the \Sigma_2 induction scheme over RCA_0. This work is joint with Marta Fiori-Carones, Alberto Marcone, and Giovanni Soldà.
Title: A conservation result for RT^2 and B\Sigma^0_3.
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: It's well known that COH+D^2 is equivalent to RT^2 (over RCA_0). Some basis theorems for RT^2 are proved by this decomposition. Carrying out this proof within a model of WKL_0+B\Sigma^0_3, we can prove a conservation result. In this talk, we see a proof of \ll^2-basis theorem for D^2, using effective coded \omega-models of WKL_0. These discussions and results can give a new view point to conservation results, with help of a view point of some types of basis theorem. The contents are joint work with Keita Yokoyama.
References
[1] Hirschfeldt, Denis R. Slicing the truth: On the computable and reverse mathematics of combinatorial principles. 2015.
[2] Fiori-Carones, M., Kołodziejczyk, L. A., Wong, T. L., Yokoyama, K. "An isomorphism theorem for models of Weak Kőnig's Lemma without primitive recursion." (2022).
Title: The computability theoretic and reverse mathematical analysis of Ramsey's Theorem.
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: Ramsey's theorem has long occupied a central position in the study of reverse mathematics, and in particular, there has been much research on Ramsey's theorem for pairs : RT^2_2. In this talk, I will introduce the relationships between RT^2_2 and the basic systems of reverse mathematics from the viewpoint of computability and reverse mathematics, showing that every instance of RT22 has a low_2 solution.
Title: The game metatheorem.
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: We present a new metatheorem based on Ash and Kight’s original eta-system priority argument. The previous modification of Ash and Knight’s metatheorem by the author was more hands-on and slightly more general than the original. This new version is more abstract, less hands-on, less general, but much easier to apply. We will also mention a new topological version that is currently work in progress with Andrew Marks.
Title: Proof-theoretic linguistics: the formal approach to natural language.
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30.
Abstract: If we consider a sentence of our language as a sequence of symbols, we can see that this sequence is non-commutative, non-associative, and does not allow duplicates; which is a very weak system for manipulating symbol sequences. In this talk, we will treat formal languages as a substructural logic and clarify the relationship between structural rules and linguistic structure. Further, we also introduce recent research on the incremental processing of natural language in this field.
Title: On the embedding of Kripke models into Beth models
Venue: Complex A 801 (and online via zoom).
Time: 16:00-17:30.
Abstract: Kripke showed in [1] that first-order Kripke models can be embedded into first-order Beth models with constant domains by a sophisticated transformation.
Following [2, Chapter 13], we revisit the embedding from modern perspectives.
[1] S. A. Kripke, Semantical Analysis of Intuitionistic Logic I, Studies in Logic and the Foundations of Mathematics, Vol.40, pp. 92-130, 1965.
[2] A. S. Troelstra and D. van Dalen, Constructivism in Mathematics, Vol 2, Elsevier, 1988.
Title: Negation and modality in view of non-deterministic semantics
Venue: Complex A 801 (and online via zoom).
Time: 16:00-17:30.
Abstract: Non-deterministic semantics is a semantic framework systematically developed by Arnon Avron and Iddo Lev. One way of describing this semantics is that it generalizes a many-valued semantics. Generalization lies in the fact that the value of a complex formula is not determined uniquely by its subformulas, but instead there are several values that can be assigned. The aim of the talk is twofold. First we introduce the non-deterministic semantics without assuming any familiarity on the topic. Second, we discuss two related topics: (i) non-deterministic semantics for systems with *very* weak negation, and (ii) modal semantics *without* possible worlds.