arXiv subjects

Grigori Mints

Publications and source records attributed to Grigori Mints.

3 recordsLinked to original sources

arXiv2012

Intuitionistic Existential Instantiation and Epsilon Symbol

A natural deduction system for intuitionistic predicate logic with existential \ instantiation rule presented here uses Hilbert's $\e$-symbol. It is conservative over intuitionistic predicate logic. We provide a completeness proof for a suitable Kripke semantics, sketch an approach to a normalization proof, survey related work and state some open problems. Our system extends intuitionistic systems with $\e$-symbol due to A. Dragalin and Sh. Maehara.

math.LO↗

arXiv2012

Failure of interpolation in the intuitionistic logic of constant domains

This paper shows that the interpolation theorem fails in the intuitionistic logic of constant domains. This result refutes two previously published claims that the interpolation property holds.

math.LO↗

arXiv2012

Cut-elimination for the mu-calculus with one variable

We establish syntactic cut-elimination for the one-variable fragment of the modal mu-calculus. Our method is based on a recent cut-elimination technique by Mints that makes use of Buchholz' Omega-rule.

cs.LO↗