17 found
Order:
Disambiguations
L. Gordeev [16]Lev Gordeev [5]Lew Gordeev [2]
  1.  36
    Proof Compression and NP Versus PSPACE.L. Gordeev & E. H. Haeusler - 2019 - Studia Logica 107 (1):53-83.
    We show that arbitrary tautologies of Johansson’s minimal propositional logic are provable by “small” polynomial-size dag-like natural deductions in Prawitz’s system for minimal propositional logic. These “small” deductions arise from standard “large” tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying geometric idea: if the height, h(∂), and the total number of distinct formulas, ϕ(∂), of a given tree-like deduction ∂ of a minimal (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  2.  18
    Proof Compression and NP Versus PSPACE II.Lew Gordeev & Edward Hermann Haeusler - 2020 - Bulletin of the Section of Logic 49 (3):213-230.
    We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in the weight of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  14
    Proof-Theoretical Analysis: Weak Systems of Functions and Classes.L. Gordeev - 1988 - Annals of Pure and Applied Logic 38 (1):1-121.
  4. On Cut Elimination in the Presence of Perice Rule.Lev Gordeev - 1987 - Archive for Mathematical Logic 26 (1):147-164.
     
    Export citation  
     
    Bookmark   5 citations  
  5.  20
    Generalizations of the One-Dimensional Version of the Kruskal-Friedman Theorems.L. Gordeev - 1989 - Journal of Symbolic Logic 54 (1):100-121.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  6.  24
    Phase Transitions of Iterated Higman-Style Well-Partial-Orderings.Lev Gordeev & Andreas Weiermann - 2012 - Archive for Mathematical Logic 51 (1-2):127-161.
    We elaborate Weiermann-style phase transitions for well-partial-orderings (wpo) determined by iterated finite sequences under Higman-Friedman style embedding with Gordeev’s symmetric gap condition. For every d-times iterated wpo ${\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d}\right)}$ in question, d > 1, we fix a natural extension of Peano Arithmetic, ${T \supseteq \sf{PA}}$ , that proves the corresponding second-order sentence ${\sf{WPO}\left({\rm S}{\textsc{eq}}^{d}, \trianglelefteq _{d}\right) }$ . Having this we consider the following parametrized first-order slow well-partial-ordering sentence ${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d}, r\right):}$ $$\left( \forall K > 0 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  14
    Systems of Iterated Projective Ordinal Notations and Combinatorial Statements About Binary Labeled Trees.L. Gordeev - 1989 - Archive for Mathematical Logic 29 (1):29-46.
    We introduce the appropriate iterated version of the system of ordinal notations from [G1] whose order type is the familiar Howard ordinal. As in [G1], our ordinal notations are partly inspired by the ideas from [P] where certain crucial properties of the traditional Munich' ordinal notations are isolated and used in the cut-elimination proofs. As compared to the corresponding “impredicative” Munich' ordinal notations (see e.g. [B1, B2, J, Sch1, Sch2, BSch]), our ordinal notations arearbitrary terms in the appropriate simple term (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8.  26
    Generalizations of the Kruskal-Friedman Theorems.L. Gordeev - 1990 - Journal of Symbolic Logic 55 (1):157-181.
    Kruskal proved that finite trees are well-quasi-ordered by hom(e)omorphic embeddability. Friedman observed that this statement is not provable in predicative analysis. Friedman also proposed (see in [Simpson]) some stronger variants of the Kruskal theorem dealing with finite labeled trees under home(e)omorphic embeddability with a certain gap-condition, where labels are arbitrary finite ordinals from a fixed initial segment of ω. The corresponding limit statement, expressing that for all initial segments of ω these labeled trees are well-quasi-ordered, is provable in Π 1 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  9.  14
    Proof-Theoretic Conservations of Weak Weak Intuitionistic Constructive Set Theories.Lev Gordeev - 2013 - Annals of Pure and Applied Logic 164 (12):1274-1292.
    The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set theories (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  21
    A Modified Sentence Unprovable in PA.L. Gordeev - 1994 - Journal of Symbolic Logic 59 (4):1154 - 1157.
  11.  26
    Masahiro Hamano and Mitsuhiro Okada. A Direct Independence Proof of Buchholz's Hydra Game on Finite Labeled Trees. Archive for Mathematical Logic, Vol. 37 No. 2 , Pp. 67–89. [REVIEW]Lev Gordeev - 2001 - Bulletin of Symbolic Logic 7 (4):534-535.
  12.  8
    Propositional Proof Compressions and DNF Logic.L. Gordeev, E. Haeusler & L. Pereira - 2011 - Logic Journal of the IGPL 19 (1):62-86.
    This paper is a continuation of dag-like proof compression research initiated in [9]. We investigate proof compression phenomenon in a particular, most transparent case of propositional DNF Logic. We define and analyze a very efficient semi-analytic sequent calculus SEQ*0 for propositional DNF. The efficiency is achieved by adding two special rules CQ and CS; the latter rule is a variant of the weakened substitution rule WS from [9], while the former one being specially designed for DNF sequents. We show that (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  21
    A Note on da Costa-Doria “Exotic Formalizations”.L. Gordeev - 2010 - Archive for Mathematical Logic 49 (7-8):813-821.
    We analyze N. C. A. da Costa and F. A. Doria’s “exotic formalization” of the conjecture P = NP [3–7]. For any standard axiomatic PA extension T and any number-theoretic sentence ${\varphi }$ , we let ${\varphi ^{\star} := \varphi \vee \lnot \mathsf{Con}\left( \mathsf{T}\right)}$ and prove the following “exotic” inferences 1–3. 1. ${\mathsf{T}+\varphi ^{\star}}$ is consistent, if so is T, 2. ${\mathsf{T}+\varphi}$ is consistent, provided that ${\mathsf{T}+\varphi ^{\star}}$ is ω-consistent, 3. ${\mathsf{T}+\varphi}$ is consistent, provided that T is consistent and has (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  14.  1
    Proof Compression and NP Versus PSPACE II: Addendum.Lew Gordeev & Edward Hermann Haeusler - 2022 - Bulletin of the Section of Logic 51 (2):197-205.
    In our previous work we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier’s cut-free sequent calculus for minimal logic with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction. In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea is to omit full minimal logic and compress only “naive” normal tree-like ND refutations of the existence of Hamiltonian cycles in given non-Hamiltonian graphs, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  15.  11
    Archive for Mathematical Logic. [REVIEW]Lev Gordeev - 2001 - Bulletin of Symbolic Logic 7 (4):534-535.
  16.  9
    Finite Methods in 1-Order Formalisms.L. Gordeev - 2001 - Annals of Pure and Applied Logic 113 (1-3):121-151.
    Familiar proof theoretical and especially automated deduction methods sometimes accept infinity where, in fact, it can be omitted. Our first example deals with the infinite supply of individual variables admitted in 1-order deductions, the second one deals with infinite-branching rules in sequent calculi with number-theoretical induction. The contents of Section 1 summarize and extend basic ideas and results published elsewhere, whereas basic ideas and results of Section 2 are exposed for the first time in the present paper. We consider classical (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  17.  1
    A Modified Sentence Unprovable in $Mathbf{PA}$.L. Gordeev - 1994 - Journal of Symbolic Logic 59 (4):1154-1157.