Margaris has shown1 that for every triple 〈s,t,m〉 of integers such that 1 ≦ s < t < m it is possible to construct a formalisation of an m-valued propositional calculus satisfying the following conditions: I. Every statement which takes only truth-values belonging to the set {1, …,s} is provable. II. Every provable statement takes only truth-values belonging to the set {1, …, t}. III. There exist statements Pk, Qk which take only truth-values belonging to the set {1, …, k) and neither of which takes only truth-values belonging to the set {1, …, k—1} such that Pk is provable and Qk is unprovable (k = s+1, …, t). The systems of Margaris are all functionally incomplete and he appears to suggest2 that it is impossible to construct functionally complete systems having the required properties.

There are several ways for a formula to be “the contrary” of a thesis. When there is a negation we could call a formula an “antithesis” if it is the negation of a thesis—or its negation is a thesis—both properties being equivalent when the negation is classical.

When there is no negation or when the connective called “negation” is very different from classical negation, we are forced to look for a different notion.

Whence:

Definition 1. In a propositional calculus, a substitution antithesis—or, for short, an s-antithesis—is a formula no instance of which is a thesis.

There is another kindred notion, but only for calculi for which a deducibility has been defined:

Definition 2. A deduction antithesis—for short, a d-antithesis—is a formula from which every formula is deducible.

Both notions have been used in the study of the deducibility of certain systems (see below, §4).

In the classical propositional calculus, the s-antitheses are simply the formulas which are negations of theses (and whose negations are theses).

In S5 and in all the weaker modal propositional calculi, there are s-antitheses which are not negations of theses (and whose negations are not theses); typical examples are ¬(Mp ⊃ Lp) and ¬(p ⊃ Lp) where p is a propositional variable, and ⊃, ¬, M and L are respectively material implication, negation, possibility and necessity (see [8]).

A version of Herbrand's theorem tells us that a universal sentence of a first-order language with at least one constant is satisfiable if and only if the conjunction of all its ground instances is. In general the set of such instances is infinite, and arbitrarily large finite subsets may have to be inspected in order to detect inconsistency. Essentially, the reason that every member of such an infinite set may potentially matter, can be traced back to sentences like

(1)

Loosely put, such sentences effectively sabotage any attempt to build a model from below in a finite number of steps, since new members of the Herbrand universe are constantly brought to attention. Since they cause an indefinite expansion of the relevant part of the Herbrand universe, such sentences could quite appropriately be called expanding.

When such sentences are banned, stronger versions of Herbrand's theorem can be stated. Define a clause (disjunction of literals) to be non-expanding if every non-ground term occurring in a positive literal also occurs (possibly as an embedded subterm) in a negative literal of the same clause. Written as a disjunction of literals, the matrix of (1) clearly fails this criterion. Moreover, say that a sentence is non-expanding if it is a universal sentence with a quantifier-free matrix that is a conjunction of non-expanding clauses. Such sentences do in a sense never reach out beyond themselves, and the relevant part of the Herbrand universe is therefore drastically reduced.

In this paper, we show by a proof-theoretical argument that in a logic without structural rules, that is in noncommutative linear logic with exponentials, every formula A for which exchange rules (and weakening and contraction as well) are admissible is provably equivalent to? A. This property shows that the expressive power of “noncommutative exponentials” is much more important than that of “commutative exponentials”.

We give limits defined in terms of abstract pointclasses of the amount of determinacy available in certain canonical inner models involving strong cardinals. We show for example:

Theorem A. Det(-IND) ⇒ there exists an inner model with a strong cardinal.

Theorem B. Det(AQI) ⇒ there exist type-l mice and hence inner models with proper classes of strong cardinals.

where -IND(AQI) is the pointclass of boldface -inductive (respectively arithmetically quasi-inductive) sets of reals.

We show how to force, with finite conditions, the forcing axiom PFA(T), a relativization of PFA to proper forcing notions preserving a given Suslin tree T. The proof uses a Neeman style iteration with generalized side conditions consisting of models of two types, and a preservation theorem for such iterations. The consistency of this axiom was previously known using a standard countable support iteration and a preservation theorem due to Miyamoto.

Improving on a result of Arana, we construct an effective family (φr ∣ r ϵ ℚ ∩ [0,1]) of Σn-conservative Πn sentences, increasing in strength as r decreases, with the property that ¬φp is Πn-conservative over PA + φq whenever p < q. We also construct a family of Σn sentences with properties as above except that the roles of Σn and Πn are reversed. The latter result allows to re-obtain an unpublished result of Solovay, the presence of a subset order-isomorphic to the reals in every non-trivial end-segment of every branch of the E-tree, and to generalize it to analogues of the E-tree at higher levels of the arithmetical hierarchy.