2. Quine’s Mathematical Logic and Stratification

Quine - New Foundations for Mathematical Logic (1937)

Willard Van Orman Quine proposed New Foundations for Mathematical Logic as a direct alternative to the rigid Theory of Types established by Whitehead and Russell in Principia Mathematica.

Quine’s objective was to translate pure mathematics into formal logic utilizing a completely minimized primitive vocabulary, abandoning hierarchical type theory to allow for the existence of a single, universal class (\(V\)).

Suggested Reading:
  • Quine, W. V. (1937). New Foundations for Mathematical Logic. The American Mathematical Monthly, 44(2), pp. 70-80.

The Primitives

Imagine building an entire programming language from just three CPU instructions. Quine’s language operates strictly on three primitive mathematical constructs:

  1. Membership: \(x \in y\) (Object \(x\) belongs to set \(y\))
  2. Alternative Denial: \((\phi \mid \psi)\) (The logical NAND gate)
  3. Universal Quantification: \((x)\phi\) (For all \(x\), \(\phi\) is true)

Everything else in mathematics—from addition to complex geometry—must be built from these three atoms. To prevent human mathematicians from writing endless strings of NAND gates, Quine created 15 Derivative Definitions to act as typographical macros.

Contextual Eliminability & The 15 Derivative Definitions

In Quine’s philosophy of logic, mathematical objects do not possess independent metaphysical substance. Mathematical expressions operate as syntactic macros that dissolve upon evaluation into raw primitive statements. Quine terms this design principle Contextual Eliminability: every high-level mathematical notation must be uniquely eliminable in favor of primitive membership and logical connectives.

The 15 Derivative Definitions (D1–D15) form a four-stage compilation pipeline, translating mathematical reasoning systematically down into primitive NAND gates and membership assertions.

Phase 1: Boolean Connectives (D1 - D5)

Quine proves that every standard propositional connective compiles down to Sheffer’s alternative denial gate (\(|\)):

  • D1: Denial (Not)
    \(\sim\phi =_{\text{def}} (\phi \mid \phi)\)
    Passing the identical proposition into both inputs of a NAND gate outputs its logical negation.

  • D2: Conjunction (And)
    \((\phi\cdot\psi) =_{\text{def}} \sim(\phi \mid \psi)\)
    Wrapping a NAND operation in a negation produces logical AND.

  • D3: Implication (If-then)
    \((\phi\supset\psi) =_{\text{def}} (\phi \mid \sim\psi)\)

  • D4: Alternation (Or)
    \((\phi\lor\psi) =_{\text{def}} (\sim\phi\supset\psi)\)

  • D5: Equivalence (Iff)
    \((\phi\equiv\psi) =_{\text{def}} ((\phi \mid \psi) \mid (\phi\lor\psi))\)

Phase 2: First-Order Logic & Identity (D6 - D8)

With Boolean logic operational, Quine constructs existential quantification, set inclusion, and equality without introducing a primitive equality operator:

  • D6: Particular Quantification (Exists)
    \((\exists\alpha)\phi =_{\text{def}} \sim(\alpha)\sim\phi\)
    “There exists an \(\alpha\)” translates to “It is not the case that for all \(\alpha\), \(\phi\) is false.”

  • D7: Inclusion (Subclass)
    \((\alpha \subseteq \beta) =_{\text{def}} (\gamma)((\gamma \in \alpha)\supset(\gamma \in \beta))\)

  • D8: Identity (Equals)
    \((\alpha=\beta) =_{\text{def}} (\gamma)((\alpha \in \gamma)\supset(\beta \in \gamma))\)
    Leibnizian Extensional Identity: Two entities are mathematically identical if every class containing \(\alpha\) also contains \(\beta\). Identity is established through external containment relations rather than internal inspection.

Phase 3: Definite Descriptions (D9 - D10)

Definite descriptions provide the mechanism for referencing specific entities defined by unique predicates:

  • D9: Description in Membership Context
    \(((\iota\alpha)\phi \in \beta) =_{\text{def}} (\exists\gamma)((\gamma \in \beta)\cdot(\alpha)((\alpha=\gamma)\equiv\phi))\)
    “The unique \(\alpha\) satisfying \(\phi\) belongs to class \(\beta\).”

  • D10: Description Denoting a Class
    \((\beta \in (\iota\alpha)\phi) =_{\text{def}} (\exists\gamma)((\beta \in \gamma)\cdot(\alpha)((\alpha=\gamma)\equiv\phi))\)

Phase 4: Class and Relational Abstractions (D11 - D15)

Class abstractions represent the pinnacle of contextual eliminability. Expressions such as “the set of even numbers” are not static physical entities; they are dynamic queries executed against definite descriptions:

  • D11: Class Abstraction
    \(\hat{\alpha}\phi =_{\text{def}} (\iota\beta)(\alpha)((\alpha \in \beta)\equiv\phi)\)

  • D12: Unit Class (Singleton)
    \(\{\alpha\} =_{\text{def}} \hat{\beta}(\beta=\alpha)\)

  • D13: Pair Class
    \(\{\alpha,\beta\} =_{\text{def}} \hat{\gamma}((\gamma=\alpha)\lor(\gamma=\beta))\)

  • D14: Ordered Couple (Kuratowski Pair)
    \((\alpha,\beta) =_{\text{def}} \{\{\alpha\},\{\alpha,\beta\}\}\)

  • D15: Relational Abstraction
    \(\hat{\alpha}\hat{\beta}\phi =_{\text{def}} \hat{\gamma}(\exists\alpha)(\exists\beta)((\gamma=(\alpha,\beta))\cdot\phi)\)

The Kuratowski Type-Inflation Problem

Quine adopted Casimir Kuratowski’s standard definition of the ordered pair: \((\alpha,\beta) = \{\{\alpha\},\{\alpha,\beta\}\}\). In classical set theory, this definition provides an elegant foundation for coordinate geometry and relations. In a stratified universe, however, Kuratowski pairing introduces an asymmetric type-inflation penalty.

Variable Base Level:       alpha : type n,   beta : type n
First Singleton Level:     {alpha} : type n + 1,   {alpha, beta} : type n + 1
Outer Enclosing Set:       {{alpha}, {alpha, beta}} : type n + 2
Resulting Pair Type:       (alpha, beta) : type n + 2

Because the ordered pair \((\alpha,\beta)\) resides two integer levels higher than its constituent elements, any binary relation \(R \subseteq A \times B\) requires its domain and codomain variables to be type-shifted by \(+2\). When chaining relational mappings, this \(+2\) displacement accumulates, creating severe stratification violations during function composition.

Resolving this architectural friction required Theodore Hailperin to engineer a flat, homogeneous pairing operator, which forms the focus of Chapter 3.

Postulates and The Principle of Stratification

To generate theorems, Quine relies on one core postulate (P1: Extensionality) and five rules of inference (R1-R5). The most critical rule is R3 (Principle of Abstraction), which states that for any formula \(\phi\), there exists a class containing exactly the objects satisfying \(\phi\).

However, an unrestricted R3 immediately triggers Russell’s Paradox. If \(\phi\) is “not a member of itself” (\(x \notin x\)), R3 generates a self-contradictory class.

To solve this without reverting to ZFC’s total ban on the Universal Set, Quine modified the rule to R3’: A formula can only generate a class if it is stratified.

ImportantWhat is Stratification?

Stratification means you can assign integers to variables such that for every membership relation \(x \in y\), the type of \(y\) is exactly one integer higher than \(x\) (\(n\) and \(n+1\)).

Formulas like \(x \in x\) are unstratified (because \(x\) cannot be both \(n\) and \(n+1\) simultaneously). In NF, unstratified formulas are grammatically legal to write, but R3’ forbids them from generating sets. This nullifies the paradox while perfectly preserving the Universal Set \(V\) (because the formula \(x=x\), defining the universal set, is trivially stratified as \(n=n\)).

A Concrete Example of Stratification

Test the formula: “There exists a set \(y\) such that \(x \in y\) and \(y \in z\).”

In formal logic:

\[\exists y (x \in y \land y \in z)\]

To prove this formula is stratified, assign an integer to each variable such that the right-hand term of any membership relation \(a \in b\) is \(+1\) greater than the left-hand term:

  1. Assign \(x = 1\).
  2. From \(x \in y\), \(y\) must equal \(x + 1 = 2\).
  3. From \(y \in z\), \(z\) must equal \(y + 1 = 3\).

All variables map to consistent integers (\(x=1, y=2, z=3\)) without contradiction. The formula is stratified.

Guided Example: Stratification Types

Examine the formula: \(x \in y \land y \in z\)

If we declare that \(\text{type}(x) = 1\), then by the rule of stratification: \(\text{type}(y) = 1 + 1 = 2\)

What must \(\text{type}(z)\) be for this entire formula to remain strictly stratified?

\(\text{type}(z) = \_\_\_\_\_\)

Problem Set: Stratification in First-Order Logic

Before mapping ontologies in code, you must manually resolve stratification boundaries in pure logic.

Problem 2.1: Resolving Russell’s Paradox

In standard notation, Russell’s paradoxical class is generated by the formula \(\phi = (x \notin x)\). Write out the explicit typing (e.g., \(n\), \(n+1\)) that proves this formula is unstratified. Explain exactly why Quine’s Rule R3’ rejects its construction as a set.

Problem 2.2: The Universal Set Proof

The Universal Set (\(V\)) is defined by the formula \(x = x\). Using Quine’s definition of identity (D8), prove that this formula is strictly stratified and therefore legally generates the set of all sets under R3’.

Next: Hailperin’s Finite Axiomatization ➔