Carregant...
Tipus de document
Treball de fi de màsterData de publicació
Llicència de publicació
Si us plau utilitzeu sempre aquest identificador per citar o enllaçar aquest document: https://hdl.handle.net/2445/215386
Interactive Proofs in Bounded Arithmetics
Títol de la revista
Autors
Director/Tutor
ISSN de la revista
Títol del volum
Recurs relacionat
Resum
Previous work [3] has shown that V02, the theory of bounded arithmetic in Buss’ Language equipped with comprehension for boundedly definable sets, is consistent with the conjecture NEXP ⊈ P/poly. That work entertains two diferent formalizations of the inclusion NEXP ⊆ P/poly inside V02, termed α and β. Both formalizations are provably equivalent in the standard model of arithmetic, by invoking the Easy Witness Lemma (EWL), a technically deep modern result in complexity theory. While the implication β → α is provable in V02, it is open whether V02 proves the converse implication α → β. Since this converse implication can be interpreted as a formalization of the EWL, whether V02 proves the equivalence of the two formalizations amounts to whether V02 proves (this formalizationof) the EWL.
In the present work, we make progress towards resolving this question in the positive. More concretely, we show that V02+α does prove a suitable formalization of IP = PSPACE, which is a central ingredient in the proof of the EWL. In the process of doing so, we lay the foundations necessary to discuss exact counting of large sets and formalization of interactive proofs in V02 and other second-order bounded arithmetics.
Descripció
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2023-2024. Tutor: Albert Atserias
Matèries (anglès)
Citació
Citació
SOTO, Martín. Interactive Proofs in Bounded Arithmetics. [consulta: 31 de desembre de 2025]. [Disponible a: https://hdl.handle.net/2445/215386]