The Number One, Part Three

In an earlier post, "What it Means to be Number One", I presented Quine's definition of the number one, which is defined in terms of four basic mathematical constructs: class membership (⌜α ϵ β⌝), universal generalization (⌜(α)ϕ⌝), joint denial (⌜(ϕ ↓ ψ)⌝), and class abstraction (⌜α^ϕ⌝).  It is six pages of dense text.  In another post, "The Number One, Part Two", I claimed that the length of the definition is "the result of giving the number one a precise, complete, logical definition without resorting to using any numbers except zero".  This is not quite true.  I've since realized that the size comes not from precision, completeness nor logicality, but from Quine's definition of negation, which is

⌜∼ϕ⌝ for ⌜(ϕ ↓ ϕ)⌝

This is definition is important because it enables his system to define all truth-functional connectives in terms of just one truth-functional connectives, thereby minimizing the number of basic constructs in his system.  But it does have the effect of making expanded definitions quite large.  You see, any time a negation is expanded, the expression which is negated (ϕ) is duplicated in the resulting expansion.  If that expression also contains negated expressions, then those expressions are quadrupled, and if those negated expressions contain negated expressions, they are octupled, and so on.  The result is an exponential relationship between the size of an expanded definition and the number of layers of negation in the definition.  Those of you who know computer science know that exponential relationships mean huge outputs for all but the smallest inputs.  Hence the 6-page definition of one.  If we expand all constructs contained in Quine's definition of one except negation, the result is not so big.  It is

x^∼(y)∼(∼(y ϵ x) ↓ ∼(α^(∼(α ϵ x) ↓ ∼(α ϵ α′^(∼(α′ ϵ α′′^((α′′′)(∼∼(∼(α′′′ ϵ α′′) ↓ _▪α′′′ ϵ y) ↓ ∼∼(∼(α′′′ ϵ y) ↓ _▪α′′′ ϵ α′′))))))) ϵ α^((α′)(∼∼(∼(α′ ϵ α) ↓ _▪α′ ϵ x′^(∼((α′′)(∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′) ↓ ∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′))))) ↓ ∼∼(∼(α′ ϵ x′^(∼((α′′)(∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′) ↓ ∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′))))) ↓ _▪α′ ϵ α)))))

which is not shockingly complicated.  Even if we expand statements of membership in and of class abstractions in this definition (which is something I did not do in "What it means to be..."), the definition of one is still just

x^∼(y)∼(∼(y ϵ x) ↓ ∼(∼(γ)∼(∼(∼(β)∼(∼((α)(∼∼(∼(α ϵ β) ↓ _▪∼(γ′)∼(∼(α ϵ γ′) ↓ ∼(α′)∼(∼(α′ ϵ γ′) ↓ (∼(α′ ϵ x) ↓ ∼(∼(γ′′)∼(∼(α′ ϵ γ′′) ↓ ∼(α′′)∼(∼(α′′ ϵ γ′′) ↓ _▪∼(∼(γ′′′)∼(∼(α′′ ϵ γ′′′) ↓ ∼(α′′′)∼(∼(α′′′ ϵ γ′′′) ↓ _▪(α′′′′)(∼∼(∼(α′′′′ ϵ α′′′) ↓ _▪α′′′′ ϵ y) ↓ ∼∼(∼(α′′′′ ϵ y) ↓ _▪α′′′′ ϵ α′′′)))))))))))) ↓ ∼∼(∼(∼(γ′)∼(∼(α ϵ γ′) ↓ ∼(α′)∼(∼(α′ ϵ γ′) ↓ (∼(α′ ϵ x) ↓ ∼(∼(γ′′)∼(∼(α′ ϵ γ′′) ↓ ∼(α′′)∼(∼(α′′ ϵ γ′′) ↓ _▪∼(∼(γ′′′)∼(∼(α′′ ϵ γ′′′) ↓ ∼(α′′′)∼(∼(α′′′ ϵ γ′′′) ↓ _▪(α′′′′)(∼∼(∼(α′′′′ ϵ α′′′) ↓ _▪α′′′′ ϵ y) ↓ ∼∼(∼(α′′′′ ϵ y) ↓ _▪α′′′′ ϵ α′′′)))))))))))) ↓ _▪α ϵ β))) ↓ ∼(β ϵ γ))) ↓ ∼(α)∼(∼(α ϵ γ) ↓ _▪(α′)(∼∼(∼(α′ ϵ α) ↓ _▪∼(γ′)∼(∼(α′ ϵ γ′) ↓ ∼(x′)∼(∼(x′ ϵ γ′) ↓ _▪∼((α′′)(∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′) ↓ ∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′)))))) ↓ ∼∼(∼(∼(γ′)∼(∼(α′ ϵ γ′) ↓ ∼(x′)∼(∼(x′ ϵ γ′) ↓ _▪∼((α′′)(∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′) ↓ ∼∼(∼(α′′ ϵ x′) ↓ _▪α′′ ϵ x′)))))) ↓ _▪α′ ϵ α))))))

which is more than anyone would want to try to write or memory, but still not embarrassingly long.  If we don't expand any of the truth-functional connectives, nor existential quantification, the result is something that it almost readable by a person who is familiar with symbolic logic:

x^(∃y)(y ϵ x _▪ (∃γ)((∃β)((α)(α ϵ β_▪ ≡ _▪(∃γ′)(α ϵ γ′ _▪ (α′)(α′ ϵ γ′_▪ ⊃ (α′ ϵ x _▪ (∃γ′′)(α′ ϵ γ′′ _▪ (α′′)(α′′ ϵ γ′′_▪ ⊃ _▪∼((∃γ′′′)(α′′ ϵ γ′′′ _▪ (α′′′)(α′′′ ϵ γ′′′_▪ ⊃ _▪(α′′′′)(α′′′′ ϵ α′′′_▪ ≡ _▪α′′′′ ϵ y)))))))))) _▪ β ϵ γ) _▪ (α)(α ϵ γ_▪ ⊃ _▪(α′)(α′ ϵ α_▪ ≡ _▪(∃γ′)(α′ ϵ γ′ _▪ (x′)(x′ ϵ γ′_▪ ⊃ _▪∼((α′′)(α′′ ϵ x′_▪ ≡ _▪α′′ ϵ x′))))))))