Ajtai's theorem for $T^2_2(R)$ and pebble games with backtracking

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Ken, Eitetsu, Narusevych, Mykyta
Format: Preprint
Publié: 2024
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866913620217036800
author Ken, Eitetsu
Narusevych, Mykyta
author_facet Ken, Eitetsu
Narusevych, Mykyta
contents 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 predicate $R$ in the bounded arithmetic $T^2_2(R)$ to the existence of a particular kind of winning strategy (called oblivious) for Prover in the game. While the unprovability of the said principle in $T^2_2(R)$ is an immediate consequence of a celebrated theorem of Ajtai (which deals with a stronger theory $T_2(R)$), up-to-date no methods working for $T^2_2(R)$ directly (in particular without switching lemma) are known. Although the full analysis of the introduced pebble game is left open, as a first step towards resolving it, we restrict ourselves to a simplified version of the game. In this case, Prover can use only two pebbles and move in an extremely oblivious way. Besides, a series of backtracks can be made only once during a play. Under these assumptions, we show that no strategy of Prover can be winning.
format Preprint
id arxiv_https___arxiv_org_abs_2406_10924
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Ajtai's theorem for $T^2_2(R)$ and pebble games with backtracking
Ken, Eitetsu
Narusevych, Mykyta
Logic
Logic in Computer Science
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 predicate $R$ in the bounded arithmetic $T^2_2(R)$ to the existence of a particular kind of winning strategy (called oblivious) for Prover in the game. While the unprovability of the said principle in $T^2_2(R)$ is an immediate consequence of a celebrated theorem of Ajtai (which deals with a stronger theory $T_2(R)$), up-to-date no methods working for $T^2_2(R)$ directly (in particular without switching lemma) are known. Although the full analysis of the introduced pebble game is left open, as a first step towards resolving it, we restrict ourselves to a simplified version of the game. In this case, Prover can use only two pebbles and move in an extremely oblivious way. Besides, a series of backtracks can be made only once during a play. Under these assumptions, we show that no strategy of Prover can be winning.
title Ajtai's theorem for $T^2_2(R)$ and pebble games with backtracking
topic Logic
Logic in Computer Science
url https://arxiv.org/abs/2406.10924