Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · math/0409070

First-Order Intuitionistic Logic with Decidable Propositional Atoms

Alexander Sakharov
View original source ↗Read source document ↗Export metadata ↓

Abstract

Intuitionistic logic extended with decidable propositional atoms combines classical properties in its propositional part and intuitionistic properties for derivable formulas not containing propositional symbols. Sequent calculus is used as a framework for investigating this extension. Admissibility of cut is retained. Constrained Kripke structures are introduced for modeling intuitionistic logic with decidable propositional atoms. The extent of the disjunction and existence properties is investigated. The latest information about this research can be found at http://sakharov.net/median.html

Explore related subjects

math.GMmath.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Alexander Sakharov. 2005-05-08. First-Order Intuitionistic Logic with Decidable Propositional Atoms. https://arxiv.org/abs/math/0409070

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Irreducibility of the Cuboid Polynomial $P_{a,u}(t)$ via a Rank-Zero Elliptic Curve

In this paper we study the even monic degree-8 cuboid polynomial $P_{a,u}(t)$ introduced by R. A. Sharipov in the first-cuboid specialization of his cuboid equations. For nonzero integers $a,u$ with $u^2\neq a^2$ we prove that $P_{a,u}(t)$ is irreducible in $\mathbb{Z}[t]$ (equivalently, in $\mathbb{Q}[t]$), thus confirming Sharipov's irreducibility conjecture in this two-parameter case. Over $K=\mathbb{Q}(\sqrt2)$ we have a factorization $P_{a,u}(t)=H_-(t)H_+(t)$ into two conjugate quartics. We show that reducibility of either $H_\pm$ would force the discriminant of a certain quadratic in $S=t^2$ to be a square in $K$, which in turn implies (via $τ=(au/Δ)^2$, where $Δ=u^2-a^2$) the existence of a rational point $(y,v)\in\mathcal{C}(\mathbb{Q})$ on the genus-one quartic $\mathcal{C}: v^2=16y^4+136y^2+1$ with $y^2=τ$. We give an explicit isomorphism $\overline{\mathcal{C}}\simeq E$ with the elliptic curve $E: Y^2=X(X-8)(X-9)$, which has conductor $48$ and Mordell-Weil rank $0$. Enumerating $E(\mathbb{Q})$ and tracing back to $\mathcal{C}(\mathbb{Q})$ rules out the only possible values $τ\in\{0,1/4\}$, and hence excludes any further factorization of $H_\pm$ in $K[t]$. A quadratic Galois descent then yields the irreducibility of $P_{a,u}(t)$ over $\mathbb{Q}$ and $\mathbb{Z}$.

math.GM↗
arXiv2026

Irreducibility of the Cuboid Polynomial $Q_{p,q}(t)$ via the Rank-One Chabauty-Coleman Method

Let $Q_{p,q}(t)\in\mathbb{Z}[t]$ be Sharipov's even monic degree-$10$ second cuboid polynomial, with coprime positive integers $p\ne q$. We prove that $Q_{p,q}(t)$ is irreducible over $\mathbb{Q}$, and hence over $\mathbb{Z}$. More generally, the normalized associated quintic $P_s(x)$ and its composition $P_s(t^2)$ are irreducible over $\mathbb{Q}$ for every $s\in\mathbb{Q}\setminus\{0,\pm1\}$. The proof reduces linear and quadratic factors to rational points and horizontal conjugate pairs on one fixed genus-$2$ curve. A certified rank upper bound for its Jacobian, together with an exact divisor calculation, gives a rank-one annihilating differential at the prime $3$. For the quadratic-factor case, the symmetric coordinates of a horizontal pair lie on an explicit double cover of an elliptic quartic. All rational affine points on this model are $3$-adically integral and reduce to six smooth residue classes. The pulled-back differential is a unit in each class, proving that six displayed points form the complete list. Their coordinates exclude every admissible parameter. A negative real root of the irreducible quintic then supplies the additional degree argument required for irreducibility of the degree-$10$ polynomial. The rank computation and all exact arithmetic certificates are specified explicitly for reproduction.

math.GM↗