LetL0be a language on ℕ consisting of 0, 1, +, ∸, ·, ⌊½a⌋, ∣a∣, #, ∧(a,b), ∨(a,b), ¬(a), ≤ (a,b), andμx≤ ∣s∣t(x). Hereμx≤ ∣s∣t(x) is the smallest numberx≤ ∣s∣ satisfyingt(x) > 0 and 0 if there exist no suchxand we stipulate that ifsandt(a) are terms inLo, thenμx≤ ∣s∣t(x) is also a term inLo. The defining axioms of functions ∧(a,b), ∨(a,b), ¬(a), ≤ (a,b) are as follows:LetLa language on ℕ with only predicate constant = andL0⊆L. Letf(b,a1,…,am) be a function for ℕm+1into (...) ℕ. We say “fis weakly expressed by termst1(b,a1,…,am),…,tr(b,a1,…,am) inL” if for everyb,a1,…,am∈ ℕ,f(b,a1,…,am) is equal to one ofti(b,a1, …,am). The critical number ofbinfwith respect toLis the minimum numbernsuch that wheneverf(b,a1,…,an) is weakly expressed by termst1(b,a1, …,an),…, the number of occurrences ofbin someti(b,a1,…,an) is at leastn.As is defined in [1], a functionfis defined by a limited iteration fromgandhwith respect toLiff the following holds: Letτbe defined aswith the condition; andis defined bywhereandare terms inL. We say “fis defined by a short limited iteration fromgandh” ifis defined bywhereτ,s, tare the same as above satisfying the condition. (shrink)

In this paper, we develop the system LZF of set theory with the unrestricted comprehension in full linear logic and show that LZF is a conservative extension of ZF– i.e., the Zermelo-Fraenkel set theory without the axiom of regularity. We formulate LZF as a sequent calculus with abstraction terms and prove the partial cut-elimination theorem for it. The cut-elimination result ensures the subterm property for those formulas which contain only terms corresponding to sets in ZF–. This implies that LZF is (...) a conservative extension of ZF– and therefore the former is consistent relative to the latter. (shrink)

We define theories of bounded arithmetic, whose definable functions and relations are exactly those in certain complexity classes. Based on a recursion-theoretic characterization of NC in Clote , the first-order theory TNC, whose principal axiom scheme is a form of short induction on notation for nondeterministic polynomial-time computable relations, has the property that those functions having nondeterministic polynomial-time graph Θ such that TNC x y Θ are exactly the functions in NC, computable on a parallel random-access machine in polylogarithmic parallel (...) time with a polynomial number of processors.0 We then define three theories of weak second-order arithmetic which respectively characterize relations in the classes of alternating logarithmic time, logspace and nondeterministic logspace. (shrink)

T i 2 = S i +1 2 implies ∑ p i +1 ⊆ Δ p i +1 ⧸poly. S 2 and IΔ 0 ƒ are not finitely axiomatizable. The main tool is a Herbrand-type witnessing theorem for ∃∀∃ П b i -formulas provable in T i 2 where the witnessing functions are □ p i +1.

In [10], we have shown that the statement that all ∑ 1 1 partitions are Ramsey is deducible over ATR 0 from the axiom of ∑ 1 1 monotone inductive definition,but the reversal needs П 1 1 - CA 0 rather than ATR 0 . By contrast, we show in this paper that the statement that all ∑ 0 2 games are determinate is also deducible over ATR 0 from the axiom of ∑ 1 1 monotone inductive definition, but the (...) reversal is provable even in ACA 0 . These results illuminate the substantial differences among lightface theorems which can not be observed in boldface. (shrink)

We study L∞κ-freeness in the variety of Boolean algebras. It is shown that some of the theorems on L∞κ-free algebras which are known to hold in varieties such as groups, abelian groups etc. are also true for Boolean algebras. But we also investigate properties such as the ccc of L∞κ-free Boolean algebras which have no counterpart in the varieties above.

Let f ϵ Z [ X, Y ] be irreducible. We give a condition that there are only finitely many integers n ϵ Z such that f is reducible and we give a bound for such integers. We prove a similar result for polynomials with coefficients in polynomial rings. Both results are proved by, so-called, nonstandard arithmetic.

We give a simple game-theoretic proof of Silver's theorem that every analytic set is Ramsey. A set P of subsets of ω is called Ramsey if there exists an infinite set H such that either all infinite subsets of H are in P or all out of P. Our proof clarifies a strong connection between the Ramsey property of partitions and the determinacy of infinite games.

The notion of an entangled linear order gives a useful method to construct counter examples for such problems as the productivity of chain conditions, the square bracket partition relation and the existence of a large size monotonic subfunction. In particular, if there exists and ℵ1-entangled linear order then some consequences ofMA ℵ 1 or of wOCA fail. So, in which model ofZFC does an ℵ1-entangled linear order exist? Todorcevic [6] has shown if cf2ℵ 0=ω1 then there is an ℵ1-entangled linear (...) order of size ℵ1. And it is widely known that adding κ many Cohen reals adds such a linear order of size κ. In this note it is shown that adding asingle Cohen real is sufficient to get a maximal size ℵ1-entangled linear order. (shrink)

We give a proof of Gödel's first incompleteness theorem based on Berry's paradox, and from it we also derive the second incompleteness theorem model-theoretically.

Within a weak subsystem of second-order arithmetic , that is -conservative over , we reformulate Kreisel's proof of the Second Incompleteness Theorem and Boolos' proof of the First Incompleteness Theorem.

An ordered field is said to be Scott complete iff it is complete with respect to its uniform structure. Zakon has asked whether nonstandard real lines are Scott complete. We prove in ZFC that for any complete Boolean algebra B which is not (ω, 2)-distributive there is an ultrafilter U of B such that the Boolean ultrapower of the real line modulo U is not Scott complete. We also show how forcing in set theory gives rise to examples of Boolean (...) ultrapowers of the real line which are not Scott complete. (shrink)

In this note we treat maximal and minimal normal subgroups of a superstable group and prove that these groups are definable under certain conditions. Main tool is a superstable version of Zil'ber's indecomposability theorem.

We prove the strong normalization theorem for the natural deduction system for the constructive arithmetic TRDB (the system with Definition by Transfinite Recursion and Bar induction), which was introduced by Yasugi and Hayashi. We also establish the consistency of this system, applying the strong normalization theorem.

We study the following conjecture. Conjecture. Let $T$ be an $\omega$-stable theory with continuum many countable models. Then either i) $T$ has continuum many complete extensions in $L_1$, or ii) some complete extension of $T$ in $L_1$ has continuum many $L_1$-types without parameters. By Shelah's proof of Vaught's conjecture for $\omega$-stable theories, we know that there are seven types of $\omega$-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. (shrink)

We investigate the second order bounded arithmetical systems which is isomorphic to TAC i , TNC i or TLS.

We give an extender characterization of a very strong elementary embedding between transitive models of set theory, whose existence is known as the axiom I2. As an application, we show that the positive solution of a partition problem raised by Magidor would refute it.

We show that K-generic projective planes have Morley rank either two or infinity. We also show give a direct argument that such planes are not Desarguesian.

In this, journal, W. Buchholz gave an elegant proof of a characterization theorem for provably total recursive functions in the theory IDv for the v-times iterated inductive definitions . He characterizes the classes of functions by Hardy functions. In this note we will show that a slow growing analogue to the theorem can be obtained by a slight modification of Buchholz' proof.

A partial map f of a structure M is called almost total if |M — dom| = |M — ran| < ω. We study a difference between an almost total elementary map and an automorphism.