「判断とは何か?」, 「導出(証明)とは何か?」という問に対して, to-assert-is-to-prove という立場のもとでの解答を与える理論を提示する.
1995年に竹内は論理的必然性の様相論理の意味論を提案した. 本研究では, その論理の演繹的体系を提示する.
みかけ上は区別がつかないボールが N>2 個与えられている. そのうち一個だけが, 他のボールと重さが異なっている. 天秤を使ってそのボールを特定し, かつ軽いか重いかも検出せよ. ただし天秤の使用回数は高々 n 回までとする. これがよく知られたアインシュタインボールパズル(EBP)である. N=12, n=3の場合が典型的な例である.
Bounded Arithmetic において不完全性定理とフォーシングの組み合わせについて検討する.
We present a Kripke semantics for the predicate extension of the minimum orthologic. We also discuss an embedding of this logic into the predicate extension of the modal logic KTB.
We introduce the class of intermediate infinitary logics and show its basic properties. In particular, we will show the existence of infinitary many Kripke incomplete intermediate infinitary logics.
昨年の SLACS で発表した「β変換の標準化定理の簡単な証明」をβη変 換へ拡張する.
多相型体系では, ML型体系のような意味での principal type は存在しないことが知られている. この発表では, bound quantifier を拡張して conditional type と呼ぶ新しい型を提案する. この型を用いると多相型体系においても, 次のような意味の principal type が表現できることを示す. すなわち, 任意の式 M について, ある conditional type σが存在して, M が型τをもつこととσがτの subtype であることが同値.
実数の黄金表記とは黄金比 b を基数とした2進列による表記である. 本発表では, b + b*b =1 であるからその列には 011 が現われないと仮定できることを指摘し, そのような列はノイズのある serial 回線で受信していてもビットの誤差を検査できることを指摘する. また, 黄金比の拡張として b + b^2 + b^3 + .. b^d=1 を満たす b を基数とする2進列表記に関しても, その誤り検出可能性の能力をエントロピーを用いて考察する.
To fill the gap between mathematical proofs and proofs in mathematical logic, we introduce a (semi-formal) proof system and discuss its properties.