This paper introduces valuation structures associated with preferential models. Based on KLM valuation structures, we present a canonical approach to obtain injective preferential models for any preferential relation satisfying the property INJ, and give uniform proofs of representation theorems for injective preferential relations appeared in the literature. In particular, we show that, in any propositional language (finite or infinite), a preferential inference relation satisfies INJ if and only if it can be represented by a standard preferential model. This conclusion generalizes the result obtained by Freund. In addition, we prove that, when the language is finite, our framework is sufficient to establish a representation theorem for any injective relation.

The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with (kn+1) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search.

By a classifiable theory we shall mean a theory which is superstable, without the dimensional order property, which has prime models over pairs. In order to define what we mean by unique decomposition, we remind the reader of several definitions and results. We adopt the usual conventions of stability theory and work inside a large saturated model of a fixed classifiable theory T; for instance, if we write M ⊆ N for models of T, M and N we are thinking of these models as elementary submodels of this fixed saturated models; so, in particular, M is an elementary submodel of N. Although the results will not depend on it, we will assume that T is countable to ease notation.

We do adopt one piece of notation which is not completely standard: if T is classifiable, M0 ⊆ Mi for i = 1, 2 are models of T and M1 is independent from M2 over M0 then we write M1M2 for the prime model over M1 ∪ M2.

We show that every finite lattice is embeddable into the Σ20 enumeration degrees via a lattice-theoretic embedding which preserves 0 and 1.

We show that Intuitionistic Open Induction iop is not closed under the rule DNS(Ǝ1). This is established by constructing a Kripke model of iop + ¬Ly(2y > x), where Ly(2y > x) is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA− plus the scheme of weak ¬¬ LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula φ(y) having only y free. (PA−)i ⊢ Lyφ(y). We observe that the theories iop, i∀1 and iΠ1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop.

A classical quantified modal logic is used to define a “feasible” arithmetic whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands ⃞∝ as “∝ is feasibly demonstrable”.

differs from a system that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., ⃞-free) formulas. Thus, is defined without any reference to bounding terms, and admitting induction over formulas having arbitrarily many alternations of unbounded quantifiers. The system also uses only a very small set of initial functions.

To obtain the characterization, one extends the Curry-Howard isomorphism to include modal operations. This leads to a realizability translation based on recent results in higher-type ramified recursion. The fact that induction formulas are not restricted in their logical complexity, allows one to use the Friedman A translation directly.

The development also leads us to propose a new Frege rule, the “Modal Extension” rule: if ⊢ ∝ a then ⊢ A↔ ∝ for new symbol A.

In the study of categories whose morphisms display a behaviour similar to that of partial functions, the concept of morphism domain is, obviously, central. In this paper an operation defined on morphisms describes those properties which are related to morphisms being regarded as abstractions of partial functions. This operation allows us to characterise the morphism domains directly, and gives rise to an algebra defined by a simple set of identities. No product-like categorical structures are needed therefore. We also develop the construction of topologies together with the notion of continuous morphism, in order to test the effectiveness of this approach. It is interesting to see how much of the computational character of the morphisms is translated into continuity.

After presenting a general setting in which to look at forcing axioms, we give a hierarchy of generalized bounded forcing axioms that correspond level by level, in consistency strength, with the members of a natural hierarchy of large cardinals below a Mahlo. We give a general construction of models of generalized bounded forcing axioms. Then we consider the bounded forcing axiom for a class of partially ordered sets Γ1 such that, letting Γ0 be the class of all stationary-set-preserving partially ordered sets, one can prove the following:

(a) Γ0 ⊆ Γ1,

(b) Γ0 = Γ1 if and only if NSω1 is ℵ1-dense.

(c) If P ∉ Γ1, then BFA({P}) fails.

We call the bounded forcing axiom for Γ1Maximal Bounded Forcing Axiom (MBFA). Finally we prove MBFA consistent relative to the consistency of an inaccessible Σ2-correct cardinal which is a limit of strongly compact cardinals.

We study the relationships between definitions of compactness in topological spaces and the roll the axiom of choice plays in these relationships.

The present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.

The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions.

We give a detailed description of the simulation of tq-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative.

We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e.. by only one specific combination, and structural rules.

We confirm a conjecture, about neat embeddings of cylindric algebras, made in 1969 by J. D. Monk, and a later conjecture by Maddux about relation algebras obtained from cylindric algebras. These results in algebraic logic have the following consequence for predicate logic: for every finite cardinal α ≥ 3 there is a logically valid sentence X, in a first-order language ℒ with equality and exactly one nonlogical binary relation symbol E, such that X contains only 3 variables (each of which may occur arbitrarily many times), X has a proof containing exactly α + 1 variables, but X has no proof containing only α variables. This solves a problem posed by Tarski and Givant in 1987.

If T is a model complete theory with the strict order property, then the theory of the models of T with an automorphism has no model companion.

We analyze the two cardinal properties of definable sets in homogeneous graphs.

We prove that every n-modal logic between Kn and S5n is undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the (undecidable) representation problem of finite relation algebras.

We give a model-theoretic proof of the fact that for all infinite Abelian groups P ≠ NP in the sense of binary nondeterminism. This result has been announced 1994 by Christine Gaßner.

We give a complete description of minimal groups infinitely definable in separably closed fields of finite degree of imperfection. In particular we answer positively the question of the existence of such a group with infinite transcendence degree (i.e., a minimal group with non thin generic).

In this article we provide wellordering proofs for metapredicative systems of explicit mathematics and admissible set theory featuring suitable axioms about the Mahloness of the underlying universe of discourse. In particular, it is shown that in the corresponding theories EMA of explicit mathematics and KPm0 of admissible set theory, transfinite induction along initial segments of the ordinal φω00, for φ being a ternary Veblen function, is derivable. This reveals that the upper bounds given for these two systems in the paper Jäger and Strahm [11] are indeed sharp.

We consider equational theories for functions denned via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S21. In particular this solves an open problem formulated by Takeuti (c.f. [5, p.5 problem 9.]).

We prove the consistency result from the title. By forcing we construct a model of g = ℵ1, b = cf(Sym(ω)) = ℵ2.