講演一覧

証明可能性論理Dのモデル拡張 

アブストラクト：「証明可能性」という概念の様相としての振る舞いを理解するために、証明可能性論理と呼ばれる様相論理がある。証明可能性論理の中でもよく研究されている様相論理としてGLがある。

GLの定理すべてと□(□φ∨□ψ)→□φ∨□ψ, ¬□⊥という論理式を公理として追加して得られる様相論理を D と呼ぶ(ただし推論規則は モーダス・ポネンス のみ)。Dもまた証明可能性論理である。

DのモデルはGLのモデルに「尻尾」と呼ばれる逆方向の無限遷移と「終端」と呼ばれる自分以外の全ての可能世界と関係づく世界を加えたものになっている。

Dの証明体系はヒルベルト流のみ与えられていたが、最近の研究(Kashima,Kurahashi,Iwata 2023)によってシークエント計算が導入された。本研究では、Dのモデルに対してさらに尻尾と終端を付け加えたモデルを考え、この意味で定義された論理とDとの差について考察した。 


局所反映原理における保存性

アブストラクト：理論の局所反映原理とは，理論の健全性の形式化であり，局所反映原理に関してBeklemishevの保存性定理が知られている．今回はBeklemishevの保存性定理の非標準的な証明可能性述語に基づく一般化を与える．さらにRosser 証明可能性述語をもとに保存性定理を分析して得られた結果を紹介する．本発表は神戸大学の倉橋太志氏との共同研究に基づく． 

講演資料


Structural Connection between Bidirectional Implications and Type-Raising

アブストラクト：Within the context of the CG natural deduction system, which is sensitive to the order and quantity of assumptions, we introduce two implications (←, →). We derive two rules from these additions: (a ← x) → a and a ← (x → a) from x. Our discussion revolves around the methodology to streamline the complexity of proof diagrams generated by these rules, reducing them to problems associated with higher-order unification. Through this reduction, we reorient the focus from termination judgments in proof search to termination judgments in unification, thereby enhancing the clarity of proof determination in this system.


Z定理のモジュール性

アブストラクト：一般に，書き換え系RとSのそれぞれで合流性が言えても，R∪Sが合流性を持つとは限らない．しかし，「RとSが可換である」という条件が加わると，Hindley-Rosenの補題よりR∪Sの合流性が言える．本研究では，合流性を示すための手法の１つであるZ定理のモジュール性に着目し，書き換え系RとSがそれぞれZ定理を満たす場合，さらにどのような条件が加われば R∪SのZ定理が成り立つかを明らかにする．また，ラムダ計算を具体例として取り上げ，モジュール性を使ったZ定理証明を行う． 


Existence Property for Negated Formulas in Intermediate Predicate Logics

アブストラクト：Existence and disjunction properties are regarded as the ``hallmarks'' of constructivity of logical systems such as intuitionistic logic.

In many cases, these properties appear together.

However, we observe that they come apart in intermediate predicate logics.

Of these two properties, we focus on existence property (EP) and consider its weaker variants including EP for negated formulas.

(This is an interim report of ongoing research of the author. 

講演資料


Epistemic possiblity in intuitionistic epistemic logic

アブストラクト：Artemov and Protopopescu defined an intuitionistic epistemic logic IEL to reason about intuitionistic knowledge. While classical knowledge implies classical truth, intuitionistic truth implies intuitionistic knowledge. We describe Artemov and Protopopescu's IEL and its BHK interpretation. We characterize epistemic possibility in IEL. 

講演資料


De Groot duality for represented spaces

アブストラクト：We explore de Groot duality in the setting of represented spaces. The de Groot dual of a space is the space of closures of its singletons, with the representation inherited from the hyperspace of closed subsets. This yields an elegant duality, in particular between Hausdorff spaces and compact T1-spaces. This is joint work with Arno Pauly (Swansea University) 


A refinement of the theory of quantum information over noisy quantum channels by algorithmic randomness

アブストラクト：The notion of probability plays a crucial role in quantum mechanics. It appears as the Born rule. In modern mathematics which describes quantum mechanics, however, probability theory means nothing other than measure theory, and therefore any operational characterization of the notion of probability is still missing in quantum mechanics. In our former works, based on the toolkit of algorithmic randomness, we presented an operational refinement of the Born rule, called the principle of typicality, for specifying the property of the results of quantum measurements in an operational way. Then, in a series of works, we have refined and reformulated quantum information theory presented in Nielsen and Chuang's textbook, "Quantum Computation and Quantum Information," based on the principle of typicality, in order to demonstrate how properly our framework works in practical problems in quantum mechanics. In this talk, we refine and reformulate the contents of Section 12.4 of the book based on the principle of typicality, with a focus on the refinement and reformulation of Maxwell's demon by algorithmic randomness in our framework. 


Models for GL

アブストラクト：In this talk, we discuss semantical properties of the logic GL of provability. The logic GL is a normal modal logic which is axiomatized by the the Löb formula. However, it is known that GL can also be axiomatized by an axiom □ p ⊃ □□ p and an ω-rule (♢∗) which takes countably many premises ϕ ⊃ ♢^{n} ⊤ (n ∈ ω) and returns a conclusion ϕ ⊃ ⊥. We show that the class of transitive Kripke frames which validates (♢∗) and the class of transitive Kripke frames which strongly validates (♢∗) are equal, and that the following three classes of transitive Kripke frames, the class which validates (♢∗), the class which weakly validates (♢∗), and the class which is defined by the Löb formula, are mutually different, while all of them characterize GL. This gives an example of a proof system P and a class C of Kripke frames such that P is sound and complete with respect to C but the soundness cannot be proved by simple induction on the height of the derivations in P. As a corollary, we show that the class of modal algebras which is defined by equations □ x ≤ □□ x and ∧_{n∈ω} ♢^{n} 1 = 0 is not a variety. 

講演資料


Determinacy of probabilistic omega-languages 

アブストラクト：Probabilistic automata is a natural extension of non-deterministic automata in which the non-determinism is replaced by a probability distribution. The accepted omega-languages of such automata not only depend on the acceptance condition, such as Büchi, but also the probability semantics. We study the determinacy of Gale-Stewart games whose winning sets are recognized by probabilistic automata with various acceptance condition under threshold probabilistic semantics. 


Tightness and related notions in fragments of Peano Arithmetic

アブストラクト：こちら

講演資料



Strong Solovay reducibility 


講演資料



Provability of matrix properties in formal theories of linear algebra 

アブストラクト：The proof complexity of linear algebra was initiated by the works of Soltys , Cook and Tzameret in which the provability of determinant identities in weak fragments were considered. In this talk, we will discuss the provability of properties of the determinant, the rank function and Pfaffian in fragments of bounded arithmetic as well as Soltys' systems of linear algebra. 



証明可能性論理 S の Curry-Howard 対応 

アブストラクト：証明可能性論理 S は Peano 算術における証明可能性を様相 □ として定式化した論理であり，Solovay (1976) により与えられた．この論理の特徴として必然化規則が成り立たず，正規な様相論理でないという点があげられる．本発表では S の natural deduction とその term calculus を与え，非正規性についてプログラムの観点から議論する． 



超算術的解析に属する選択公理の変種とωモデル反映による超算術的解析の近似

アブストラクト：超算術的解析（hyperarithmetic analysis）と呼ばれる二階算術の理論のクラスに関するトピックを二つ話す．はじめに超算術的解析に属する新たな選択公理の変種をいくつか紹介し，それらと既存の理論との含意関係を説明する．次にωモデル反映（ω-model reflection）を用いて定義される理論のクラスによって超算術的解析のクラスを近似する取り組みについて話す． 


講演資料



A Gentzen-style calculus for substructural logics with axioms W and S

アブストラクト：We discuss a Gentzen-style calculus for substructural logics with axioms related to both associativity and contraction such as W and S. 



Nested sequent calculi for modal logics

アブストラクト：We introduce a way to get nested sequent calculi for many modal logics (S4, S5, K + ◇^mA→□^n◇A, etc.). A feature of these calculi is easiness of syntactic cut-elimination. These calculi are closely related to Brunnler's nested sequent calculi and Negri's labelled sequent calculi. 



Negligible classes in computability theory and reverse mathematics 

アブストラクト：In their seminal work on algorithmic randomness, Zvonkin and Levin (implicitly) defined the concept of negligibility, where a class of reals C is said to be negligible if its Turing upper closure has Lebesgue measure 0 (or said otherwise, there is no probabilistic algorithm which generates a member of C with positive probability). We will illustrate this notion by exhibiting some natural examples of negligible classes and explain how negligibility can be generalized to prove non-implication results in reverse mathematics. This is joint work with Eric Astor, Damir Dzhafarov, Ludovic Patey, Chris Porter, Paul Shafer, Reed Solomon and Linda Brown Westrick. 


講演資料



Tableau Calculus for Undirected Graphs 

アブストラクト：An undirected graph can be assumed as a kind of Kripke frame that has irreflexivity and symmetry. In this presentation, we formulate the tableau calculus of the hybrid logic for undirected graphs. Our main result is to show the completeness and the termination property of the tableau method, which leads us to prove the decidability. * This is a joint work with Tsubasa Takagi (TITech). 



Uniform reductions in formal systems and a characterization of the Π^1_2 part of Π^1_1- CA_0. 

アブストラクト：Uniform reductions (Weihrauch reduction, arithmetical Weihrauch reduction) are ways to compare the complexity of two theorems according to computability theory.

In this talk, we consider uniform reductions in some axiomatic systems of second order arithmetic.

We will introduce a Pi^1_2-weakening of Pi^1_3 sentence which conserves uniform reductions over ACA_0 and show that our Pi^1_2-weakening of arithmetical Ramsey’s theorem for [\mathbb{N}]^{\mathbb{N}} characterizes the Π^1_2 part of Π^1_1- CA_0.



2階直観主義命題論理の解釈と決定可能性に関する考察 



Equivalences of Σ^0_2 determinacy among certain difference classes 

アブストラクト：Recently, Tanaka [1] proved that the determinacy hierarchy over the differences of the boldface Σ^0_2 sets collapses to that of Σ^0_2∧Π^0_2, by showing that the corresponding hierarchy of MID (Multiple Inductive Definitions) collapses to [Σ^1_1]^ 2 - ID with two Σ^1_1 operators (with parameters). Thereby, the following old question by T. Nemoto has been brought back to us: a transfinite iteration of Σ^1_1-ID can be deduced from the determinacy of Σ^0_2 (Conjecture 3.11, [2]). In fact, she [2] proved that a transfinite iteration of Σ1 1 -ID implies Sep(∆^0_2, Σ^0_2)-Det, and then even without showing the reversal, made a seemingly stronger conjecture. In this paper, we prove that the determinacy of Sep(∆^0_2, Σ^0_2) is equivalent to that of Σ^0_2, which answers Nemoto’s question half. However, a full form of transfinite iterations of Σ^1_1-ID seems to be properly stronger than them, which will be discussed in [3]. Notice that we only consider boldface assertions with set parameters.


[1] K. Tanaka, Collapsing the hierarchy of multiple inductive definitions?, unpublished notes, BIMSA, September 2023, 7 pages.

[2] T. Nemoto, Determinacy of Wadge classes in the Baire space and simple iteration of inductive definition, RIMS Kokyuroku1635 (2009) 121-133.

[3] K. Tanaka, K. Yoshii and W. Li, Reverse-mathematics and the determinacy hierarchy over the differences of Σ02 sets, in preparation (2023). 



Π^1_1-conservation and proof transformations about Ramsey's theorem for pairs

Ramsey's theorem for pairs is well studied in context of reverse mathematics. One of the streams is to pursue its first-order strength. Slaman and Yokoyama ([1]) showed that RT^2 + WKL_0 is Π^1_1-conservative extension of BΣ^0_3. In this talk we improve this result. We show that they have a polynomial time proof transformation. A basic idea is based on a work by Kołodziejczyk, Wong and Yokoyama ([2]).


[1] T. A. Slaman and K. Yokoyama. "The strength of Ramsey’s theorem for pairs and arbitrarily many colors." The Journal of Symbolic Logic 83.4 (2018): 1610-1617.

[2] L. A. Kołodziejczyk, T. L. Wong, and K. Yokoyama. "Ramsey’s theorem for pairs, collection, and proof size." Journal of Mathematical Logic (2023): 2350007. 


講演資料



A generalization of many-valued semantics and proof systems