The Gödel translation provides an embedding of the intuitionistic logic $\mathsf {IPC}$ into the modal logic $\mathsf {Grz}$ , which then embeds into the modal logic $\mathsf {GL}$ via the splitting translation. Combined with Solovay’s theorem that $\mathsf {GL}$ is the modal logic of the provability predicate of Peano Arithmetic $\mathsf {PA}$ , both $\mathsf {IPC}$ and $\mathsf {Grz}$ admit provability interpretations. When attempting to ‘lift’ these results to the monadic extensions $\mathsf {MIPC}$ , $\mathsf {MGrz}$ , and $\mathsf {MGL}$ of these logics, the same techniques no longer work. Following a conjecture made by Esakia, we add an appropriate version of Casari’s formula to these monadic extensions (denoted by a ‘+’), obtaining that the Gödel translation embeds $\mathsf {M^{+}IPC}$ into $\mathsf {M^{+}Grz}$ and the splitting translation embeds $\mathsf {M^{+}Grz}$ into $\mathsf {MGL}$ . As proven by Japaridze, Solovay’s result extends to the monadic system $\mathsf {MGL}$ , which leads us to a provability interpretation of both $\mathsf {M^{+}IPC}$ and $\mathsf {M^{+}Grz}$ .

Simpson [6] showed that every countable model ${\cal M} \models PA$ has an expansion $\left( {{\cal M},X} \right) \models P{A^{\rm{*}}}$ that is pointwise definable. A natural question is whether, in general, one can obtain expansions of a nonprime model in which the definable elements coincide with those of the underlying model. Enayat [1] showed that this is impossible by proving that there is ${\cal M} \models PA$ such that for each undefinable class X of ${\cal M}$, the expansion $\left( {{\cal M},X} \right)$ is pointwise definable. We call models with this property Enayat models. In this article, we study Enayat models and show that a model of $PA$ is Enayat if it is countable, has no proper cofinal submodels and is a conservative extension of all of its elementary cuts. We then show that, for any countable linear order γ, if there is a model ${\cal M}$ such that $Lt\left( {\cal M} \right) \cong \gamma$, then there is an Enayat model ${\cal M}$ such that $Lt\left( {\cal M} \right) \cong \gamma$.

In this paper we shall prove that any 2-transitive finitely homogeneous structure with a supersimple theory satisfying a generalized amalgamation property is a random structure. In particular, this adapts a result of Koponen for binary homogeneous structures to arbitrary ones without binary relations. Furthermore, we point out a relation between generalized amalgamation, triviality and quantifier elimination in simple theories.

By the Galvin–Mycielski–Solovay theorem, a subset X of the line has Borel’s strong measure zero if and only if $M+X\neq \mathbb {R}$ for each meager set M.

A set $X\subseteq \mathbb {R}$ is meager-additive if $M+X$ is meager for each meager set M. Recently a theorem on meager-additive sets that perfectly parallels the Galvin–Mycielski–Solovay theorem was proven: A set $X\subseteq \mathbb {R}$ is meager-additive if and only if it has sharp measure zero, a notion akin to strong measure zero.

We investigate the validity of this result in Polish groups. We prove, e.g., that a set in a locally compact Polish group admitting an invariant metric is meager-additive if and only if it has sharp measure zero. We derive some consequences and calculate some cardinal invariants.

In [1, §14E], a sequent calculus formulation (L.-formulation) of type assignment (theory of functionality) is given for a system based either on a system of combinators with strong reduction or on a system of λη-calculus provided that the rule for subject conversion (which says that if X has type α and X cnv Y then Y has type α) is postulated for the system. This sequent calculus formulation does not work for a system based on the λβ-calculus. In [2] I introduced a sequent calculus formulation for a system without the rule of subject conversion based on any of the three systems mentioned above. Further, in [2, §5] I pointed out that if proper inclusions of the form of the statement that λx·x is a function from α to β are postulated, then functions are identified with their restrictions in the λη-calculus but not in the λβ-calculus, and that therefore there is some interest in having a sequent calculus formulation of type assignment with the rule of subject conversion for systems based on the λβ-calculus. In this paper, such a system is presented, the elimination theorem (Gentzen's Hauptsatz) is proved for it, and it is proved equivalent to the natural deduction formulation of [1, §14D].

I shall assume familiarity with the λβ-calculus, and shall use (with minor modifications) the notational conventions of [1]. Hence, the theory of type assignment (theory of functionality) will be based on an atomic constant F such that if α and β are types then Fαβ represents roughly the type of functions from α to β (more exactly it represents the type of functions whose domain includes α and under which the image of α is included in β).

There is a family of questions in relativized complexity theory—weak analogs of the Friedberg Jump-Inversion Theorem—that are resolved by 1-generic sets but which cannot be resolved by essentially any weaker notion of genericity. This paper defines aw2-generic sets, i.e., sets which meet every dense set of strings that is re. in some incomplete r.e. set. Aw2-generic sets are very close to 1-generic sets in strength, but are too weak to resolve these questions. In particular, it is shown that for any set X there is an aw2-generic set G such that NPG ∩ co-NPG ⊈ PG⊕x. (On the other hand, if G is 1-generic, then NPG ∩ co-NPG ⊆ PG⊕SAT, where SAT is the NP-complete satisfiability problem [6].) This result runs counter to the fact that most finite extension constructions in complexity theory can be made effective. These results imply that any finite extension construction that ensures any of the Friedberg analogs must be noneffective, even relative to an arbitrary incomplete r.e. set. It is then shown that the recursion theoretic properties of aw2-generic sets differ radically from those of 1-generic sets: every degree above 0′ contains an aw2-generic set: no aw2-generic set exists below any incomplete r.e. set: there is an aw2-generic set which is the join of two Turing equivalent aw2-generic sets. Finally, a result of Shore is presented [30] which states that every degree above 0′ is the jump of an aw2-generic degree.

Let α be any countable admissible ordinal greater than ω. There is a transitive set A such that A is admissible, locally countable, OnA = α, and A satisfies Σ1-separation. In fact, if B is any nonstandard model of KP + ∀x ⊆ ω (the hyperjump of x exists), the ordinal standard part of B is greater than ω, and every standard ordinal in B is countable in B, then HCB ∩ (standard part of B) satisfies Σ-separation.

A prime model O of some complete theory T is a model which can be elementarily imbedded into any model of T (cf. Vaught [7, Introduction]). We are going to replace the assumption that T is complete and that the maps between the models of T are elementary imbeddings (elementary extensions) by more general conditions. T will always be a first order theory with identity and may have function symbols. The language L(T) of T will be denumerable. The maps between models will be so called F-maps, i.e. maps which preserve a certain set F of formulas of L(T) (cf. I.1, 2). Roughly speaking a generalized prime model of T is a denumerable model O which permits an F-map O→M into any model M of T. Furthermore O has to be “generated” by formulas which belong to a certain subset G of F.