Abstract In this paper, we consider the logic ${\textsf{ITL}}^{e}$, a variant of intuitionistic linear temporal logic that is interpreted over the class of dynamic Kripke frames. These are bi-relational structures of the form $ \langle{W, \preccurlyeq , f}\rangle $ where $\preccurlyeq $ is a partial order on $W$ and $f: W \to W$ is a $\preccurlyeq $-monotone function. Our main result answers a question recently raised by Boudou et al. (2017, A decidable intuitionistic temporal logic. In Computer Science Logic 2017, pp. 14:1–14:17. Vol. 82 of LIPIcs) about axiomatizing this logic. We provide an axiomatization of ${\textsf{ITL}}^{e}$ and prove its strong completeness with respect to the class of all dynamic Kripke frames. The proposed axiomatization is infinitary; it has two derivation rules with countably many premises and one conclusion. It should be mentioned that ${\textsf{ITL}}^{e}$ is semantically non-compact, so no finitary proof system for this logic could be strongly complete.

First we define a new class of fuzzy Turing machines that we call Generalized Fuzzy Turing Machines. Our machines are equipped with rejecting states as well as accepting states. While we use a t-norm for computing degrees of accepting or rejecting paths, we use its dual t-conorm for computing the accepting or rejecting degrees of inputs. We naturally define when a generalized fuzzy Turing machine accepts or decides a fuzzy language. We prove that a fuzzy language L is decidable if and only if L and its complement are acceptable. Moreover, to each r.e. or co-r.e language L, we naturally correspond a fuzzy language which is acceptable by a generalized fuzzy Turing machine. A converse to this result is also proved. We also consider Atanasov's intuitionistic fuzzy languages and introduce a version of fuzzy Turing machine for studying their computability theoretic properties.

In this article, we study the two hierarchies of intuitionistic bounded arithmetic introduced by Buss and Harnik. Harnik's hierarchy contains the theory IS21 defined and studied by Cook and Urquhart as the first level. We prove level by level equivalence between the two hierarchies (for the first level, the fact was first proved by Cook and Urquhart using realizability and functional interpretation and later by Buss by an elementary method). Next we investigate the question of whether the hierarchy, denoted IS2i⁠, collapses. We show that if IS2i⊢IS2i+1⁠, then S2i(PV)⊢Σib=Πib and so the polynomial hierarchy collapses to Σip=Πip⁠. Our proof for this is independent from earlier works on relating the collapse of the hierarchy of classical bounded arithmetic and the collapse of the polynomial hierarchy. We give an elementary model theoretic proof using only the basic properties of the theories IS2i and we do not use results which belong to Cook and Urquhart and also Harnik that characterize the definable functions of these theories with long witnessing proofs.

It is shown that the intuitionistic theory of polynomial induction on positive Π1b (coNP) formulas does not prove the sentence ¬¬∀x, y∃z ≤ y(x ≤ |y| → x = |z|). This implies the unprovability of the scheme ¬¬PIND(∑1b+) in the mentioned theory. However, this theory contains the sentence ∀x, y¬¬∃z ≤ y(x ≤ |y| → x = |z|). The above independence result is proved by constructing an ω-chain of submodels of a countable model of S2 + Ω3 + ¬exp such that none of the worlds in the chain satisfies the sentence, and interpreting the chain as a Kripke model.

In this note we show that the intuitionistic theory of polynomial induction on ∏1b+-formulas does not imply the intuitionistic theory I S21 of polynomial induction on ∑1b+-formulas. We also show the converse assuming the Polynomial Hierarchy does not collapse. Similar results hold also for length induction in place of polynomial induction. We also investigate the relation between various other intuitionistic first-order theories of bounded arithmetic. Our method is mostly semantical, we use Kripke models of the theories.

Abstract We show that Intuitionistic Open Induction iop is not closed under the rule DNS(Ǝ1). This is established by constructing a Kripke model of iop + ¬Ly(2y > x), where Ly(2y > x) is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA− plus the scheme of weak ¬¬ LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula φ(y) having only y free. (PA−)i ⊢ Lyφ(y). We observe that the theories iop, i∀1 and iΠ1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop.