We introduce the notions of stationarily ordered types and theories; the latter generalizes weak o-minimality and the former is a relaxed version of weak o-minimality localized at the locus of a single type. We show that forking, as a binary relation on elements realizing stationarily ordered types, is an equivalence relation and that each stationarily ordered type in a model determines some order-type as an invariant of the model. We study weak and forking non-orthogonality of stationarily ordered (...) types, show that they are equivalence relations and prove that invariants of non-orthogonal types are closely related. The techniques developed are applied to prove that in the case of a binary, stationarily ordered theory with fewer than countable models, the isomorphism type of a countable model is determined by a certain sequence of invariants of the model. In particular, we confirm Vaught's conjecture for binary, stationarily ordered theories. (shrink)

The complete characterisation of order types of non-standard models of Peano arithmetic and its extensions is a famous open problem. In this paper, we consider subtheories of Peano arithmetic (both with and without induction), in particular, theories formulated in proper fragments of the full language of arithmetic. We study the order types of their non-standard models and separate all considered theories via their possible order types. We compare the theories with and without induction and (...) observe that the theories without induction tend to have an algebraic character that allows model constructions by closing a model under the relevant algebraic operations. (shrink)

The complete characterisation of order types of non-standard models of Peano arithmetic and its extensions is a famous open problem. In this paper, we consider subtheories of Peano arithmetic (both with and without induction), in particular, theories formulated in proper fragments of the full language of arithmetic. We study the order types of their non-standard models and separate all considered theories via their possible order types. We compare the theories with and without induction and (...) observe that the theories without induction tend to have an algebraic character that allows model constructions by closing a model under the relevant algebraic operations. (shrink)

The characterization of second-order type isomorphisms is a purely syntactical problem that we propose to study under the enlightenment of game semantics. We study this question in the case of second-order λμ-calculus, which can be seen as an extension of system F to classical logic, and for which we define a categorical framework: control hyperdoctrines.Our game model of λμ-calculus is based on polymorphic arenas which evolve during the play. We show that type isomorphisms coincide with the “equality” on (...) arenas associated with types. Finally we deduce the equational characterization of type isomorphisms from this equality. We also recover from the same model Roberto Di Cosmo’s characterization of type isomorphisms for system F.This approach leads to a geometrical comprehension on the question of second-order type isomorphisms, which can be easily extended to some other polymorphic calculi including additional programming features. (shrink)

An ordinal in a model of set theory is truly countable if its set of predecessors is countable in the real world. We classify the order types of the sets of truly countable ordinals. Models with indiscernibles and other related results are discussed.

We consider total well-founded orderings on monadic terms satisfying the replacement and full invariance properties. We show that any such ordering on monadic terms in one variable and two unary function symbols must have order typeω,ω2orωω. We show that a familiar construction gives rise to continuum many such orderings of order typeω. We construct a new family of such orderings of order typeω2, and show that there are continuum many of these. We show that there are only (...) four such orderings of order typeωω, the two familiar recursive path orderings and two closely related orderings. We consider also total well-founded orderings onNnwhich are preserved under vector addition. We show that any such ordering must have order typeωkfor some 1 ≤k≤n. We show that ifkshrink)

We consider total well-founded orderings on monadic terms satisfying the replacement and full invariance properties. We show that any such ordering on monadic terms in one variable and two unary function symbols must have order type $\omega, \omega^2$ or $\omega^\omega$. We show that a familiar construction gives rise to continuum many such orderings of order type $\omega$. We construct a new family of such orderings of order type $\omega^2$, and show that there are continuum many of these. (...) We show that there are only four such orderings of order type $\omega^\omega$, the two familiar recursive path orderings and two closely related orderings. We consider also total well-founded orderings on $\mathbf{N}^n$ which are preserved under vector addition. We show that any such ordering must have order type $\omega^k$ for some $1 \leq k \leq n$. We show that if $k < n$ there are continuum many such orderings, and if $k = n$ there are only $n$!, the $n$! lexicographic orderings. (shrink)

If A and B are subsets of natural numbers we say that A is recursively equivalent to B (denoted A ≃ B) if there is a one-one partial recursive function which maps A onto B, and that A is recursively isomorphic to B (denoted A ≅ B) if there is a one-one total recursive function which maps A onto B and Ā (the complement of A) onto B#x00AF;.

We give for ordinals α a lower bound for the least ordinal α such that Frordξ,β) and show that given enough measurable cardinals there are forcing extensions where the given bounds are sharp.

We present some techniques in c.c.c. forcing, and apply them to prove consistency results concerning the isomorphism and embeddability relations on the family of ℵ 1 -dense sets of real numbers. In this direction we continue the work of Baumgartner [2] who proved the axiom BA stating that every two ℵ 1 -dense subsets of R are isomorphic, is consistent. We e.g. prove Con). Let K H , be the set of order types of ℵ 1 -dense homogeneous (...) subsets of R with the relation of embeddability. We prove that for every finite model L , : Con iff L is a distributive lattice. We prove that it is consistent that the Magidor-Malitz language is not countably compact. We deal with the consistency of certain topological partition theorems. E.g. We prove that MA is consistent with the axiom OCA which says: “If X is a second countable space of power ℵ 1 , and { U 0 ,\h.;, U n−1 } is a cover of D ▪ X x X -} x,x> ¦ x ϵ X } consisting of symmetric open sets, then X can be partitioned into { X i \brvbar; i ϵ ω } such that for every i ϵ ω there is l such that D ⊇ U l ”. We also prove that MA+OCA [xrArr] 2 ℵ 0 = ℵ 2. (shrink)

J. N. Crossley [1] raised the question of whether the implication 2 + A = A ⇒ 1 + A = A is true for constructive order types (C.O.T.'s). Using an earlier definition of constructive order type, A. G. Hamilton [2] presented a counterexample. Hamilton left open the general question, however, since he pointed out that Crossley considers only orderings which can be embedded in a standard dense r.e. ordering by a partial recursive function, and that his (...) counterexample fails to meet this requirement. We resolve the question by finding a C.O.T. A which meets Crossley's requirement and such that 2 + A = A but 1 + A ≠ A. At the suggestion of A. B. Manaster and A. G. Hamilton we easily extend this construction to show that for any n ≧ 2, there is a C.O.T. A such that n + A = A but m + A ≠ A for 0 < m < n. Hence, Theorem 3 of [2] and all of its corollaries hold with the new definition of C.O.T. The construction is not difficult and requires no priority argument. The techniques are similar to those developed in [3], but no outside results are needed here. (shrink)

The goal of this short note is to interest set theorists in the order type ω*ω1, and to encourage them to work on the question of whether or not the Continuum Hypothesis decides the partition relation τ→2, for τ=ω*ω1 and for τ=ω1ω+2.

The main purpose of this paper is to introduce a class of algebraic structures related to many-valued ukasiewicz algebras. They are symmetrical Heyting algebras with a set of modal operators indexed by a finite completely symmetric poset. A representation theorem is given for these (not functionally complete) algebras.

This Element is an exposition of second- and higher-order logic and type theory. It begins with a presentation of the syntax and semantics of classical second-order logic, pointing up the contrasts with first-order logic. This leads to a discussion of higher-order logic based on the concept of a type. The second Section contains an account of the origins and nature of type theory, and its relationship to set theory. Section 3 introduces Local Set Theory, an important (...) form of type theory based on intuitionistic logic. In Section 4 number of contemporary forms of type theory are described, all of which are based on the so-called 'doctrine of propositions as types'. We conclude with an Appendix in which the semantics for Local Set Theory - based on category theory - is outlined. (shrink)

We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version à (...) la Tarski and à la Russell are shown to be the same. (shrink)

We prove an Omitting Types Theorem for certain algebraizable extensions of first order logic without equality studied in [SAI 00] and [SAY 04]. This is done by proving a representation theorem preserving given countable sets of infinite meets for certain reducts of ?- dimensional polyadic algebras, the so-called G polyadic algebras (Theorem 5). Here G is a special subsemigroup of (?, ? o) that specifies the signature of the algebras in question. We state and prove an independence result (...) connecting our representation theorem to Martin's axiom (Theorem 6). Also we show that the countable atomic G polyadic algebras are completely representable (Corollary 16) contrasting results on cylindric algebras. Several related results are surveyed. (shrink)

A key idea in both Frege's development of arithmetic in theGrundlagen[7] and Zermelo's 1904 proof [10] of the well-ordering theorem is that of a “type reducing” correspondence between second-level and first-level entities. In Frege's construction, the correspondence obtains betweenconceptandnumber, in Zermelo's (through the axiom of choice), betweensetandmember. In this paper, a formulation is given and a detailed investigation undertaken of a system ℱ of many-sorted first-order logic (first outlined in the Appendix to [6]) in which this notion of type (...) reducing correspondence is accorded a central role and which enables Frege's and Zermelo's constructions to be presented in such a way as to reveal their essential similarity. By adapting Bourbaki's version of Zermelo's proof of the well-ordering theorem, we show that, within ℱ, any correspondencecbetween second-level entities (here calledconcepts) and first-level ones (here calledobjects) induces a well-ordering relationW(c) in a canonical manner. We shall see that, whencis the “Fregean” correspondence between concepts and cardinal numbers,W(c) is (the well-ordering of) the ordinalω+ 1, and whencis a “Zermelian” choice function on concepts,W(c) is a well-ordering of the universal concept embracing all objects.In ℱ an important role is played by the notion ofextensionof a concept. To each conceptXwe assume there is assigned an objecte(X) in such a way that, for any conceptsX, Ysatisfying a certain predicateE, we havee(X) =e(Y) iff the same objects fall underXandY. (shrink)

Mendler, N.P., Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic 51 159–172. We add to the second-order lambda calculus the type constructors μ and ν, which give the least and greatest solutions to positively defined type expressions. Strong normalizability of typed terms is shown using Girard's candidat de réductibilité method. Using the same structure built for that proof, we prove a necessary and sufficient condition for determining when a collection (...) of equational type constraints admit the typing of only strongly normalizable terms. (shrink)

Fix \. Let \ denote first order logic restricted to the first n variables. Using the machinery of algebraic logic, positive and negative results on omitting types are obtained for \ and for infinitary variants and extensions of \.

On the analogy of the colloquial register in some modern languages, where narrative and argument may be punctuated by oaths and exclamations in order to maintain a high affective level and compel the hearer's attention, it is reasonable to postulate that Attic conversation also was punctuated by oaths, that this ingredient in comic language was drawn from life, and that the comparative frequency of ║ M M Δ in comedy is sufficiently explained thereby. There are obvious affinities between some (...) passages of comedy, relaxed conversation in Plato and Xenophon, and the forceful, man-to-man tone which Demosthenes sometimes adopts to such good effect . Compare, for instance, Ar. V. 133 f. στιν δ' νομα ⋮ τ μν γέροντι ⋮ Φιλοκλέων / να μ Δία, τ δ' υε κτλ., where the oath is a response to imagined incredulity, and X. Smp. 4.27 ατν δ σέ, η, γ εδον να μ τν πόλλω, τε κτλ. . It is also important that the commonest oaths fit, in most of their forms, the end of an iambic trimeter: μ τν Δία, ν Δία,ν τούς θεούς, μ τος θεούς. Add that in Aristophanic dialogue over half the iambic trimeters end with major pause, and half the remainder with minor pause, and we can see why Δ / established itself early as a distinctive comic pattern. Out of 105 examples of M M Δ cited from comedy in Section II above, 59 have the oath at verse-end. In the case of πάνυ, which was almost exclusively Attic and — to judge from its great rarity in tragedy — felt by Athenian poets to be prosaic, we lack evidence on its functions in the colloquial register; it may or may not have served as affective punctuation. In prose, we have to reckon with the fact that π Mπ and Mπ π constituted a genuine stylistic choice as far back as the evidence will take us, since the two earliest instances in prose are [X.] Ath. 2.3 πάνυ δι χρείαν and ibid. 3.5 πολλ τι πάνυ. The oath, as treated by the comic poets on the basis of colloquial usage, is bound to have served as a model for πάνυ, exerting an influence which pulled πάνυ to the end of the verse, but there was also a powerful metrical constraint. As a dibrach ending in a vowel which could not be elided or enter into crasis, πάνυ was especially appropriate for verse-end. That in itself was enough both to establish Mπ π as the dominant pattern in comedy and to promote Mπ … π. Out of the total of 104 examples of Mπ π in comedy, 93 have πάνυ at verse-end, which makes Mπ π / one of the hallmarks of comic style. Mπ … π does not occur in prose in association with any other feature identified as colloquial, but it should be noted that Aiskhines and Demosthenes are much fonder of Mπ π than other prose authors. In some cases one can see that the order Mπ π avoids a succession of short syllables or hiatus or both , but there are other cases in which it has the opposite effect . The possibility of comic influence on oratorical language cannot be dismissed out of hand. It is also possible that someone will find positive determinants which will explain all the cases of Mπ π in prose. σόδρα, which, like πάνυ, is peculiarly Attic, is metrically more tractable than πάνυ, since it can be elided; even so, out of the 80 comic examples of Mσ σ no less than 58 have σόδρα at verse-end, and of those 58 there are 22 at major pause, 8 at presumed major pause and 9 at minor pause. The comic treatment of σόδρα is thus comparable with the treatment of πάνυ, and Timokles 222.4 τηρεν…σόδρα is in fact the closest analogy we have to Ar. Pl. 234 f. χθομαι…πάνυ. δέ and γάρ are a different matter, and in some significant respects different from each other. Postponement of δέ is especially prominent in Aeschylus and then abundant in fourth-century comedy. It is much less common in Euripides , rare in Sophocles and Aristophanes , and virtually limited in prose to the categories which I labelled –. There is as yet no evidence to associate postponement of δέ with colloquial language; on the contrary, it seems to have begun as a feature of poetic language and to have been taken up and exploited by fourth-century comedy. If, in addition to being Aeschylean, it was colloquial in the fourth century, what happened to it afterwards? Except for such an isolated and inexplicable case as Diod. xx85.1 — in a military narrative — it is not a feature of the Koine at literary, documentary or subliterate level. Postponement of γάρ was no doubt encouraged by postponement of δέ, but it is not itself notably poetic ). One can see how it could possibly have developed in the spoken language of the fourth century, extending the function of γάρ as an explanatory particle in a way which makes it comparable with the English ‘you see’ in ‘He didn't dare pick it up. He hurt his back last year, you see’. For an extension of this kind we may compare the current extension of the English genitive affix in ‘Then the girl whose place she was taking's mother turned up’ and ‘The man that Christopher liked's Introduction is much better’. Moreover, postponed γάρ appears in a segment of conversation constructed in indirect speech by Theophrastus in Char. 8.9 τ πργμα βοσθαι γάρ . Again we must ask: what happened to it afterwards? A couple of cases in Theophrastus' botanical works could be a reflex of the influence of comedy on literary language at Athens. The influence was plainly short-lived, since it did not affect the Koine. It is not hard to see why serious poetry in the fifth century and earlier should have experimented occasionally with the postponement of δέ and γάρ: treatment of M M q as a valid alternative to M q M is metrically very convenient. No poet, however, could afford to use common words in a bizarre, un-Greek way merely to save himself time and trouble in constructing a verse. Linguistic innovation is normally analogical, proceeding by extension from a starting-point already there, and the most obvious starting-point for postponement of δέ and γάρ is constituted by my class . This consideration provides comic postponement with a pedigree, but does not deny it individuality. The remarkable scale and frequency with which comedy exploited a phenomenon which tragedy used with restraint and prose hardly at all gives comic postponement the right to be regarded as a quite distinctive artificial feature of comedy. (shrink)