3 papers
math.LO2024
Games with backtracking options corresponding to the ordinal analysis of
Eitetsu Ken
We give another proof of ordinal analysis of -fragments of Peano Arithmetic which is free from cut-elimination of -logic. Our main tool is a direct witnessing argument u…
math.LO2024
Ajtai's theorem for and pebble games with backtracking
Eitetsu Ken, Mykyta Narusevych
We introduce a pebble game extended by backtracking options for one of the two players (called Prover) and reduce the provability of the pigeonhole principle for a generic predicat…
cs.LO2023
On matrix rank function over bounded arithmetics
Eitetsu Ken, Satoru Kuroda
In [Mulmuley, 1987], Mulmuley gave an algorithm reducing the computation of the matrix rank function to that of determinants, of which the proof for the verification is elementary.…