[Proof Complexity] New Preprints

Amir Tabatabai amir.akbar at gmail.com
Mon Nov 27 16:38:05 CET 2017

Dear All,

I have recently posted some of my preprints on arxiv whose links are
attached in the following. Corrections, comments and suggestions are all



Briefly, the first three are my attempts to generalize Solovay's seminal
work on the provability logic of Peano arithmetic to provide a provability
interpretation for some modal systems such as K4, KD4 and S4 and hence a
formalization for the BHK interpretation via classical arithmetical proofs.
Then I lift the techniques to investigate the provability logics of
hierarchies of theories rather than just one theory.

The forth is on developing a method to transform any proof in arithmetical
theories to a sequence of computational reductions. This technique leads to
a combinatorial characterization of low complexity theorems (below \Pi^0_1)
of the theories of arithmetic.

The fifth is on providing a predicative formalization of the implication
constant and then function spaces via weaving the notion of time with the
usual formulations of the notion of space via topological spaces and
Grothendieck topoi. As a result, we first propose a topological semantics
for weak modal systems like K and K4, and topological and categorical
semantics for some sub-intuitionistic logics and then we will lift this
relationship to the higher structured level of Grothendieck topoi and modal
lambda calculi.

Best wishes,

More information about the Proof-Complexity mailing list