Switch to: Citations

Add references

You must login to add references.
  1. Lifting independence results in bounded arithmetic.Mario Chiari & Jan Krajíček - 1999 - Archive for Mathematical Logic 38 (2):123-138.
    We investigate the problem how to lift the non - $\forall \Sigma^b_1(\alpha)$ - conservativity of $T^2_2(\alpha)$ over $S^2_2(\alpha)$ to the expected non - $\forall \Sigma^b_i(\alpha)$ - conservativity of $T^{i+1}_2(\alpha)$ over $S^{i+1}_2(\alpha)$ , for $i > 1$ . We give a non-trivial refinement of the “lifting method” developed in [4,8], and we prove a sufficient condition on a $\forall \Sigma^b_1(f)$ -consequence of $T_2(f)$ to yield the non-conservation result. Further we prove that Ramsey's theorem, a $\forall \Sigma^b_1(\alpha)$ - formula, is not provable (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Lower Bounds to the size of constant-depth propositional proofs.Jan Krajíček - 1994 - Journal of Symbolic Logic 59 (1):73-86.
    LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...)
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • Witnessing functions in bounded arithmetic and search problems.Mario Chiari & Jan Krajíček - 1998 - Journal of Symbolic Logic 63 (3):1095-1115.
    We investigate the possibility to characterize (multi) functions that are Σ b i -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T 2 in terms of natural search problems defined over polynomial-time structures. We obtain the following results: (1) A reformulation of known characterizations of (multi)functions that are Σ b 1 - and Σ b 2 -definable in the theories S 1 2 and T 1 2 . (2) New characterizations of (multi)functions that are (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations