In this paper we consider the three-valued logic used by Kleene [6] in the theory of partial recursive functions. This logic has three truth values: true (T), false (F), and undefined (U). One interpretation of U is as follows: Suppose we have two partially recursive predicates P(x) and Q(x) and we want to know the truth value of P(x) ∧ Q(x) for a particular x0. If x0 is in the domain of definition of both P and Q, then P(x0) ∧ Q(x0) is true if both P(x0) and Q(x0) are true, and false otherwise. But what if x0 is not in the domain of definition of P, but is in the domain of definition of Q? There are several choices, but the one chosen by Kleene is that if Q(X0) is false, then P(x0) ∧ Q(x0) is also false and if Q(X0) is true, then P(x0) ∧ Q(X0) is undefined.

What arises is the question about knowledge of whether or not x0 is in the domain of definition of P. Is there an effective procedure to determine this? If not, then we can interpret U as being unknown. If there is an effective procedure, then our decision for the truth value for P(x) ∧ Q(x) is based on the knowledge that is not in the domain of definition of P. In this case, U can be interpreted as undefined. In either case, we base our truth value of P(x) ∧ Q(x) on the truth value of Q(X0).

In a previous paper [13] we introduced a hierarchy (GnAω)n∈ℕ of subsystems of classical arithmetic in all finite types where the growth of definable functions of GnAω corresponds to the well-known Grzegorczyk hierarchy. Let AC-qf denote the schema of quantifier-free choice.

[11], [13], [8] and [7] study various analytical principles Γ in the context of the theories GnAω + AC-qf (mainly for n = 2) and use proof-theoretic tools like, e.g., monotone functional interpretation (which was introduced in [12]) to determine their impact on the growth of uniform bounds Φ such that

which are extractable from given proofs (based on these principles Γ) of sentences

Here A0(u, k, v, w) is quantifier-free and contains only u, k, v, w as free variables; t is a closed term and ≤p is defined pointwise. The term ‘uniform bound’ refers to the fact that Φ does not depend on v ≤ptuk (see [12] for the relevance of such uniform bounds in numerical analysis and for concrete applications to approximation theory).

Among the results of this paper are the following:

1. Every Boolean (ultra)power is the union of an updirected elementary family of direct ultrapowers.

2. Under certain conditions, a finitely iterated Boolean ultrapower is isomorphic to a single Boolean ultrapower.

3. A ω-bounded filtral power is an elementary substructure of a filtral power.

4. Let be an elementary class closed under updirected unions (e.g., if is an amalgamation class); then is closed under finite products if and only if is closed under reduced products if and only if is a Horn class.

We prove an Ax-Kochen-Ershov like transfer principle for groups acting on groups. The simplest case is the following: let B be a soluble group acting on an abelian group G so that G is a torsion-free divisible module over the group ring ℤ[B], then the theory of B determines the one of the two-sorted structure 〈G,B,*〉, where * is the action of B on C. More generally, we show a similar principle for structures 〈G,B,*〉, where G is a torsion-free divisible module over the quotient of ℤ[B] by the annulator of G.

Two applications come immediately from this result:

First, for not necessarily commutative domains, where we consider the action of a subgroup of the invertible elements on the additive group. We obtain then the decidability of a weakened structure of ring, with partial multiplication.

The second application is to pure groups. The semi-direct product of G by B is bi-interpretable with our structure 〈G,B,*〉. Thus, we obtain stable decidable groups that are not linear over a field.

The basic notions of the theory of term rewriting are defined for terms that may involve function letters of infinite arity. A sufficient condition for completeness is derived, and its use demonstrated by the example of abstract clones over infinitary signatures.

0# can be invisibly class generic.

In this paper, we prove that there exist computably enumerable degrees a and b such that a > b and for any degree x, if x ≤ a and x is a minimal degree, then x < b.

Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε0-recursive function []0: T → ω so that a reduces to b implies [a]0 > [b]0. The construction of [ ]0 is based on a careful analysis of the Howard-Schütte treatment of Gödel's T and utilizes the collapsing function ψ: ε0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [ ]0 is also crucially based on ideas developed in the 1995 paper “A proof of strongly uniform termination for Gödel's T by the method of local predicativity” by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper.

Indeed, for given n let Tn be the subsystem of T in which the recursors have type level less than or equal to n + 2. (By definition, case distinction functionals for every type are also contained in Tn.) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the Tn-derivation lengths in terms of ω+2-descent recursive functions. The derivation lengths of type one functionals from Tn (hence also their computational complexities) are classified optimally in terms of <ωn+2 -descent recursive functions.

In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T0 is primitive recursive, thus any type one functional a in T0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T1 in terms of multiple recursion.

As proof-theoretic corollaries we reobtain the classification of the IΣn+1-provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO(ε0) ⊢ Π20 − Refl(PA) and PRA + PRWO(ωn+2) ⊢ Π20 − Refl(IΣn+1), hence PRA + PRWO(ε0) ⊢ Con(PA) and PRA + PRWO(ωn+2) ⊢ Con(IΣn+1).

For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity.

In this paper we show that the compactness of a Loeb space depends on its cardinality, the nonstandard universe it belongs to and the underlying model of set theory we live in. In §1 we prove that Loeb spaces are compact under various assumptions, and in §2 we prove that Loeb spaces are not compact under various other assumptions. The results in §1 and §2 give a quite complete answer to a question of D.Ross in [9], [11] and [12].

If there is no inner model with a cardinal κ such that ο(κ) = κ++ then the set K ∩ Hω1 is definable over Hω1 by a Δ4 formula, and the set of countable initial segments of the core model is definable over Hω1 by a Π3 formula. We show that if there is an inner model with infinitely many measurable cardinals then there is a model in which is not definable Σ3 by any Σ3 formula, and K ∩ Hω1 is not definable by any boolean combination of Σ3 formulas.

We denote by KP_ the fragment of set-theory containing the axioms of extensionality, pairing, union and foundation as well as the schemas of ∆0-comprehension and ∆0-collection, that is: Kripke-Platek set-theory (KP) with the axiom of foundation in place of the ∈-induction schema. The theory KP is obtained by adding to KP_ the schema of ∈-induction

Using ∈-induction it is possible to prove the existence of the transi tive closure without appealing to the axiom of infinity (see, e.g., [1]). Vice versa, when a theory proves the existence of the transitive closure, some induction is immediately ensured (by foundation and comprehension). This is not true in general: e.g., the whole of Zermelo-Fraenkel set-theory without the axiom of infinity does not prove ∈-induction (in fact, it does not prove the existence of the transitive closure; see, e.g., [3]). Open-induction is the schema of ∈-induction restricted to open formulas. We prove the following theorem.

KP_ proves open-induction.

We reason in a fixed but arbitrary model of KP_ whom we refer to as the model. The language is extended with a name for every set in the model. We call this constants parameters. Let φ(x) be a satisfiable open-formula possibly depending on parameters and with no free variable but x. We show that φ(x) is satisfied by an ∈-minimal set, that is, a set a such that φ(a) and (∀x ∈ a) ¬φ(x). We assume that no ordinal satisfies φ(x), otherwise the existence of a ∈-minimal set follows from foundation and comprehension.

We show the consistency, relative to a supercompact cardinal, of the least measurable cardinal being both strongly compact and fully Laver indestructible. We also show the consistency, relative to a supercompact cardinal, of the least strongly compact cardinal being somewhat supercompact yet not completely supercompact and having both its strong compactness and degree of supercompactness fully Laver indestructible.

We present a full completeness theorem for the multiplicative fragment of a variant of noncommutative linear logic, Yetter's cyclic linear logic (CyLL). The semantics is obtained by interpreting proofs as dinatural transformations on a category of topological vector spaces, these transformations being equivariant under certain actions of a noncocommutative Hopf algebra called the shuffle algebra Multiplicative sequents are assigned a vector space of such dinaturals, and we show that this space has as a basis the denotations of cut-free proofs in CyLL + MIX. This can be viewed as a fully faithful representation of a free *-autonomous category, canonically enriched over vector spaces.

This paper is a natural extension of the authors' previous work, “Linear Läuchli Semantics”, where a similar theorem is obtained for the commutative logic MLL + MIX. In that paper, we interpret proofs as dinaturals which are invariant under certain actions of the additive group of integers. Here we also present a simplification of that work by showing that the invariance criterion is actually a consequence of dinaturality. The passage from groups to Hopf algebras in this paper corresponds to the passage from commutative to noncommutative logic. However, in our noncommutative setting, one must still keep the invariance condition on dinaturals.

It is proved consistent that there be a proper σ-ideal on ω1 and an ℵ1-preserving poset ℙ such that ℙ ⊩ the σ-ideal generated by is not proper.

We shall prove quantifier elimination theorems for neocompact formulas, which define neocompact sets and are built from atomic formulas using finite disjunctions, infinite conjunctions, existential quantifiers, and bounded universal quantifiers. The neocompact sets were first introduced to provide an easy alternative to nonstandard methods of proving existence theorems in probability theory, where they behave like compact sets. The quantifier elimination theorems in this paper can be applied in a general setting to show that the family of neocompact sets is countably compact. To provide the necessary setting we introduce the notion of a law structure. This notion was motivated by the probability law of a random variable. However, in this paper we discuss a variety of model theoretic examples of the notion in the light of our quantifier elimination results.

We define a generalized version of CM-triviality, and show that in the presence of enough regular types, or solubility, a stable CM-trivial group is nilpotent-by-finite. A torsion-free small CM-trivial stable group is abelian and connected. The first result makes use of a generalized version of the analysis of bad groups.

Applying Woodin's non-stationary tower notion of forcing, I prove that the existence of a supercompact cardinal κ in V and a Ramsey dilator in some small forcing extension V[G] implies the existence in V of a measurable dilator of size κ, measurable by κ-complete measures.

The main result of this paper is Theorem 3.1 which is a criterion for weak o-minimality of a linearly ordered structure in terms of realizations of 1-types. Here we also prove some other properties of weakly o-minimal structures. In particular, we characterize all weakly o-minimal linear orderings in the signature {<, =} . Moreover, we present a criterion for density of isolated types of a weakly o-minimal theory. Lastly, at the end of the paper we present some remarks on the Exchange Principle for algebraic closure in a weakly o-minimal structure.

Our goal in this paper is to analyze the interpretation of arbitrary unsolvable λ-terms in a given model of λ-calculus. We focus on graph models and (a special type of) stable models. We introduce the syntactical notion of a decoration and the semantical notion of a critical sequence. We conjecture that any unsolvable term β-reduces to a term admitting a decoration. The main result of this paper concerns the interconnection between those two notions: given a graph model or stable model , we show that any unsolvable term admitting a decoration and having a non-empty interpretation in generates a critical sequence in the model.

In the last section, we examine three classical graph models, namely the model of Plotkin and Scott, Engeler's model and Park's model . We show that and do not contain critical sequences whereas does.

We prove that every rectangularly dense diagonal-free cylindric algebra is representable. As a corollary, we give finite, sound and complete axiomatizations for the finite-variable fragments of first order logic without equality and for multi-dimensional modal S5-logic.