We consider the weak truth-table reducibility ≤_wtt and we prove the existence of wtt-introimmune sets in ∆⁰₂. This closes the gap on the existence of arithmetical r-introimmune sets for all the known reducibilities ≤_r strictly contained in the Turing reducibility.

We investigate the complexity of the standard translation of lambda calculus into combinatory logic. The main result shows that the asymptotic growth rate of the size of a translated term is Ø(n³) in worst-case, where n denotes the size of the lambda term.

We analyze semantically the logical inference rules in cut-free sequent calculi for the modal logics hich are obtained from the least normal logic K by adding axioms from T, 4, 5, D and B. This implies Kripke completeness, as well as the cutelimination property or the subformula property of the calculi. By slightly modifying the arguments, the  nite model property of the logics also follows.

By means of a forcing argument, it was shown by Pereira that if CH holds then there is a separable PCF space of height ω1 + 1 which is not Fréchet-Urysohn. In this paper, we give a direct proof of Pereira’s theorem by means of a forcing-free argument, and we extend his result to PCF spaces of any height δ + 1 where δω2 with cf(δ) = ω1.

The typical indirect proof of an abstract extension theorem, by the Kuratowski-Zorn lemma, is based on a onestep extension argument. While Bell has observed this in case of the axiom of choice, for subfunctions of a given relation, we now consider such extension patterns on arbitrary directed-complete partial orders. By postulating the existence of so-called total elements rather than maximal ones, we can single out an immediate consequence of the Kuratowski-Zorn lemma from which quite a few abstract extension theorems can be deduced more directly, apart from certain definitions by cases. Applications include Baer’s criterion for a module to be injective. Last but not least, our general extension theorem is equivalent to a suitable form of the Kuratowski-Zorn lemma over constructive set theory.

In this paper, we introduce a proof system NQGL for a Kripke complete predicate extension of the logic GL of provability. While GL is defined by K and the Lӧb formula □(□p ⊃p) ⊃□p, NQGL does not have the L¨ob formula as its axiom, but has a non-compact rule, that is, a derivation rule with countably many premises, instead. We show that NQGL enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite.

In this paper we isolate a property for forcing notions, the *-Prikry condition, that is similar to the Prikry condition but that is topological: A forcing P satisfies it iff for every p ∈Pand for every open dense D ⊆P, there are n ∈ωand q ≤∗p such that for any r ≤q with l(r) = l(q) + n, r ∈D, for some length notion l. This is implicit in many proofs in literature. We prove this for the tree Prikry forcing and the long extender Prikry forcing.