Search

In this paper, the positive fragment of the logic [ABSTRACT FROM AUTHOR]

In this paper we prove that the first order theories of the free MV algebras with finitely many generators are different from each other. This answers to the MV algebra analogue of a well-known (now solved) problem of Tarski for groups. [ABSTRACT FROM AUTHOR]

The main result of this paper is Theorem [1.1], which shows that it is possible for derived models to satisfy [ABSTRACT FROM AUTHOR]

As far as algebraic properties are concerned, the usual addition on the class of ordinal numbers is not really well behaved; for example, it is not commutative, nor left cancellative etc. In a few cases, the natural Hessenberg sum is a better alternative, since it shares most of the usual properties of the addition on the naturals. A countably infinite iteration of the natural sum has been used in a recent paper by Väänänen and Wang, with applications to infinitary logics. We present a detailed study of this infinitary operation, showing that there are many similarities with the ordinary infinitary sum, providing an order theoretical characterization, and finding connections with certain kinds of infinite mixed sums. [ABSTRACT FROM AUTHOR]

In this paper we give characterizations of the stable and ℵ0-stable theories, in terms of an external property called representation. In the sense of the representation property, the mentioned classes of first-order theories can be regarded as 'not very complicated'. [ABSTRACT FROM AUTHOR]

Here we study properties of weakly circularly minimal cyclically ordered groups. The main result of the paper is that any weakly circularly minimal cyclically ordered group is abelian. [ABSTRACT FROM AUTHOR]

The purpose of this paper is to survey the correspondence between bounded arithmetic and propositional proof systems. In addition, it also contains some new results which have appeared as an extended abstract in the proceedings of the conference TAMC 2008 [11]. Bounded arithmetic is closely related to propositional proof systems; this relation has found many fruitful applications. The aim of this paper is to explain and develop the general correspondence between propositional proof systems and arithmetic theories, as introduced by Krajíček and Pudlák [46]. Instead of focusing on the relation between particular proof systems and theories, we favour a general axiomatic approach to this correspondence. In the course of the development we particularly highlight the role played by logical closure properties of propositional proof systems, thereby obtaining a characterization of extensions of EF in terms of a simple combination of these closure properties (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The present paper introduces and studies the variety WH of weakly Heyting algebras. It corresponds to the strict implication fragment of the normal modal logic K which is also known as the subintuitionistic local consequence of the class of all Kripke models. The tools developed in the paper can be applied to the study of the subvarieties of WH; among them are the varieties determined by the strict implication fragments of normal modal logics as well as varieties that do not arise in this way as the variety of Basic algebras or the variety of Heyting algebras. Apart from WH itself the paper studies the subvarieties of WH that naturally correspond to subintuitionistic logics, namely the variety of R-weakly Heyting algebras, the variety of T-weakly Heyting algebras and the varieties of Basic algebras and subresiduated lattices. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

This paper is concerned with topological set theory, and particularly with Skala's and Manakos' systems for which we give a topological characterization of the models. This enables us to answer natural questions about those theories, reviewing previous results and proving new ones. One of these shows that Skala's set theory is in a sense compatible with any ‘normal’ set theory, and another appears on the semantic side as a ‘Cantor theorem’ for the category of Alexandroff spaces. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The paper proposes a flexible way to build concepts within fuzzy logic and set theory. The framework is general enough to capture some important particular cases, with their own independent interpretations, like “antitone” or “isotone” concepts constructed from fuzzy binary relations, but also to allow the two universes (of objects and attributes) to be equipped each with its own truth structure. Perhaps the most important feature of our approach is that we do not commit ourselves to any kind of logical connector, covering thus the case of a possibly non-commutative conjunction too. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

This paper studies, with techniques of Abstract Algebraic Logic, the effects of putting a bound on the cardinality of the set of side formulas in the Deduction Theorem, viewed as a Gentzen-style rule, and of adding additional assumptions inside the formulas present in Modus Ponens, viewed as a Hilbert-style rule. As a result, a denumerable collection of new Gentzen systems and two new sentential logics have been isolated. These logics are weaker than the positive implicative logic. We have determined their algebraic models and the relationships between them, and have classified them according to several standard criteria of Abstract Algebraic Logic. One of the logics is protoalgebraic but neither equivalential nor weakly algebraizable, a rare situation where very few natural examples were hitherto known. In passing we have found new, alternative presentations of positive implicative logic, both in Hilbert style and in Gentzen style, and have characterized it in terms of the restricted Deduction Theorem: it is the weakest logic satisfying Modus Ponens and the Deduction Theorem restricted to at most 2 side formulas. The algebraic part of the work has lead to the class of quasi-Hilbert algebras, a quasi-variety of implicative algebras introduced by Pla and Verdú in 1980, which is larger than the variety of Hilbert algebras. Its algebraic properties reflect those of the corresponding logics and Gentzen systems. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Dual-intuitionistic logics are logics proposed by Czermak (1977), Goodman (1981) and Urbas (1996). It is shown in this paper that there is a correspondence between Goodman's dual-intuitionistic logic and Nelson's constructive logic N-. [ABSTRACT FROM AUTHOR]

In his long and illuminating paper [1] Joe Barback defined and showed to be non-vacuous a class of infinite regressive isols he has termed “complete y torre” (CT) isols. These particular isols a enjoy a property that Barback has since labelled combinatoriality. In [2], he provides a list of properties characterizing the combinatoria isols. In Section 2 of our paper, we extend this list of characterizations to include the fact that an infinite regressive isol X is combinatorial if and only if its associated Dekker semiring D (X) satisfies all those Π2 sentences of the anguage LN for isol theory that are true in the set ω of natural numbers. (Moreover, with X combinatorial, the interpretations in D(X)of the various function and relation symbols of LN via the “lifting ” to D(X) of their Σ1 definitions in ω coincide with their interpretations via isolic extension.) We also note in Section 2 that Π2(L)-correctness, for semirings D(X), cannot be improved to Π 3(L)-correctness, no matter how many additional properties we succeed in attaching to a combinatoria isol; there is a fixed ${\vec \forall} {\vec \exists} {\vec \forall}$(L) sentence that blocks such extension. (Here L is the usual basic first-order language for arithmetic.) In Section 3, we provide a proof of the existence of combinatorial isols that does not involve verification of the extremely strong properties that characterize Barback's CT isols. [ABSTRACT FROM AUTHOR]

Let T be the standard Veblen 1908 ordinal notation system for Γ0 as defined, for example, in Schütte's 1977 textbook [13] on Proof Theory. We define a slight modification of the standard assignment of fundamental sequences for the limit ordinals in T and prove that Γ0 is subrecursively inaccessible for this assignment, i.e. the induced slow and fast growing hierarchy match up at Γ0 for the first time.The results of this paper also indicate that ϕℇ00 may be considered as a new slow growing ordinal of PA in the sense that the induced slow growing hierarchy up to ϕℇ00 classifies the PA-provablyrecursive functions.We show how the results of this paper can be used to bui d a subrecursive hierarchyover the predicative ordinals in the spirit of Wainer's 1970 abstract [16 ]. [ABSTRACT FROM AUTHOR]

The purpose of this paper is to explore the relationship between IΔ0 + exp and its weaker subtheories. We give a method of translating certain classes of IΔ0 + exp proofs into weaker systems of arithmetic such as Buss' systems S2. We show if IEi (exp) ⊢ A with a proof P of expind-rank(P) ≤ n + 1where all (∀ ≤: right) or (∃ ≤: left) have bounding terms not containing function symbols, then Si2 ⊇ IEi,2 ⊢ An. Here A is not necessarily a bounded formula. For IOpen(exp) we prove a similar result. Using our translations we show IOpen(exp) ⊊ IΔ0(exp). Here IΔ0(exp) is a conservative extension of IΔ0 + exp obtained by adding to IΔ0 a symbol for 2 x to the language as well as defining axioms for it. [ABSTRACT FROM AUTHOR]

In this paper we prove a bounded translation of intuitionistic propositional logic into basic propositional logic. Our new theorem, compared with the translation theorem in [1], has the advantage that it gives an effective bound on the translation, depending on the complexity of formulas. [ABSTRACT FROM AUTHOR]

In this paper, we generalize a result of Brown and Simpson [1] to prove that RCA0+Π0∞-BCT is conservative over RCA0 with respect to the set of formulae in the form ∃!Xϕ(X), where ϕ is arithmetical. We also consider the conservation of Π00∞-BCT over Σb1-NIA+∇b1-CA. [ABSTRACT FROM AUTHOR]

A table of contents for the June 2009 issue of "Mathematical Logic Quarterly" is presented.

In this paper we shall introduce the variety WQS of weak-quasi-Stone algebras as a generalization of the variety QS of quasi-Stone algebras introduced in [9]. We shall apply the Priestley duality developed in [4] for the variety N of ¬-lattices to give a duality for WQS. We prove that a weak-quasi-Stone algebra is characterized by a property of the set of its regular elements, as well by mean of some principal lattice congruences. We will also determine the simple and subdirectly irreducible algebras (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

This paper studies systems of explicit mathematics as introduced by Feferman [9, 11]. In particular, we propose weak explicit type systems with a restricted form of elementary comprehension whose provably terminating operations coincide with the functions on binary words that are computable in polynomial time. The systems considered are natural extensions of the first-order applicative theories introduced in Strahm [19, 20] (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper we study the logical strength of the determinacy of infinite binary games in terms of second order arithmetic. We define new determinacy schemata inspired by the Wadge classes of Polish spaces and show the following equivalences over the system RCA0*, which consists of the axioms of discrete ordered semi-rings with exponentiation, Δ10 comprehension and Π00 induction, and which is known as a weaker system than the popularbase theory RCA0: 1. Bisep(Δ10, Σ10)-Det* ↔ WKL0,2. Bisep(Δ10, Σ20)-Det* ↔ ATR0 + Σ11 induction,3. Bisep(Σ10, Σ20)-Det* ↔ Sep(Σ10, Σ20)-Det* ↔ Π11-CA0,4. Bisep(Δ20, Σ20)-Det* ↔ Π11-TR0, where Det* stands for the determinacy of infinite games in the Cantor space (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

This paper is concerned with implicit computational complexity of the exptime computable functions. Modifying the lexicographic path order, we introduce a path order EPO. It is shown that a termination proof for a term rewriting system via EPO implies an exponential bound on the lengths of derivations. The path order EPO is designed so that every exptime function is representable as a term rewrite system compatible with EPO (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper we study the category of hyper MV-algebras and we prove that it has a terminal object and a coequalizer. We show that Jia's construction can be modified to provide a free hyper MV-algebra by a set. We use this to show that in the category of hyper MV-algebras the monomorphisms are exactly the one-to-one homomorphisms. (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In [10] it is claimed that the set of predicate tautologies of all complete BL-chains and the set of all standard tautologies (i. e., the set of predicate formulas valid in all standard BL-algebras) coincide. As noticed in [11], this claim is wrong. In this paper we show that a complete BL-chain B satisfies all standard BL-tautologies iff for any transfinite sequence (ai: i ∈ I) of elements of B, the condition ∧i ∈ I (a2i) = (∧i ∈ Iai)2 holds in B. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper, we investigate definable models of Peano Arithmetic PA in a model of PA. For any definable model N without parameters in a model M, we show that N is isomorphic to M if M is elementary extension of the standard model and N is elementarily equivalent to M. On the other hand, we show that there is a model M and a definable model N with parameters in M such that N is elementarily equivalent to M but N is not isomorphic to M. We also show that there is a model M and a definable model N with parameters in M such that N is elementarily equivalent to M, and N is isomorphic to M, but N is not definably isomorphic to M. And also, we give a generalization of Tennenbaum's theorem. At the end, we give a new method to construct a definable model by a refinement of Kotlarski's method. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In his Ph.D. thesis [7], L. van den Dries studied the model theory of fields (more precisely domains) with finitely many orderings and valuations where all open sets according to the topology defined by an order or a valuation is globally dense according with all other orderings and valuations. Van den Dries proved that the theory of these fields is companionable and that the theory of the companion is decidable (see also [8]). In this paper we study the case where the fields are expanded with finitely many orderings and an independent derivation. We show that the theory of these fields still admits a model companion in the language LD<,m= {+, –, ·, D, <1, ..., <m, 1, 0}. We denote this model companion by CODFm and give a geometric axiomatization of this theory which uses basic notions of algebraic geometry and some generalized open subsets which appear naturally in this context. This axiomatization allows to recover (just by putting m = 1) the one given in [4] for the theory CODF of closed ordered differential fields. Most of the technics we use here are already present in [2] and [4]. Finally, we prove that it is possible to describe the completions of CODFm and to obtain quantifier elimination in a slightly enriched (infinite) language. This generalizes van den Dries' results in the “derivation free” case. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Let f, g ∈ ωω . We will denote by g ≫ f that for every k < ω, f (nk) ≤ g (n ) except for finitely many n . The ideal ℐf on ω2 is the collection of sets X such that, for some g ≫ f and τ ∈ ∏n <ωg (n )2, every x ∈ X satisfies τ (n ) ⊂ x for infinitely many n . In the present paper, we will prove the consistency of cov(ℐf) < &cfr; and non(ℐf) < &cfr;. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

We reconsider some classical natural semantics of integers (namely iterators of functions, cardinals of sets, index of equivalence relations) in the perspective of Kolmogorov complexity. To each such semantics one can attach a simple representation of integers that we suitably effectivize in order to develop an associated Kolmogorov theory. Such effectivizations are particular instances of a general notion of “self-enumerated system” that we introduce in this paper. Our main result asserts that, with such effectivizations, Kolmogorov theory allows to quantitatively distinguish the underlying semantics. We characterize the families obtained by such effectivizations and prove that the associated Kolmogorov complexities constitute a hierarchy which coincides with that of Kolmogorov complexities defined via jump oracles and/or infinite computations (cf. [6]). This contrasts with the well-known fact that usual Kolmogorov complexity does not depend (up to a constant) on the chosen arithmetic representation of integers, let it be in any base n ≥ 2 or in unary. Also, in a conceptual point of view, our result can be seen as a mean to measure the degree of abstraction of these diverse semantics. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The present paper introduces and studies the variety &Wscr;&Hscr;n of n-linear weakly Heyting algebras. It corresponds to the algebraic semantic of the strict implication fragment of the normal modal logic K with a generalization of the axiom that defines the linear intuitionistic logic or Dummett logic. Special attention is given to the variety &Wscr;&Hscr;2 that generalizes the linear Heyting algebras studied in [10] and [12], and the linear Basic algebras introduced in [2]. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

A well known theorem proved (independently) by J. Paris and H. Friedman states that BΣn +1 (the fragment of Arithmetic given by the collection scheme restricted to Σn +1-formulas) is a Πn +2-conservative extension of IΣn (the fragment given by the induction scheme restricted to Σn-formulas). In this paper, as a continuation of our previous work on collection schemes for Δn +1(T )-formulas (see [4]), we study a general version of this theorem and characterize theories T such that T + BΣn +1 is a Πn +2-conservative extension of T . We prove that this conservativeness property is equivalent to a model-theoretic property relating Πn-envelopes and Πn-indicators for T . The analysis of Σn +1-collection we develop here is also applied to Σn +1-induction using Parsons' conservativeness theorem instead of Friedman-Paris' theorem. As a corollary, our work provides new model-theoretic proofs of two theorems of R. Kaye, J. Paris and C. Dimitracopoulos (see [8]): BΣn +1 and IΣn +1 are Σn +3-conservative extensions of their parameter free versions, BΣ–n +1 and IΣ–n +1. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Given a π -institution I , a hierarchy of π -institutions I(n ) is constructed, for n ≥ 1. We call I(n ) the n-th order counterpart of I . The second-order counterpart of a deductive π -institution is a Gentzen π -institution, i.e. a π -institution associated with a structural Gentzen system in a canonical way. So, by analogy, the second order counterpart I(2) of I is also called the “Gentzenization” of I . In the main result of the paper, it is shown that I is strongly Gentzen , i.e. it is deductively equivalent to its Gentzenization via a special deductive equivalence, if and only if it has the deduction-detachment property . (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Generalizing model companions from model theory we define companions of pieces of canonical partitions of Polish G-spaces. This unifies several constructions from logic. The central problem of the paper is the existence of companions which form a G-orbit which is a Gδ-set. We describe companions of some typical G-spaces. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

It is known that there is a close relation between Prikry forcing and the iteration of ultrapowers: If U is a normal ultrafilter on a measurable cardinal κ and 〈Mn, jm,n | m ≤ n ≤ ω〉 is the iteration of ultrapowers of V by U, then the sequence of critical points 〈j0,n(κ) | n ∈ ω〉 is a Prikry generic sequence over Mω. In this paper we generalize this for normal precipitous filters. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In Aczel [1], the existence of largest (written “greatest” in Barwise and Moss [2]) fixed points of set continuous operators is proved assuming the schema version of dependent choices in Zermelo-Fraenkel set theory without the axiom of Foundation. In the present paper, we study whether the existence of largest fixed points of set continuous operators is provable without the schema version of dependent choices, using Boffa's weak antifoundation axioms. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The present paper proposes a generalisation of the notion of disjunctive (or rich) sequence, that is, of an infinite sequence of letters having each finite sequence as a subword. Our aim is to give a reasonable notion of disjunctiveness relative to a given set of sequences F. We show that a definition like “every subword which occurs at infinitely many different positions in sequences in F has to occur infinitely often in the sequence” fulfils properties similar to the original unrelativised notion of disjunctiveness. Finally, we investigate our concept of generalised disjunctiveness in spaces of Cantor expansions of reals. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Let h : ℕ → ℚ be a computable function. A real number x is called h-monotonically computable (h-mc, for short) if there is a computable sequence (xs) of rational numbers which converges to x h-monotonically in the sense that h(n)|x – xn| ≥ |x – xm| for all n andm > n. In this paper we investigate classes h-MC of h-mc real numbers for different computable functions h. Especially, for computable functions h : ℕ → (0, 1)ℚ, we show that the class h-MC coincides with the classes of computable and semi-computable real numbers if and only if Σi∈ℕ(1 – h(i)) = ∞and the sum Σi∈ℕ(1 – h(i)) is a computable real number, respectively. On the other hand, if h(n) ≥ 1 and h converges to 1, then h-MC = SC (the class of semi-computable reals) no matter how fast h converges to 1. Furthermore, for any constant c > 1, if h is increasing and converges to c, then h-MC = c-MC. Finally, if h is monotone and unbounded, then h-MC contains all ω-mc real numbers which are g-mc for some computable function g. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

This paper concerns intermediate structure lattices Lt(&Nscr;/&Mscr;), where &Nscr; is an almost minimal elementary end extension of the model &Mscr; of Peano Arithmetic. For the purposes of this abstract only, let us say that &Mscr; attains L if L ≅ Lt(&Nscr;/&Mscr;) for some almost minimal elementary end extension of &Nscr;. If T is a completion of PA and L is a finite lattice, then: (A) If some model of T attains L, then every countable model of T does. (B) If some rather classless, ℵ1-saturated model of T attains L, then every model of T does. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper, we discuss uniform versions of some axioms of second order arithmetic in the context of higher order arithmetic. We prove that uniform versions of weak weak König's lemma WWKL and Σ01 separation are equivalent to (∃2) over a suitable base theory of higher order arithmetic, where (∃2) is the assertion that there exists Φ2 such that Φf1 = 0 if and only if ∃x0(fx = 0) for all f. We also prove that uniform versions of some well-known theorems are equivalent to (∃2) or the axiom (Suslin) of the existence of the Suslin operator. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

A real α is called a c. e. real if it is the halting probability of a prefix free Turing machine. Equivalently, α is c. e. if it is left computable in the sense that L(α) = {q ∈ ℚ : q ≤ α} is a computably enumerable set. The natural field formed by the c. e. reals turns out to be the field formed by the collection of the d. c. e. reals, which are of the form α—β, where α and β are c. e. reals. While c. e. reals can only be found in the c. e. degrees, Zheng has proven that there are Δ02 degrees that are not even n-c. e. for any n and yet contain d. c. e. reals, where a degree is n-c. e. if it contains an n-c. e. set. In this paper we will prove that every ω-c. e. degree contains a d. c. e. real, but there are ω + 1-c. e. degrees and, hence Δ02 degrees, containing no d. c. e. real. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

The computability of reals was introduced by Alan Turing [20] by means of decimal representations. But the equivalent notion can also be introduced accordingly if the binary expansion, Dedekind cut or Cauchy sequence representations are considered instead. In other words, the computability of reals is independent of their representations. However, as it is shown by Specker [19] and Ko [9], the primitive recursiveness and polynomial time computability of the reals do depend on the representation. In this paper, we explore how the weak computability of reals depends on the representation. To this end, we introduce three notions of weak computability in a way similar to the Ershov's hierarchy of Δ02-sets of natural numbers based on the binary expansion, Dedekind cut and Cauchy sequence, respectively. This leads to a series of classes of reals with different levels of computability. We investigate systematically questions as on which level these notions are equivalent. We also compare them with other known classes of reals like c. e. and d-c. e. reals. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper we give an axiomatisation of the concept of a computability structure with partial sequences on a many-sorted metric partial algebra, thus extending the axiomatisation given by Pour-El and Richards in [9] for Banach spaces. We show that every Banach-Mazur computable partial function from an effectively separable computable metric partial Σ-algebra A to a computable metric partial Σ-algebra B must be continuous, and conversely, that every effectively continuous partial function with semidecidable domain and which preserves the computability of a computably enumerable dense set must be computable. Finally, as an application of these results we give an alternative proof of the first main theorem for Banach spaces first proved by Pour-El and Richards. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

In this paper we propose a Kripke-style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

We study the situation when the automorphism group of a recursively saturated structure acts on an ℝ-tree. The cases of (ℚ, <) and models of Peano Arithmetic are central in the paper. (© 2003 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

A basic result in intuitionism is Π02-conservativity. Take any proof p in classical arithmetic of some Π02-statement (some arithmetical statement ∀x.∃y.P(x, y), with P decidable). Then we may effectively turn p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof p of an arithmetical statement ∀x.∃y.P(x, y), with P of degree k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree k formulas. When k = 0, we get the original conservativity result as particular case. This result was a by-product of a semantical construction. J. Avigad of Carnegie Mellon University, found a short, direct syntactical derivation of the same result, using H. Friedman's A-translation. His proof is included here with his permission. (© 2003 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

There are two versions of the Proper Iteration Lemma. The stronger (but less well-known) version can be used to give simpler proofs of iteration theorems (e.g., [7, Lemma 24] versus [9, Theorem IX.4.7]). In this paper we give another demonstration of the fecundity of the stronger version by giving a short proof of Shelah's theorem on the preservation of the ωω-bounding property. (© 2003 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Derndinger [2] and Krupa [5] defined the F-product of a (strongly continuous one-parameter) semigroup (of linear operators) and presented some applications (e. g. to spectral theory of positive operators, cf. [3]). Wolff (in [7] and [8]) investigated some kind of nonstandard analogon and applied it to spectral theory of group representations. The question arises in which way these constructions are related. In this paper we show that the classical and the nonstandard F-product are isomorphic (Theorem 2.6). We also prove a little “classical” corollary (2.7.). (© 2003 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]