Natural deduction with general elimination rules

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates. Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. Received: 1 December 1998 / Revised version: 30 June 2000 / Published online: 18 July 2001     

On the weak Freese–Nation property of ?(ω)

Continuing [6], [8] and [16], we study the consequences of the weak Freese-Nation property of (?(ω),⊆). Under this assumption, we prove that most of the known cardinal invariants including all of those appearing in Cichoń's diagram take the same value as in the corresponding Cohen model. Using this principle we could also strengthen two results of W. Just about cardinal sequences of superatomic Boolean algebras in a Cohen model. These results show that the weak Freese-Nation property of (?(ω),⊆) captures many of the features of Cohen models and hence may be considered as a principle axiomatizing a good portion of the combinatorics available in Cohen models. Received: 7 June 1999 / Revised version: 17 October 1999 /?Published online: 15 June 2001     

Near coherence and filter games

We investigate a two-player game involving pairs of filters on ω. Our results generalize a result of Shelah ([7] Chapter VI) dealing with applications of game theory in the study of ultrafilters. Received: 28 September 1998 / Published online: 25 January 2001     

Groupwise dense families

We show that the Filter Dichotomy Principle implies that there are exactly four classes of ideals in the set of increasing functions from the natural numbers. We thus answer two open questions on consequences of ? < ?. We show that ? < ? implies that ? = ?, and that Filter Dichotomy together with ? < ? implies ? < ?. The technical means is the investigation of groupwise dense sets, ideals, filters and ultrafilters. With related techniques we prove the new inequality ?≤ cf(?). Received: 9 October 1998 / Revised version: 18 August 1999 / Published online: 21 December 2000     

Two applications of Boolean models

Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are a slight variation of ordinary first-order models, where truth values are now regular ideals of a given Boolean algebra. Two examples are presented: a simple conservativity result and Herbrand's theorem. Received December 5, 1995     

A version of the Jensen–Johnsbråten coding at arbitrary level n≥ 3

We generalize, on higher projective levels, a construction of “incompatible” generic Δ¹ ₃ real singletons given by Jensen and Johnsbr?ten. Received: 3 November 1998 / Revised version: 23 April 2000 / Published online: 3 October 2001     

Explaining the Gentzen–Takeuti reduction steps: a second-order system

Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π¹ ₁-CA) in terms of the more perspicious infinitary approach from [BS88]. Received: 27 April 1999 / Published online: 21 March 2001     

Meeting infinitely many cells of a partition once

We investigate several versions of a cardinal characteristic defined by Frankiewicz. Vojtáš showed , and Blass showed . We show that all the versions coincide and that is greater than or equal to the splitting number. We prove the consistency of and of . Received: 2 October 1996 / Revised version: 22 May 1997     

The Karp complexity of unstable classes

A class K of structures is controlled if, for all cardinals λ, the relation of L _∞,λ-equivalence partitions K into a set of equivalence classes (as opposed to a proper class). We prove that the class of doubly transitive linear orders is controlled, while any pseudo-elementary class with the ω-independence property is not controlled. Received: 23 September 1998 / Revised version: 6 July 1999 / Published online: 21 December 2000     

On some configurations related to the Shelah Weak Hypothesis

We show that some cardinal arithmetic configurations related to the negation of the Shelah Weak Hypothesis and natural from the forcing point of view are impossible. Received: 8 September 1999 / Published online: 3 October 2001     

A new condition number for linear programming

In this paper we define a new condition number ?(A) for the following problem: given a m by n matrix A, find x∈ℝ ⁿ , s.t. Ax<0. We characterize this condition number in terms of distance to ill-posedness and we compare it with existing condition numbers for the same problem. Received: November 5, 1999 / Accepted: November 2000?Published online September 17, 2001     

On the first Hochschild cohomology group of an algebra

Let A≡KΔ /I be a factor of a path algebra. We develop a strategy to compute dim H ¹(A), the dimension of the first Hochschild cohomology group of A, using combinatorial data from (Δ,I). That allows us to connect dim H ¹(A) with the rank and p-rank of the fundamental group π₁(Δ,I) of (Δ,I). We get explicit formulae for dim H ¹(A), when every path in Δ parallel to an arrow belongs to I or when I is homogeneous. Received: 12 April 1999 / Revised version: 9 October 2000     

An elementary proof of strong normalization for intersection types

We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly normalizing terms of pure lambda calculus can be characterized in this system, but also that a straightforward modification of its rules allows to characterize the set of weakly normalizing terms. Received: 15 June 1998 / Revised version: 15 November 1999 / Published online: 15 June 2001     

Density results in the Δ20 e-degrees

We show that the Δ⁰ ₂ enumeration degrees are dense. We also show that for every nonzero n-c. e. e-degree a, with n≥ 3, one can always find a nonzero 3-c. e. e-degree b such that b < a on the other hand there is a nonzero ωc. e. e-degree which bounds no nonzero n-c. e. e-degree. Received: 13 June 2000 / Published online: 3 October 2001     

Source algebra equivalences for blocks¶of finite general linear groups over a fixed field

T. Jost proved that Donovan's conjecture holds for the unipotent blocks of the finite general linear groups over a fixed field. In this paper, we show that the Morita equivalences exhibited by Jost are in fact equivalences between the source algebras of the corresponding blocks, and thus that Puig's conjecture holds for the unipotent blocks of finite general groups over a fixed field. Received: 3 October 2000     

Distinguishing groupwise density numbers

We show that is consistent, where is the groupwise density number and is the groupwise density number for ideals. This answers a question of Heike Mildenberger. Partially supported by Grant-in-Aid for Scientific Research (C) 17540116, Japan Society for the Promotion of Science.     

On the filter of computably enumerable supersets of an r-maximal set

We study the filter ℒ^*(A) of computably enumerable supersets (modulo finite sets) of an r-maximal set A and show that, for some such set A, the property of being cofinite in ℒ^*(A) is still Σ⁰ ₃-complete. This implies that for this A, there is no uniformly computably enumerable “tower” of sets exhausting exactly the coinfinite sets in ℒ^*(A). Received: 6 November 1999 / Revised version: 10 March 2000 /?Published online: 18 May 2001     

A new proof of a theorem of Magidor

We give a new proof using iterated Prikry forcing of Magidor's theorem that it is consistent to assume that the least strongly compact cardinal is the least supercompact cardinal. Received: 8 December 1997 / Revised version: 12 November 1998     

Consistency of V = HOD with the wholeness axiom

The Wholeness Axiom (WA) is an axiom schema that can be added to the axioms of ZFC in an extended language , and that asserts the existence of a nontrivial elementary embedding . The well-known inconsistency proofs are avoided by omitting from the schema all instances of Replacement for j-formulas. We show that the theory ZFC + V = HOD + WA is consistent relative to the existence of an embedding. This answers a question about the existence of Laver sequences for regular classes of set embeddings: Assuming there is an -embedding, there is a transitive model of ZFC +WA + “there is a regular class of embeddings that admits no Laver sequence.” Received: 7 July 1998 / Revised version: 5 November 1998