User:Miui/Stratification

NOTE: This article has been generated by AI. Use with extreme caution.

This article is about a restriction from set theory, not about an esoteric programming language. For the self-printing program, see Quine.

Stratification is the syntactic restriction that W. V. O. Quine used in New Foundations (NF, 1937) to keep unrestricted comprehension without producing Russell's paradox. It is of some interest here because it is a type system that is checked and then thrown away, and because the check itself is a tiny decidable string problem — one that can be made completely visible by writing the variables in unary.

The problem

Naive comprehension says: for any predicate P, the set {x : P(x)} exists. Take

P(C) := C ∉ C

and the resulting set is a member of itself iff it is not, which is fatal.

ZF fixes this by restricting the scope of comprehension: you may only carve a subset out of a set you already have (the axiom schema of specification). NF fixes it the other way round. Comprehension stays unrestricted in scope — the predicate ranges over everything — but the language of predicates is cut down. C ∉ C is not a legal predicate, because the same symbol C occurs on both sides of ∈, and the two sides of ∈ live at different relative types.

The rule

A formula φ in the language of ∈ and = is stratified if there is an assignment σ of a natural number (a "type") to each variable such that:

• for every atomic subformula x ∈ y: σ(y) = σ(x) + 1
• for every atomic subformula x = y: σ(x) = σ(y)

NF's comprehension schema is then: for every stratified φ, the set {x : φ(x)} exists.

Note what σ is not. The types are never written down and never appear in the theory; they only have to exist. This is Russell's simple theory of types with the type indices rubbed out — what Quine called typical ambiguity. In compiler terms, the annotations are inferred, checked, and then erased, and nothing at runtime remembers them.

The chevron notation

The rule is easier to see if the type of a variable is forced into its own name. Let every variable be a nonempty string of >, and write >ⁿ for the string of n chevrons. Pin σ(>ⁿ) = n. Because > already reads as "greater than", the notation says out loud what the type discipline requires: the right-hand side of ∈ must be exactly one greater than the left.

Stratification checking now collapses to string length. The entire algorithm is:

x ∈ y  is well-formed  iff  len(y) == len(x) + 1
x = y  is well-formed  iff  len(y) == len(x)

Formula	Types demanded	Verdict
> ∈ >>	1, 2	well-formed
>> ∈ >>>	2, 3	well-formed
> ∈ >>>	1, 3	ill-formed — skips a level
>> ∈ >	2, 1	ill-formed — points the wrong way
> = >	1, 1	well-formed
> = >>	1, 2	ill-formed — equality demands equal type
> ∈ >	1, 1 and 1, 2	ill-formed — Russell

Two things fall straight out of the table.

First, >> is the only predicate that can speak about >. Anything that has > as a member must be one chevron longer, and there is exactly one such token. Membership has no reach: it cannot skip a level (>>> is already talking about >>, not about >) and it cannot look down. Each level is described from precisely one place, the level immediately above it.

Second, > and >> are never the same set. Identifying them would be the formula > = >>, which demands σ = 1 and σ = 2 for the same position; the set that describes > is therefore always a different object from > itself. This is the whole trick. The paradox needs a thing to coincide with the thing that describes it, and in chevrons that would require a token one character longer than itself. The only fixed point of "append a chevron" is the infinite string >>>>…, which is not a token, so the Russell set has nowhere to be written.

The chevron notation is a mnemonic and slightly stricter than NF proper: real NF lets a variable be assigned any type, and only rejects a formula when the combination of its atomic subformulas forces a contradiction. Chevrons pin the assignment in advance. The rejections are the same ones, arrived at earlier.

The set of all sets

Now take the predicate

P(C) := C = C

This is stratified — put every variable at type 0 and there is nothing left to check. So comprehension hands over V = {x : x = x}, the set of all sets, and since V is a set, V ∈ V. NF has a universal set and a genuine self-membership, and no contradiction follows.

It is worth being precise about why that is not cheating. The stratification restriction applies to the formulas you use to build sets, not to the sentences that turn out true afterwards. V ∈ V is a theorem about a constant, not an instance of comprehension. In chevrons: each level has its own universe, V₁ ∈ V₂ ∈ V₃ ∈ …, every membership stepping up exactly one chevron; typical ambiguity then observes that no sentence can tell these levels apart, the subscripts are dropped, and what is left is V ∈ V.

The theory that results is genuinely strange. NF proves the axiom of infinity and refutes the axiom of choice (Specker, 1953); the singleton map x ↦ {x} raises type by one and so is not itself a set, which is where most of the strangeness comes from. Jensen's variant NFU, which allows urelements, is much better behaved and is compatible with both choice and infinity. The consistency of NF itself was open for decades until a proof by Randall Holmes, later formalised in Lean by Sky Wilshaw.

A cryptographic analogue

Restricting the language of predicates rather than the scope of comprehension is not peculiar to set theory. It turns up wherever admitting arbitrary predicates would be ruinous for some reason other than paradox. A clean case is Blake and Kolesnikov's work on securely computing the greater-than predicate, where the object of study is once again called GT and once again turns out to be the only primitive anybody needs.

The setting is two-party: a receiver R holds a private value x, a sender S holds a private set, and R is to learn whether x lies in that set without learning the set, while S learns nothing about x. Comprehension here is unrestricted in scope — x ranges over the whole domain DI = {0, …, 2n − 1}, there is no ambient set to carve a subset out of — but S may only use predicates the protocol can actually evaluate, and the generator of that language is GT.

The even integers on an interval

Take the set of all even integers lying in a large interval (y, z). The obvious definition — "x is even and y < x < z" — leans on a divisibility predicate that has no place in the admissible language. What is written instead is

S = {x | x₀ < 1 ∧ x ∈ (y, z)}

where x₀ is the low bit of x. Evenness is not tested; it is re-expressed as an instance of GT on a one-bit domain. The set is thereby a conjunction of two interval memberships, one of them very small, and the paper's reductions carry it the rest of the way down: membership in an interval reduces to two invocations of GT, membership in a union of intervals reduces to interval membership, and conjunction (with disjunction by De Morgan) reduces to those. Nothing but > survives at the bottom.

Points of contact

• One relation generates the language. In NF every legal formula is built from ∈ and = under a type discipline; in the protocol every legal set is built from > under a reducibility discipline. Neither theory says "no predicates". Both say "these predicates".
• Equality is the awkward one. The paper writes x₀ < 1 rather than x₀ = 0, and it assumes the compared values are never equal outright, enforcing this by a mapping that pushes the two inputs onto different parities so the equality case cannot arise. Compare the chevron table above, where = is the constraint that pins two positions together and ∈ is the one that holds them exactly one step apart: > is the relation that moves, which is why in both settings it is the one you build from.
• Different payoff, same shape. The restriction buys consistency in NF and one-round efficiency against a computationally unbounded receiver in the protocol. Structurally, both keep "for every x" and give up "for every P".

The parallel is structural and should not be pushed further: nothing in the cryptographic work concerns types, paradox, or self-membership, and the coincidence of the name GT is just a coincidence.

Relevance

• The check is cheap. Stratifying a formula means solving a system of constraints of the forms σ(x) = σ(y) and σ(y) = σ(x) + 1. That is a difference-constraint system over a graph, solvable by union-find with offsets in near-linear time, and a contradiction is detected as a cycle whose offsets do not sum to zero. In the chevron notation it degenerates to subtracting two string lengths.
• Quine atoms. A Quine atom is a set with x = {x}. Stratification demands σ(x) = σ(x) + 1, so comprehension never produces one — the self-reproducing object is exactly what the type discipline is built to exclude. The pun is not accidental: quines are named after the same Quine, for the same reason (his "'yields falsehood when appended to its own quotation' yields falsehood when appended to its own quotation"), and stratification is what a program would have to violate to be one.
• As a language idea. An esolang in which identifier length is type, the only static check is stratification, and the checker is len(rhs) - len(lhs) == 1, seems both writable and unpleasant to write in — which is usually a good sign. It has not been done here yet.

See also

• Quine
• New Foundations
• Stratification (mathematics)
• Axiom schema of specification
• Russell's paradox
• Strong Conditional Oblivious Transfer and Computing on Intervals by Ian F. Blake & Vladimir Kolesnikov

References

• Quine, W. V. (1937). "New Foundations for Mathematical Logic". The American Mathematical Monthly 44 (2): 70–80.
• Specker, E. P. (1953). "The Axiom of Choice in Quine's New Foundations for Mathematical Logic". Proceedings of the National Academy of Sciences 39: 972–975.
• Jensen, R. B. (1969). "On the Consistency of a Slight (?) Modification of Quine's New Foundations". Synthese 19: 250–263.
• Holmes, M. R. (1998). Elementary Set Theory with a Universal Set. Cahiers du Centre de Logique 10.
• Blake, I. F. and Kolesnikov, V. (2004). "Strong Conditional Oblivious Transfer and Computing on Intervals". In P. J. Lee (ed.), Advances in Cryptology — ASIACRYPT 2004, LNCS 3329, pp. 515–529. Springer-Verlag.