[logic-ml] Talk by Yoriyuki Yamagata (6 Oct 11:00-)

[Tetsuya Sato]

京都大学数理解析研究所の佐藤です。

10月6日11:00から、産業技術総合研究所の山形頼之氏に
以下の講演をしていただくことになりましたので、
ご連絡いたします。どうぞお気軽にお越しください。
==========
Time:	11:00-12:00, 6 Oct, 2016
Place:	Rm 478, Research Building 2, Main Campus, Kyoto University
	京都大学 本部構内 総合研究2号館 4階478号室
	http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)
	http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)

Speaker: Yoriyuki Yamagata (National Institute of Advanced Industrial
Science and Technology)
(Website: http://staff.aist.go.jp/yoriyuki.yamagata/en/)

Title:	Consistency proof of an arithmetic with substitution inside a
bounded arithmetic

Abstract:
Bounded arithmetics are systems of arithmetic in which induction
is restricted to bounded formulas.  Bounded formulas are formulas
in which all quantifiers are bounded by some terms.
Among many such systems, Buss's hierarchy of bounded arithmetics
have particular interest, because their provably total functions
exactly correspond polynomial-time hierarchy.

A major open problem on bounded arithmetics is whether Buss's
hierarchy collapses or not.  If it collapses, for example, it
implies P=NP.  One strategy to differentiate the hierarchy is
to use Gödel sentence of some theories. In this talk, we
consider a theory PV by Cook and Urquhart and its restrictions.
PV is an equational system, which has roughly the same strength
to Buss's S12.   Beckmann proved that when induction and
substitution are removed from PV, the consistency of the system
can be proved by S12.  On the other hand,  Buss and
Ignjatović proved that S12 cannot prove the consistency
of the system which obtained by removing just induction, but
adding propositional logic and BASIC axioms, from PV.

In this talk, we improve the Beckmann by proving that S22 can
prove the consistency of the system which obtained by removing
just induction from PV.  By delineating bounded arithmetics
which can prove consistency of various restrictions of PV,
we hope to prove non-collapse of Buss's hierarchy, and
relatedly, polynomial-time hierarchy.