On the number of variables in undecidable superintuitionistic propositional calculi

Undecidable iterative propositional calculus

In this paper, we consider iterative propositional calculi, which are finite sets of propositional formulas together with the rules of modus ponens and weak substitution (when formula being substituted must be already inferred). We construct an undecidable iterative propositional calculus using axioms in 3 variables. Particulary, we show that the general problem of derivability for these calculi is undecidable.

Undecidable problems for propositional calculi with implication

In this article, we deal with propositional calculi over a signature containing the classical implication $\to$ with the rules of modus ponens and substitution. For these calculi we consider few recognizing problems such as recognizing derivations, extensions, completeness, and axiomatizations. The main result of this paper is to prove that the problem of recognizing extensions is undecidable for every propositional calculus, and the problems of recognizing axiomatizations and completeness are undecidable for propositional calculi containing the formula $x \to ( y \to x )$. As a corollary, the…

线性框架的超直觉谓词逻辑：含两个个体变元的不可判定性

Superintuitionistic predicate logics of linear frames: undecidability with two individual variables

该研究证明线性Kripke框架定义的超直觉谓词逻辑QLC的两变量片段不可判定，且相关序数框架逻辑非递归可枚举，通过改进铺砌问题描述方法和双标记技术实现仅用两变量的证明。

Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi

In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional calculus. Moreover, we prove the same for the following restriction of this problem: whether a given finite set of theorems of a fixed propositional calculus derives all theorems of this calculus. The…