Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HAω into a type theory WL, that can be described as Troelstra's system with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HAω if and only if its corresponding type in WL is inhabited. Analogous results are proved for Diller's so-called restricted system and for a type theory based on predicate logic instead of arithmetic.

The theory of immediate pairs of Henselian valued fields, with a given residual theory (of characteristic zero) and a given theory of valuation group (nonzero), is undecidable and has completions.

The core model K was introduced by R. B. Jensen and A. J. Dodd [DoJ]. K is the union of Gödel's constructible universe L together with all mice, i.e., , and K is a transitive model of ZFC + (V = K) + GCH (see [DoJ]). V = K is consistent with the existence of Ramsey cardinals [M], and if cf(α) > ω, V = K is consistent with the existence of α-Erdös cardinals [J]. Let K be Ramsey. Then there is a smallest inner model Wκ of ZFC in which κ is Ramsey. We have Wκ ⊨ V = K and Wκ ⊆ K [M]. The existence of Wκ with is equivalent to the existence of a sharplike mouse on N ⊨ K with N ⊨ κ Ramsey. (A mouse N on is called sharplike provided .) We have , where is the mouse iteration of N. N is the oleast mouse not in Wκ (see [J] and [DJKo]). Here < denotes the mouse order. The context always clarifies whether the mouse order or the usual <-relation is meant.

The main result of §1 is that Wκ ⊨ κ is the only Ramsey cardinal. A similar result has been found true in the smallest inner model L[U] of ZFC + “κ is measurable” if U is a normal measure on κ: L[U] ⊨ κ is the only measurable cardinal [Ku].

Given a subset A of a fixed saturated model , we let denote the algebra of definable subsets of the domain of M of with parameters from A. Then a complete type p over A can be regarded as a measure on , assigning the value 1 to members of p and 0 to nonmembers. In [5] and [6], Keisler developed a theory of forking concerning probability measures. Therefore it generalizes the ordinary theory. On a different track, we can view the complement of the type p, or the collection of null sets of any measure on , as ideals on . Moreover, ideals and the pseudometric of a measure form examples of the so-called FN topology. Roughly speaking, an FN topology is one that topologizes the ring structure of a Boolean algebra. Associated with this topology is a special basis, called an FN basis. For , it is natural to identify such a basis with a collection of partial types approximating a certain type.

In this paper, we extend the theory of forking and deal with FN bases (hence ideals in particular). By proving a few results here, we hope to indicate that this extension could become as fruitful as Keisler's theory and hence provide an alternative. Our approach here is more algebraic and less analytic. Unlike [5], methods from nonstandard analysis are not used.

There are two fundamental reasons why the classical theory should be generalized. One is to extend our investigation to unstable theories. (There are no stability assumptions on the theory in the present work.) The other is to study different and more flexible ways of collecting formulas, such as FN basis.

After fixing our notation in §1, we first deal with ideals in §2. We study certain nice extensions. Specifically, we prove the existence of flat nonforking ideals. We then provide a normalization theorem for ideals.

Elementary axioms describe a category of categories. Theorems of category theory follow, including some on adjunctions and triples. A new result is that associativity of composition in categories follows from cartesian closedness of the category of categories. The axioms plus an axiom of infinity are consistent iff the axioms for a well-pointed topos with separation axiom and natural numbers are. The theory is not finitely axiomatizable. Each axiom is independent of the others. Further independence and definability results are proved. Relations between categories and sets, the latter defined as discrete categories, are described, and applications to foundations are discussed.

This paper is a sequel to [4]. Our main concern here is to study the FN bases, which correspond to classical notions like heirs and definable extensions. We also attempt to characterize these notions in our context. This leads to the use of tools like ultrapower constructions.

We continue to work under the assumptions and using the notation of [4, §1]. For example, we require a sufficiently saturated model of a fixed complete theory T in a language , and ℒ and A and B are used to denote (not necessarily small) subsets of M. The concept of FN basis is defined in [4, Definition 3.2]. Nonforking is defined in [4, Definitions 2.2 and 3.7].

This paper is organized as follows: §1 deals with heirs and definability. The classical result stating that definability is equivalent to the uniqueness of an heir is generalized (Theorem 1.7). §2 uses an ultrapower to prove the existence of an heir (Corollary 2.6). We also determine exactly when embeddability into an ultrapower is possible. §3 relates ultrapowers to flatness and nonforking. In sharp contrast to the classical case, ultrapowers of FN bases need not be nonforking; but some criteria are established (Propositions 3.2 and 3.3, and Theorem 3.4). Finally, definability is characterized as the flatness of all ultrapowers (Theorem 3.6).

Basic results on the model theory of substructures of a fixed model are presented. The main point is to avoid the use of the compactness theorem, so this work can easily be applied to the model theory of Lω1,ω and its relatives. Among other things we prove the following theorem:

Let M be a model, and let λ be a cardinal satisfying λ∣L(M)∣ = λ. If M does not have the ω-order property, then for every A ⊆ M, ∣A∣ ≤ λ, and every I ⊆ M of cardinality λ+ there exists J ⊆ I cardinality λ+ which is an indiscernible set over A.

This is an improvement of a result of S. Shelah.

Let be p-adic closures of a countable Hilbertian field K. The main result of [EJ] asserts that the field has the following properties for almost all σ1,…,σe + m ϵ G(K) (in the sense of the unique Haar measure on G(K)e+m):

(a) Kσ is pseudo p-adically closed (abbreviation: PpC), i.e., each nonempty absolutely irreducible variety defined over Kσ has a Kσ-rational point, provided that it has a simple rational point in each p-adic closure of Kσ.

(b) G(Kσ) ≅ De,m, where De,m is the free profinite product of e copies Γ1,…, Γe of G(ℚp) and a free profinite group of rank m.

(c) Kσ has exactly e nonequivalent p-adic valuation rings. They are the restrictions Oσ1,…, Oσe of the unique p-adic valuation rings on , respectively.

In this paper we show that this result is in a certain sense the best possible. More precisely, we first show that the class of fields which satisfy (a)–(c) above is elementary in the appropriate language e(K), which is the ordinary first-order language of rings augmented by constant symbols for the elements of K and by e new unary relation symbols (interpreted as e p-adic valuation rings).

Let M be a given model with similarity type L = L(M), and let L′ be any fragment of L∣L(M∣+,ω of cardinality ∣L(M)∣. We call N ≺ ML′-relatively saturated iff for every B ⊆ N of cardinality less than ∥N∥ every L′-type over B which is realized in M is realized in N. We discuss the existence of such submodels.

The following are corollaries of the existence theorems.

(1) If M is of cardinality at least ℶω1, and fails to have the ω order property, then there exists N ≺ M which is relatively saturated in M of cardinality ℶω1.

(2) Assume GCH. Let ψ ∈ Lω1, ω, and let L′ ⊆ Lω1, ω be a countable fragment containing ψ. If ∃χ > ℵ0 such that I(χ, ψ) < 2χ, then for every M ⊨ ψ and every cardinal λ < ∥M∥ of uncountable cofinality, M has an L′-relatively saturated submodel of cardinality λ.

By a variety, we mean a class of structures in some language containing only function symbols which is equationally defined or equivalently is closed under homomorphisms, submodels and products.

If K is a class of -structures then I(K, λ) denotes the number of nonisomorphic models in K of cardinality λ. When we say that K has few models, we mean that I(K,λ) < 2λ for some λ > ∣∣. If I(K,λ) = 2λ for all λ > ∣∣, then we say K has many models. In [9] and [10], Shelah has shown that for an elementary class K, having few models is a strong structural condition.

The mathematical treatment of the concepts of vagueness and approximation is of increasing importance in artificial intelligence and related research. The theory of fuzzy sets was created by Zadeh [Z] to allow representation and mathematical manipulation of situations of partial truth, and proceeding from this a large amount of theoretical and applied development of this concept has occurred. The aim of this paper is to develop a natural logic and set theory that is a candidate for the formalisation of the theory of fuzzy sets. In these theories the underlying logic of properties and sets is intuitionistic, but there is a subset of formulae that are ‘crisp’, classical and two-valued, which represent the certain information. Quantum logic or logics weaker than intuitionistic can also be adopted as the basis, as described in [L]. The relationship of this theory to the intensional set theory MZF of [Gd] and the global intuitionistic set theory GIZF of Takeuti and Titani [TT] is also treated.

In this paper we prove undecidability of first-order definability of propositional formulas. The main result is proved for intuitionistic formulas, but it remains valid for other kinds of propositional formulas by analogous arguments or with the help of various translations.

For general background on correspondence theory the reader is referred to van Benthem [1], [2] (see [3] for a survey of recent results).

The method for the proofs of undecidability in this paper will be to simulate calculations of a Minsky machine by intuitionistic formulas. §3 concerns this simulation. Effective procedures for the construction of simulating modal formulas can be found in the literature (cf. [4]).

The principal results of the paper are in §4. §5 gives some further undecidability results, that will be proved in another paper by modification of the method of this paper.

I am indebted to the referee for drawing my attention to some errors in an earlier version of this paper.

By means of models in toposes of C-sets (where C is a small category), necessary conditions are found for the minimum quantified extension of a propositional (intermediate, modal) logic to be complete with respect to Kripke semantics; in particular, many well-known systems turn out to be incomplete.

We discuss in the paper the following problem: Given a function in a given Baire class, into “how many” (in terms of cardinal numbers) functions of lower classes can it be decomposed? The decomposition is understood here in the sense of the set-theoretical union.

A chain-closed field is defined as a chainable field (i.e. a real field such that, for all n ∈ N, ΣK 2n+2 ≠ ΣK 2n ) which does not admit any “faithful” algebraic extension, and can also be seen as a field having a Henselian valuation ν such that the residue field K/ν is real closed and the value group νK is odd divisible with ∣νK/2νK∣ = 2. If K admits only one such valuation, we show that f ∈ K(X) is in ΣK(X)2n for any real algebraic extension L of K,“f(L) ⊆ ΣL 2n ” holds. The conclusion is also true for K = R((t))(a chainable but not chain-closed field), and in the case n = 1 it holds for several variables and any real field K.

In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)—full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.

The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for ∨ and ∃ restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.

A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.

The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.

The notion “validity” is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to “validity” have been used earlier by Tait (convertability), Girard (réducibilité) and Martin-Löf (computability).

In Prawitz [2] the N.D. system is restricted in the sense that ∨ and ∃ are not treated as primitive logical constants, and hence the deductions can only be seen to be “natural” with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for ∨ and ∃ in the restricted system does not imply the normalization theorem for the full system.

Many philosophers take set-theoretic discourse to be about objects of a special sort, namely sets; correlatively, they regard truth in such discourse as quite like truth in discourse about nonmathematical objects. There is a thin “disquotational” way of construing this construal; but that may candy-coat a philosophically substantive semantic theory: the Mathematical-Object theory of the basis for the distribution of truth and falsehood to sentences containing set-theoretic expressions. This theory asserts that truth and falsity for sentences containing set-theoretic expressions are grounded in semantic facts (about the relation between language and the world) of the sort modelled by the usual model-theoretic semantics for an uninterpreted formal first-order language. For example, it would maintain that ‘{ } ∈ {{ }}” is true in virtue of the set-theoretic fact that the empty set is a member of its singleton, and the semantic facts that ‘{ }’ designates the empty set,‘{{ }}’ designates its singleton, and ‘∈’ applies to an ordered pair of objects iff that pair's first component is a member of its second component.

Now this theory may come so naturally as to seem trivial. My purpose here is to loosen its grip by “modelling” an alternative account of the alethic underpinnings of set-theoretic discourse. According to the Alternative theory, the point of having set-theoretic expressions (‘set’ and ‘∈’ will do) in a language is not to permit its speakers to talk about some special objects under a special relation; rather it is to clothe a higher-order language in lower-order garments.

Nous considérons des théories d'anneaux locaux reliées aux corps p-adiques, p un nombre premier. Dans le §1 nous établissons les axiomatisations données dans [B1], ainsi qu'une autre axiomatisation des anneaux apparaissant dans [R1]. Il s'agit d'anneaux locaux henséliens dont le corps résiduel est élémentairement équivalent à une extension finie d'un corps p-adique. Nous les appelons anneaux locaux p-adiquement clos. Dans le contexte de [R1] et [B1] ils apparaissent comme fibres du faisceau structural (aussi appelé faisceau de Nash dans [BS]) accompagnant les spectres p-adiques. L'intérêt de nos axiomatisations provient de la simplicité des axiomes qui rendent compte des propriétés henséliennes. Dans le §2 nous donnons une axiomatisation d'une théorie d'anneaux locaux qui apparaît naturellement dans le contexte de la théorie des modèles des corps valués, et se trouve être une complétion d'une théorie du §1. Nous appelons ces anneaux, anneaux intègres p-adiquement clos.

Dans le §3 nous utilisons §2 pour montrer que les anneaux intègres p-adiquement clos apparaissent aussi comme anneaux quotients d'anneaux de fonctions continues définissables sur les courbes affines p-adiques. Nous représentons alors un idéal premier comme le noyau d'un morphisme d'évaluation en un point non-standard de la courbe. Le spectre p-adique fournit un outil commode qui permet de décrire la situation de façon concise.

It is shown that Con(ZF) implies Con(ZFC + there exists a Dowker filter on ω2). The problem is also considered on higher cardinals.

We study the following conjecture.

Conjecture.Let T be an ω-stable theory with continuum many countable models. Then either i) T has continuum many complete extensions in L 1(T), or ii) some complete extension of T in L 1has continuum many L 1-types without parameters.

By Shelah's proof of Vaught's conjecture for ω-stable theories, we know that there are seven types of ω-stable theory with continuum many countable models. We show that the conjecture is true for all but one of these seven cases. In the last case we show the existence of continuum many L 2-types.