Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userGlivenkos theorem, finite height, and local tabularity
54
0
0.0
(
0
)
Authors
Ilya B. Shapirovsky
Ask ChatGPT about the research
No Arabic abstract
Glivenkos theorem states that a formula is derivable in classical propositional logic $mathrm{CL}$ iff under the double negation it is derivable in intuitionistic propositional logic $mathrm{IL}$: $mathrm{CL}vdashvarphi$ iff $mathrm{IL}vdash eg egvarphi$. Its analog for the modal logics $mathrm{S5}$ and $mathrm{S4}$ states that $mathrm{S5}vdash varphi$ iff $mathrm{S4} vdash eg Box eg Box varphi$. In Kripke semantics, $mathrm{IL}$ is the logic of partial orders, and $mathrm{CL}$ is the logic of partial orders of height 1. Likewise, $mathrm{S4}$ is the logic of preorders, and $mathrm{S5}$ is the logic of equivalence relations, which are preorders of height 1. In this paper we generalize Glivenkos translation for logics of arbitrary finite height.
rate research
Read More
We study the computational complexity of satisfiability problems for classes of simple finite height (ortho)complemented modular lattices $L$. For single finite $L$, these problems are shown tobe $mc{NP}$-complete; for $L$ of height at least $3$, equivalent to a feasibility problem for the division ring associated with $L$. Moreover, it is shown that the equational theory of the class of subspace ortholattices as well as endomorphism *-rings (with pseudo-inversion) of finite dimensional Hilbert spaces is complete for the complement of the Boolean part of the nondeterministic Blum-Shub-Smale model of real computation without constants. This results extends to the category of finite dimensional Hilbert spaces, enriched by pseudo-inversion.
The Omitting Types Theorem in model theory and the Baire Category Theorem in topology are known to be closely linked. We examine the precise relation between these two theorems. Working with a general notion of logic we show that the classical Omitting Types Theorem holds for a logic if a certain associated topological space has all closed subspaces Baire. We also consider stronger Baire category conditions, and hence stronger Omitting Types Theorems, including a game version. We use examples of spaces previously studied in set-theoretic topology to produce abstract logics showing that the game Omitting Types statement is consistently not equivalent to the classical one.
We prove that any proof of a $forall Sigma^0_2$ sentence in the theory $mathrm{WKL}_0 + mathrm{RT}^2_2$ can be translated into a proof in $mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the proof in $mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the other hand, $mathrm{RT}^2_2$ has non-elementary speedup over the weaker base theory $mathrm{RCA}^*_0$ for proofs of $Sigma_1$ sentences. We also show that for $n ge 0$, proofs of $Pi_{n+2}$ sentences in $mathrm{B}Sigma_{n+1}+exp$ can be translated into proofs in $mathrm{I}Sigma_{n} + exp$ at polynomial cost. Moreover, the $Pi_{n+2}$-conservativity of $mathrm{B}Sigma_{n+1} + exp$ over $mathrm{I}Sigma_{n} + exp$ can be proved in $mathrm{PV}$, a fragment of bounded arithmetic corresponding to polynomial-time computation. For $n ge 1$, this answers a question of Clote, Hajek, and Paris.
Inspired by Ramseys theorem for pairs, Rival and Sands proved what we refer to as an inside/outside Ramsey theorem: every infinite graph $G$ contains an infinite subset $H$ such that every vertex of $G$ is adjacent to precisely none, one, or infinitely many vertices of $H$. We analyze the Rival-Sands theorem from the perspective of reverse mathematics and the Weihrauch degrees. In reverse mathematics, we find that the Rival-Sands theorem is equivalent to arithmetical comprehension and hence is stronger than Ramseys theorem for pairs. We also identify a weak form of the Rival-Sands theorem that is equivalent to Ramseys theorem for pairs. We turn to the Weihrauch degrees to give a finer analysis of the Rival-Sands theorems computational strength. We find that the Rival-Sands theorem is Weihrauch equivalent to the double jump of weak K{o}nigs lemma. We believe that the Rival-Sands theorem is the first natural theorem shown to exhibit exactly this strength. Furthermore, by combining our result with a result of Brattka and Rakotoniaina, we obtain that solving one instance of the Rival-Sands theorem exactly corresponds to simultaneously solving countably many instances of Ramseys theorem for pairs. Finally, we show that the uniform computational strength of the weak Rival-Sands theorem is weaker than that of Ramseys theorem for pairs by showing that a number of well-known consequences of Ramseys theorem for pairs do not Weihrauch reduce to the weak Rival-Sands theorem. We also address an apparent gap in the literature concerning the relationship between Weihrauch degrees corresponding to the ascending/descending sequence principle and the infinite pigeonhole principle.
We analyze the strength of Hellys selection theorem HST, which is the most important compactness theorem on the space of functions of bounded variation. For this we utilize a new representation of this space intermediate between $L_1$ and the Sobolev space W1,1, compatible with the, so called, weak* topology. We obtain that HST is instance-wise equivalent to the Bolzano-Weierstrass principle over RCA0. With this HST is equivalent to ACA0 over RCA0. A similar classification is obtained in the Weihrauch lattice.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
