Primal logic arose in access control; it has a remarkably efficient (linear time) decision procedure for its entailment problem. But primal logic is a general logic of information. In the realm of arbitrary items of information (infons), conjunction, disjunction, and implication may seem to correspond (set-theoretically) to union, intersection, and relative complementation. But, while infons are closed under union, they are not closed under intersection or relative complementation. It turns out that there is a systematic transformation of propositional intuitionistic calculi to the original (propositional) primal calculi; we call it flatting. We extend flatting to quantifier rules, obtaining arguably the right quantified primal logic (QPL). The QPL entailment problem is exponential-time complete, but it is polynomial-time complete in the case, of importance to applications (at least to access control), where the number of quantifiers is bounded.

Abstract Topological quantum computation employs two-dimensional quasiparticles called anyons. The generally accepted mathematical basis for the theory of anyons is the framework of modular tensor categories. That framework involves a substantial amount of category theory and is, as a result, considered rather difficult to understand. Is the complexity of the present framework necessary? The computations of associativity and braiding matrices can be based on a much simpler framework, which looks less like category theory and more like familiar algebra. We introduce that framework here.

Abstract We study ultrafilters onω2produced by forcing with the quotient of ${\cal P}$ (ω2) by the Fubini square of the Fréchet filter onω. We show that such an ultrafilter is a weak P-point but not a P-point and that the only nonprincipal ultrafilters strictly below it in the Rudin–Keisler order are a single isomorphism class of selective ultrafilters. We further show that it enjoys the strongest square-bracket partition relations that are possible for a non-P-point. We show that it is not basically generated but that it shares with basically generated ultrafilters the property of not being at the top of the Tukey ordering. In fact, it is not Tukey-above [ω1]<ω, and it has only continuum many ultrafilters Tukey-below it. A tool in our proofs is the analysis of similar (but not the same) properties for ultrafilters obtained as the sum, over a selective ultrafilter, of nonisomorphic selective ultrafilters.

We propose an extension of the behavioral theory of interactive sequential algorithms to deal with the following situation. A query is issued during a certain step, but the step ends before any reply is received. Later, a reply arrives, and later yet the algorithm makes use of this reply. By a persistent query, we mean a query for which a late reply might be used. Our proposal involves issuing, along with a persistent query, a location where a late reply is to be stored. After presenting our proposal in general terms, we discuss the modifications that it requires in the existing axiomatics of interactive sequential algorithms and in the existing syntax and semantics of abstract state machines. To make that discussion self-contained, we include a summary of this material before the modifications. Fortunately, only rather minor modifications are needed.

The following known observation is useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U 1 ,…, U n then R is well-founded. A question arises how to bound the ordinal height | R | of the relation R in terms of the ordinals α i = | U i |. We introduce the notion of the stature ∥ P ∥ of a well partial ordering P and show that | R | ≤ ∥α 1 × … × α n ∥ and that this bound is tight. The notion of stature is of considerable independent interest. We define ∥ P ∥ as the ordinal height of the forest of nonempty bad sequences of P , but it has many other natural and equivalent definitions. In particular, ∥ P ∥ is the supremum, and in fact the maximum, of the lengths of linearizations of P . And ∥α 1 × … × α n ∥ is equal to the natural product α 1 ⊗ … ⊗ α n .

We consider parallel algorithms working in sequential global time, for example, circuits or parallel random access machines (PRAMs). Parallel abstract state machines (parallel ASMs) are such parallel algorithms, and the parallel ASM thesis asserts that every parallel algorithm is behaviorally equivalent to a parallel ASM. In an earlier article, we axiomatized parallel algorithms, proved the ASM thesis, and proved that every parallel ASM satisfies the axioms. It turned out that we were too timid in formulating the axioms; they did not allow a parallel algorithm to create components on the fly. This restriction did not hinder us from proving that the usual parallel models, like circuits or PRAMs or even alternating Turing machines, satisfy the postulates. But it resulted in an error in our attempt to prove that parallel ASMs always satisfy the postulates. To correct the error, we liberalize our axioms and allow on-the-fly creation of new parallel components. We believe that the improved axioms accurately express what parallel algorithms ought to be. We prove the parallel thesis for the new, corrected notion of parallel algorithms, and we check that parallel ASMs satisfy the new axioms.

In earlier work, the Abstract State Machine Thesis -- that arbitrary algorithms are behaviorally equivalent to abstract state machines -- was established for several classes of algorithms, including ordinary, interactive, small-step algorithms. This was accomplished on the basis of axiomatizations of these classes of algorithms. Here we extend the axiomatization and, in a companion paper, the proof, to cover interactive small-step algorithms that are not necessarily ordinary. This means that the algorithms (1) can complete a step without necessarily waiting for replies to all queries from that step and (2) can use not only the environment's replies but also the order in which the replies were received.

In earlier work, the Abstract State Machine Thesis -- that arbitrary algorithms are behaviorally equivalent to abstract state machines -- was established for several classes of algorithms, including ordinary, interactive, small-step algorithms. This was accomplished on the basis of axiomatizations of these classes of algorithms. In Part I (Interactive Small-Step Algorithms I: Axiomatization), the axiomatization was extended to cover interactive small-step algorithms that are not necessarily ordinary. This means that the algorithms (1) can complete a step without necessarily waiting for replies to all queries from that step and (2) can use not only the environment's replies but also the order in which the replies were received. In order to prove the thesis for algorithms of this generality, we extend here the definition of abstract state machines to incorporate explicit attention to the relative timing of replies and to the possible absence of replies. We prove the characterization theorem for extended abstract state machines with respect to general algorithms as axiomatized in Part I.

This is the second in a series of three articles extending the proof of the Abstract State Machine Thesis---that arbitrary algorithms are behaviorally equivalent to abstract state machines---to algorithms that can interact with their environments during a step, rather than only between steps. As in the first article of the series, we are concerned here with ordinary, small-step, interactive algorithms. This means that the algorithms: (1) proceed in discrete, global steps, (2) perform only a bounded amount of work in each step, (3) use only such information from the environment as can be regarded as answers to queries, and (4) never complete a step until all queries from that step have been answered. After reviewing the previous article's formal description of such algorithms and the definition of behavioral equivalence, we define ordinary, interactive, small-step abstract state machines (ASMs). Except for very minor modifications, these are the machines commonly used in the ASM literature. We define their semantics in the framework of ordinary algorithms and show that they satisfy the postulates for these algorithms. This material lays the groundwork for the final article in the series, in which we shall prove the Abstract State Machine thesis for ordinary, intractive, small-step algorithms: All such algorithms are equivalent to ASMs.

This is the third in a series of three articles extending the proof of the Abstract State Machine thesis---that arbitrary algorithms are behaviorally equivalent to abstract state machines---to algorithms that can interact with their environments during a step, rather than only between steps. As in the first two articles of the series, we are concerned here with ordinary, small-step, interactive algorithms. This means that the algorithms: (1) proceed in discrete, global steps, (2) perform only a bounded amount of work in each step, (3) use only such information from the environment as can be regarded as answers to queries, and (4) never complete a step until all queries from that step have been answered. After reviewing the previous articles' definitions of such algorithms, of behavioral equivalence, and of abstract state machines (ASMs), we prove the main result: Every ordinary, interactive, small-step algorithm is behaviorally equivalent to an ASM. We also discuss some possible variations of and additions to the ASM semantics.

I plan to survey some of the adaptations and variations of logic that have been introduced for various purposes. For obvious reasons, I shall concentrate mainly on purposes related to computer science and on adaptations that have played a role in my own research. Along the way, I shall touch on some open problems.

This is the first in a series of articles extending the abstract state machine thesis---that arbitrary algorithms are behaviorally equivalent to abstract state machines---to algorithms that can interact with their environments during a step rather than only between steps. In the present work, we describe, by means of suitable postulates, those interactive algorithms that (1) proceed in discrete, global steps; (2) perform only a bounded amount of work in each step; (3) use only such information from the environment as can be regarded as answers to queries; and (4) never complete a step until all queries from that step have been answered.We indicate how a great many sorts of interaction meet these requirements. We also discuss in detail the structure of queries and replies and the appropriate definition of equivalence of algorithms.Finally, motivated by our considerations concerning queries, we discuss a generalization of first-order logic in which the arguments of function and relation symbols are not merely tuples of elements but orbits of such tuples under groups of permutations of the argument places.

Abstract This paper developed from Shelah's proof of a zero-one law for the complexity class “choiceless polynomial time,” defined by Shelah and the authors. We present a detailed proof of Shelah's result for graphs, and describe the extent of its generalizability to other sorts of structures. The extension axioms, which form the basis for earlier zero-one laws (for first-order logic, fixed-point logic, and finite-variable infinitary logic) are inadequate in the case of choiceless polynomial time; they must be replaced by what we call the strong extension axioms. We present an extensive discussion of these axioms and their role both in the zero-one law and in general.

We give an axiomatic description of parallel, synchronous algorithms. Our main result is that every such algorithm can be simulated, step for step, by an abstract state machine with a background that provides for multisets.

Abstract This paper is motivated by the question whether there exists a logic capturing polynomial time computation over unordered structures. We consider several algorithmic problems near the border of the known, logically defined complexity classes contained in polynomial time. We show that fixpoint logic plus counting is stronger than might be expected, in that it can express the existence of a complete matching in a bipartite graph. We revisit the known examples that separate polynomial time from fixpoint plus counting. We show that the examples in a paper of Cai, Fürer, and Immerman, when suitably padded, are in choiceless polynomial time yet not in fixpoint plus counting. Without padding, they remain in polynomial time but appear not to be in choiceless polynomial time plus counting. Similar results hold for the multipede examples of Gurevich and Shelah, except that their final version of multipedes is, in a sense, already suitably padded. Finally, we describe another possible candidate, involving determinants, for the task of separating polynomial time from choiceless polynomial time plus counting.

Hoare logic is a widely recommended verification tool. There is, however, a problem of finding easily checkable loop invariants; it is known that decidable assertions do not suffice to verify while programs, even when the pre- and postconditions are decidable. We show here a stronger result: decidable invariants do not suffice to verify single-loop programs. We also show that this problem arises even in extremely simple contexts. Let N be the structure consisting of the set of natural numbers together with the functions S(x) = x +1, D(x) =2 (x) =*** x /2***. There is a single-loop program *** using only three variables x,y,z such that the asserted program x = y = z =0 *** false is partially correct on N but any loop invariant I(x,y,z) for this asserted program is undecidable.

Abstract The choice construct (choosex: φ(x)) is useful in software specifications. We study extensions of first-order logic with the choice construct. We prove some results about Hilbert'sεoperator, but in the main part of the paper we consider the case when all choices are independent.

Abstract We prove some restrictions on the possible cofinalities of ultrapowers of the natural numbers with respect to ultrafilters on the natural numbers. The restrictions involve three cardinal characteristics of the continuum, the splitting numbers, the unsplitting numberr, and the groupwise density numberg. We also prove some related results for reduced powers with respect to filters other than ultrafilters.

Abstract We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.

In the theory of worst case complexity, NP completeness is used to establish that, for all practical purposes, the given NP problem is not decidable in polynomial time. In the theory of average case complexity, average case completeness is supposed to play the role of NP completeness. However, the average case reduction theory is still at an early stage, and only a few average case complete problems are known. The first algebraic problem complete for the average case under a natural probability distribution is presented. The problem is this: Given a unimodular matrix X of integers, a set S of linear transformations of such unimodular matrices and a natural number n, decide if there is a product of $\leq n$ (not necessarily different) members of S that takes X to the identity matrix.

This paper closes a gap in the foundations of the theory of average-case complexity. First, it clarifies the notion of a feasible solution for a search problem and proves its robustness. Second, it gives a general and usable notion of many–one randomizing reductions of search problems and proves that it has desirable properties. All reductions of search problems to search problems in the literature on average-case complexity can be viewed as such many–one randomizing reductions, including those reductions in the literature that use iterations and therefore do not look many–one. As an illustration, this paper presents a careful proof of a theorem of Impagliazzo and Levin in the framework of the present work.

Abstract We show that the modal propositional logic G, originally introduced to describe the modality “it is provable that”, is also sound for various interpretations using filters on ordinal numbers, for example the end-segment filters, the club filters, or the ineffable filters. We also prove that G is complete for the interpretation using end-segment filters. In the case of club filters, we show that G is complete if Jensen's principle □κ holds for all κ < ℵω; on the other hand, it is consistent relative to a Mahlo cardinal that G be incomplete for the club filter interpretation.

We use models of set theory described in [2] and [3] to prove the consistency of several combinatorial principles, for example: If ℱ is any filter on N containing all the cofinite sets, then there is a finite-to-one function f: N → N such that f(ℱ) is either the filter of cofinite sets or an ultrafilter. As a consequence of our combinatorial principles, we also obtain the consistency of: The partial ordering P of slenderness classes of abelian groups, denned and studied in [4], is a four-element chain. In the remainder of this Introduction, we shall define our terminology and state the combinatorial principles to be considered. In §2, we shall establish some implications between these principles. In §3, we shall prove our consistency results by showing that the strongest of our principles holds in models of set theory constructed in [2] and [3]. A filter on N will always mean a proper filter containing all cofinite sets; in particular, an ultrafilter will necessarily be nonprincipal. We write N ↗ N for the set of nondecreasing functions from the set N of positive integers into itself. A subset ℐ of N ↗ N is called an ideal if it is closed downward (if f(n) ≤ g(n) for all n and if g ∈ ℐ, then f ∈ ℐ) and closed under binary maximum (if f(n) = max(g(n), h(n)) for all n and if g, h ∈ ℐ then f ∈ ℐ).

Fred Richman conjectured that the following principle is not constructive: (*) If A is a decidable subset of the set N of natural numbers and if, for every decidable subset B of N, either A ⊆ B or A ⊆ N − B, then, for some n ∈ N, A ⊆ {n}. A set A of natural numbers is called decidable if ∀n(n ∈ A ∨ ⌉ (n ∈ A)) holds. In recursive models, this agrees with the recursion-theoretic meaning of decidability. In other contexts, “complemented” and “detachable” are often used. Richman's conjecture was motivated by the problem of uniqueness of divisible hulls of abelian groups in constructive algebra. Richman showed that a countable discrete abelian p-group G has a unique (up to isomorphism over G) divisible hull if the subgroup pG is decidable. He also showed that the converse implies. We confirm the nonconstructive nature of by showing (in §1) that it is not provable in intuitionistic set theory, IZF. Thus, in the models we construct, there are countable discrete abelian p-groups G whose divisible hulls are unique but whose subgroups pG are not decidable. Our models do not satisfy further conditions imposed by Richman, namely Church's Thesis and Markov's Principle, so the full conjecture remains an open problem. We do, however, show (in §2) how to embellish our first model so that the fan theorem (i.e., compactness of 2N) fails. (Church's Thesis implies the stronger statement that the negation of the fan theorem holds.) Our models will be constructed by the method of sheaf semantics [1], [3]. That is, we shall construct Grothendieck topoi in whose internal logic fails.

Abstract We exhibit a Horn sentence expressing the statement of the title; the construction generalizes to arbitrary primes in place of five.

For an equivalence relation E on the words in some finite alphabet, we consider the recognition problem (decide whether two words are equivalent), the invariant problem (calculate a function constant on precisely the equivalence classes), the normal form problem (calculate a particular member of an equivalence class, given an arbitrary member) and the first member problem (calculate the first member of an equivalence class, given an arbitrary member). A solution for any of these problems yields solutions for all earlier ones in the list. We show that, for polynomial time recognizable E, the first member problem is always in the class $\Delta _2^{\text{P}} $ (solvable in polynomial time with an oracle for an NP set) and can be complete for this class even when the normal form problem is solvable in polynomial time. To distinguish between the other problems in the list, we construct an E whose invariant problem is not solvable in polynomial time with an oracle for E (although the first member problem is in ${\text{NP}}^E \cap {\text{co - NP}}^E $), and we construct an E whose normal form problem is not solvable in polynomial time with an oracle for a certain solution of its invariant problem.

Abstract A 2-affable ultrafilter has only finitely many predecessors in the Rudin-Keisler ordering of isomorphism classes of ultrafilters over the natural numbers. If the continuum hypothesis is true, then there is an ℵ1-sequence of ultrafilters Dα such that the strict Rudin-Keisler predecessors of Dα are precisely the isomorphs of the Dβ's for β < α.

Abstract Adjoin, to a countable standard model M of Zermelo-Fraenkel set theory (ZF), a countable set A of independent Cohen generic reals. If one attempts to construct the model generated over M by these reals (not necessarily containing A as an element) as the intersection of all standard models that include M ∪ A, the resulting model fails to satisfy the power set axiom, although it does satisfy all the other ZF axioms. Thus, there is no smallest ZF model including M ∪ A, but there are minimal such models. These are classified by their sets of reals, and there is one minimal model whose set of reals is the smallest possible. We give several characterizations of this model, we determine which weak axioms of choice it satisfies, and we show that some better known models are forcing extensions of it.

Abstract Any two models of arithmetic can be jointly embedded in a third with any prescribed isomorphic submodels as intersection and any prescribed relative ordering of the skies above the intersection. Corollaries include some known and some new theorems about ultrafilters on the natural numbers, for example that every ultrafilter with the “4 to 3” weak Ramsey partition property is a P-point. We also give examples showing that ultrafilters with the “5 to 4” partition property need not be P-points and that the main theorem cannot be improved to allow a prescribed ordering of lower skies.

Ramsey's theorem [5] asserts that every infinite set X has the following partition property (RP): For every partition of the set [X]2 of two-element subsets of X into two pieces, there is an infinite subset Y of X such that [Y]2 is included in one of the pieces. Ramsey explicitly indicated that his proof of this theorem used the axiom of choice. Kleinberg [3] showed that every proof of Ramsey's theorem must use the axiom of choice, although rather weak forms of this axiom suffice. J. Dawson has raised the question of the position of Ramsey's theorem in the hierarchy of weak axioms of choice. In this paper, we prove or refute the provability of each of the possible implications between Ramsey's theorem and the weak axioms of choice mentioned in Appendix A.3 of Jech's book [2]. Our results, along with some known facts which we include for completeness, may be summarized as follows (the notation being as in [2]): A. The following principles do not (even jointly) imply Ramsey's theorem, nor does Ramsey's theorem imply any of them: the Boolean prime ideal theorem, the selection principle, the order extension principle, the ordering principle, choice from wellordered sets (ACW), choice from finite sets, choice from pairs (C2). B. Each of the following principles implies Ramsey's theorem, but none of them follows from Ramsey's theorem: the axiom of choice, wellordered choice (∀kACk), dependent choice of any infinite length k (DCk), countable choice (ACN0), nonexistence of infinite Dedekind-finite sets (WN0).

Abstract There is an analogy between concepts such as end-extension types and minimal types in the model theory of Peano arithmetic and concepts such as P-points and selective ultrafilters in the theory of ultrafilters on N. Using the notion of conservative extensions of models, we prove some theorems clarifying the relation between these pairs of analogous concepts. We also use the analogy to obtain some model-theoretic results with techniques originally used in ultrafilter theory. These results assert that every countable nonstandard model of arithmetic has a bounded minimal extension and that some types in arithmetic are not 2-isolated.

A classical result of descriptive set theory expresses every co-analytic subset of the real line as the union of an increasing sequence of Borel sets, the length of the chain being at most the first uncountable ordinal ℵ1 (see [5], [8]). An effective analog of this theorem, obtained by replacing co-analytic (Π11) and Borel (Δ11) with their lightface analogs, would represent every Π11 subset of the real line as the union of a chain of Δ11 sets. No such analog is true, however, because some Δ11 sets are not the union of their Δ11 subsets. For example, the set W, consisting of those reals which code well-orderings (in some standard coding) is Π11, but, by the boundedness principle ([3], [9]), any Δ11 subset of W contains codes only for well-orderings shorter than ω1, the first nonrecursive ordinal. Accordingly, we define the core of a Π11 set to be the union of its Δ11 subsets; clearly this is the largest subset of the given Π11 set for which an effective version of the classical representation could exist. In §1, we develop the elementary properties of cores of Π11 sets. For example, such a core is itself Π11 and can be represented as the union of a chain of Δ11 sets in a natural way; the chain will have length at most ω1. We show that the core of a Π11 set is “almost all” of the set, while on the other hand there are uncountable Π11 sets with empty cores.

If two nonstandard models of complete arithmetic are elementarily embedded in a third, then their intersection may be considerably smaller than either of them; indeed, the intersection may be only the standard model. For example, if D and E are nonprincipal ultrafilters on ω, then the nonstandard models D-prod and E-prod (where is the standard model) have canonical elementary embeddings into D-prod (E-prod , and the intersection of their images is easily seen to be the (canonical image of the) standard model. In this paper, we shall prove that, under certain conditions, this phenomenon will not occur. Our main result (Theorem 3) is that the intersection of countably many pairwise cofinal models is itself cofinal with these models, provided that at least one of them is generated by a single element. (Precise definitions will be given below.) The theorems in this paper were first formulated in terms of ultrafilters, then rephrased (using the methods of Chapter III of [1]) as statements about ultra-powers of , and finally generalized to their present form. Since the theorems and their proofs are now entirely model-theoretic, they are presented here separately from the study of ultrafilters in which they originated. That study, including applications of the present results, will appear in [2]. Let L be the first-order language whose n-place relation symbols are all the relations R ⊆; ωn and whose n-place function symbols are all the functions f: ωn → ω. Let be the standard model for L; its universe is ω and every nonlogical symbol of L denotes itself. Let be an elementary extension of . The relation (or function) denoted by R (or f) in will be called *R (or *f).

Consider the Löwenheim-Skolem theorem in the form: If a theory in a countable first-order language has a model, then it has a countable model. As is well known, this theorem becomes false if one omits the hypothesis that the language be countable, for one then has the following trivial counterexample. Example 1. Let the language have uncountably many constants, and let the theory say that they are unequal. To motivate some of our future definitions and to introduce some notation, we present another, less trivial, counterexample. Example 2. Let L0 be the language whose n-place predicate (resp. function) symbols are all the n-place predicates (resp. functions) on the set ω of natural numbers. Let be the standard model for L0; we use the usual notation Th( ) for its complete theory. Add to L0 a new constant e, and add to Th( ) an axiom schema saying that e is infinite. By the compactness theorem, the resulting theory T has models. However, none of its models are countable. Although this fact is well known, we sketch a proof in order to refer to it later. By [5, p. 81], there is a family {Aα ∣ < α < c} of infinite subsets of ω, the intersection of any two of which is finite.

The method of inner models, used by Gödel to prove the (relative) consistency of the axiom of choice and the generalized continuum hypothesis [2], cannot be used to prove the (relative) consistency of any statement which contradicts the axiom of constructibility (V = L). A more precise statement of this well-known fact is: (*)For any formula θ(x) of the language of ZF, there is an axiom α of the theory ZF + V ≠ L such that the relativization α(θ) is not a theorem of ZF. On p. 108 of [1], Cohen gives a proof of (*) in ZF assuming the existence of a standard model of ZF, and he indicates that this assumption can be avoided. However, (*) is not a theorem of ZF (unless ZF is inconsistent), because (*) trivially implies the consistency of ZF. What assumptions are needed to prove (*)? We know that the existence of a standard model implies (*) which, in turn, implies the consistency of ZF. Is either implication reversible? From our main result, it will follow that, if the converse of the first implication is provable in ZF, then ZF has no standard model, and if the converse of the second implication is provable in ZF, then so is the inconsistency of ZF. Thus, it is quite improbable that either converse is provable in ZF.