In this paper we generalize the pigeonhole principle by using isols as our fundamental counting tool.

It is well known that combinatory logic with unrestricted introduction and elimination rules for implication is inconsistent in the strong sense that an arbitrary term Y is provable. The simplest proof of this, now usually called Curry's paradox, involves for an arbitrary term Y, a term X defined by X = Y(CPy).

The fact that X = P XY = X ⊃ Y is an essential part of the proof.

The paradox can be avoided by placing restrictions on the implication introduction rule or on the axioms from which it can be proved.

In this paper we determine the forms that must be taken by inconsistency proofs of systems of propositional calculus based on combinatory logic, with arbitrary restrictions on both the introduction and elimination rules for the connectives. Generally such a proof will involve terms without normal form and cut formulas, i.e. formulas formed by an introduction rule that are immediately removed by an elimination with at most some equality steps intervening. (Such a sequence of steps we call a “cut”.)

The above applies not only to the strong form of inconsistency defined above, but also to the weak form of inconsistency defined by: all propositions are provable, if this can be represented in the system.

Any inconsistency proof of this kind of system can be reduced to one where the major premise of the elimination rule involved in the cut and its deduction must also appear in the deduction of the minor premise involved in the cut.

We can, using this characterization of inconsistency proofs, put appropriate restrictions on certain introduction rules so that the systems, including a full classical propositional one, become provably consistent.

The results in this paper say that natural upper bounds for sets of degrees associated with theories and models of arithmetic cannot be minimal. The basic new result says that for any completion T of PA, there is another completion S such that S<TT and Rep(S) = Rep(T). This immediately implies that deg(T) is not minimal over {deg(X): X ∈ Rep(T)}. As an application of the basic result, we obtain the fact that if is a non-standard model of TA (true arithmetic), then deg () cannot be minimal over {deg(X): X is arithmetical}. More generally, if is a non-standard model of an arbitrary completion T of PA, then deg() cannot be minimal over {deg(): X ∈ Rep(T)}. We vary the basic result, making S′ ≡TT′. As an application of the variant, we obtain the fact that if is a non-standard model of PA, then {deg(): ≅ } has no minimal element.

The remainder of the present section gives a brief account of the background needed for the basic new result and the variant. These two results are proved in Section 2. The applications are given in Section 3, along with further background needed for the applications. One important source of ideas used in the present paper is a paper of Scott [9]. In addition, there are ideas taken from Tennenbaum [12], Feferman [3], Marker [6], [7], and Solovay. Chapter 19 of [1] gathers together most of this material. In fact, it contains all that is really essential. In one application, we appeal to Solovay's result on degrees of models of an arbitrary completion of PA, a result which is not completely proved in [1]. However, for the best application, which implies all the others, we use only some ideas from the proof of Solovay's theorem. These are given in lemmas that are proved in Section 3, where they are needed, or taken from [1], While the proof of Solovay's result requires an infinitely nested priority construction, our best application rests on nothing more than finite-injury constructions.

Answers are given to two questions concerning the existence of some sparse subsets of ℋ = {0, 1 … ., H – 1} ⊆ *ℕ. where H is a hyperfinite integer. In §1. we answer a question of Kanovei by showing that for a given cut U in ℋ, there exists a countably determined set X ⊆ ℋ which contains exactly one element in each U-monad, if and only if U = a · ℕ for some a Є ℋ ∖ {0}. In §2, we deal with a question of Keisler and Leth in [6]. We show that there is a cut V ⊆ ℋ such that for any cut U, (i) there exists a U-discrete set X ⊆ ℋ with X + X = ℋ (mod H) provided , (ii) there does not exist any U-discrete set X ⊆ ℋ with X + X = ℋ (mod H) provided . We obtain some partial results for the case U = V.

A logical calculus will be presented which not only is a formulation of a “basic logic” in the sense of the writer's previous papers, but which has the additional property that no weaker calculus can be a formulation of a basic logic. A sort of minimum logical calculus is thus attained, which has nothing superfluous about it for achieving the purpose for which it is designed.

In the case of some logical calculi the question can arise as to whether certain of the postulates are really logically valid and necessary. Sometimes a test is available, such as the truth-table test, enabling us to distinguish between logically valid sentences and others, but often no such test is available, especially where quantifiers are involved. Is or is not the axiom of infinity, for example, to be regarded as logically valid? Or is the principle of double negation really acceptable, even though it satisfies the truth-table test?

In [9], Yates proved the existence of a Turing degree a such that 0, 0′ are the only c.e. degrees comparable with it. By Slaman and Steel [7], every degree below 0′ has a 1-generic complement, and as a consequence, Yates degrees can be 1-generic, and hence can be low. In this paper, we prove that Yates degrees occur in every jump class.

In intuitionistic mathematics one distinguishes between sets with a constructive character and sets in a more general sense. The first kind consists of spreads and the latter of species. The definition of a spread utilizes so-called choice sequences (in [5] infinitely proceeding sequence or ips), i.e., sequences of well-determined mathematical objects which are chosen more or less freely. One can restrict the choices by some law, which, however, need not be predetermined (changing one's mind is allowed).

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 problem of changing the cofinality of a measurable cardinal to ω with the help of an iterated ultrapower construction has been introduced in [Bu] and more completely studied in [De]. The aim of this paper is to investigate how the construction above has to be changed to obtain an uncountable cofinality for the (previously) measurable cardinal.

A forcing approach of this question has been developed by Magidor in [Ma]. Just as in the countable case with Prikry forcing, it turns out that the needed hypothesis and the models constructed are the same in both techniques. However the ultrapowers yield a solution which may appear as more effective. In particular the sequence used to change the measurable cardinal into a cardinal of cofinality α has the property that for any β < α the restriction to β of this sequence can be used to change the cofinality of the (same) measurable cardinal to β.

The result we prove is as follows:

Theorem. Assume that α is a limit ordinal, that (Uβ)β<α is a sequence of complete ultrafilters on κ > α in the model N0, andfor B included in α let NB be the ultrapower of N0 by those Uβ which are such that β is in B.

Let L be a countable first-order language and L(Q) be obtained by adjoining an additional quantifier Q. Q is a generalization of the quantifier “there exists uncountably many x such that…” which was introduced by Mostowski in [4]. The logic of this latter quantifier was formalized by Keisler in [2]. Krivine and McAloon [3] considered quantifiers satisfying some but not all of Keisler's axioms. They called a formula φ(x) countable-like if

for every ψ. In Keisler's logic, φ(x) being countable-like is the same as ℳ⊨┐Qxφ(x). The main theorem of [3] states that any countable model ℳ of L[Q] has an elementary extension N, which preserves countable-like formulas but no others, such that the only sets definable in both N and M are those defined by formulas countable-like in M. Suppose C(x) in M is linearly ordered and noncountable-like but with countable-like proper segments. Then in N, C will have new elements greater than all “old” elements but no least new element — otherwise it will be definable in both models. The natural question is whether it is possible to use generalized quantifiers to extend models elementarily in such a way that a noncountable-like formula C will have a minimal new element. There are models and formulas for which it is not possible. For example let M be obtained from a minimal transitive model of ZFC by letting Qxφ(x) mean “there are arbitrarily large ordinals satisfying φ”.

A structure of finite signature is constructed so that: for all existential formulas and for all tuples of elements of the same length as the tuple one can decide in a quadratic time depending only on the length of the formula, if holds in the structure. In other words, the structure satisfies the relativized model-theoretic version of P=N P in the sense of [4]. This is a model-theoretical approach to results of Hemmerling and Gaßner.

We extend some recent results about bounded invariant equivalence relations and invariant subgroups of definable groups: we show that type-definability and smoothness are equivalent conditions in a wider class of relations than heretofore considered, which includes all the cases for which the equivalence was proved before.

As a by-product, we show some analogous results in purely topological context (without direct use of model theory).

We employ the lens provided by formal truth theory to study axiomatizations of Peano Arithmetic ${\textsf {(PA)}}$. More specifically, let Elementary Arithmetic ${\textsf {(EA)}}$ be the fragment $\mathsf {I}\Delta _0 + \mathsf {Exp}$ of ${\textsf {PA}}$, and let ${\textsf {CT}}^-[{\textsf {EA}}]$ be the extension of ${\textsf {EA}}$ by the commonly studied axioms of compositional truth ${\textsf {CT}}^-$. We investigate both local and global properties of the family of first order theories of the form ${\textsf {CT}}^-[{\textsf {EA}}] +\alpha $, where $\alpha $ is a particular way of expressing “${\textsf {PA}}$ is true” (using the truth predicate). Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to ${\textsf {PA}}$ and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of ${\textsf {PA}}$.