After a long discussion at Reddit where many counter and counter-counter arguments appeared, I was pointed an error:
S(
... S ...) is not defined. I meant to expand S inside such a statement before applying the outward S(), but I’ve realized that S is not defined solely by functional symbols but by a predicate, so “expand S” does not make sense.I need to confess that the article is worth withdrawal due to a fundamental error.
An error in most logic studybooks
Victor Porton, no affiliation, porton.victor@gmail.com
Abstract: In most logic study books “extension by definition” is erroneous.
This error is almost as serious as if we found a contradiction in ZF. There are no contradictions in ZF, but ZF is always used together with such definitions. So, for practical purposes it is as if the error were in ZF itself.
That’s a security hazard: Nuclear powerplants for instance are made using logic.
In this article I show how to produce a contradiction using ZF and extension by definition. I also show how to generalize this error to Peano arithmetic (or even predicate calculus).
I show which logical systems are free of this paradox.
Keywords: logical paradoxes, logic paradoxes, logical paradox, logic paradox
Gödel encoding
Every logical formula can be written as a string of characters. For example the formula that there exists a natural number whose square is below five:
∃x∈ℕ:(x^2 < 5)
can be represented as characters,
∃, x, ∈, ℕ, :, (, x,^, 2, >, 5, )
As Pythagorus said “everything is a number”. Every logical formula can be encoded as a number: For each logical formula we produce a number, and having this number, can reconstruct this formula back.
Gödel did it this way (see [1]):
Gödel used a system based on prime factorization. He first assigned a unique natural number to each basic symbol in the formal language of arithmetic with which he was dealing.
To encode an entire formula, which is a sequence of symbols, Gödel used the following system. Given a sequence of positive integers, the Gödel encoding of the sequence is the product of the first n primes raised to their corresponding values in the sequence:
enc(x1,…,xn) = 2^x1 · … pn^xn According to the fundamental theorem of arithmetic, any number (and, in particular, a number obtained in this way) can be uniquely factored into prime factors, so it is possible to recover the original sequence from its Gödel number (for any given number n of symbols to be encoded).
So, every formula can be represented as a string or even as a single natural number.
The error, informally
I will denote the set described by a set comprehension (more precisely, its numeric encoding, such as Gödel’s encoding) X as S(X).
Let M be the set comprehension
`{ X∊set comprehensions | X not in S(X) }`.
Therefore:
M in S(M) ⇔ M not in S(M).
Contradiction.
Extension by definition is erroneous
So, we have a logical paradox in our basic logic. What’s wrong?
I claim that the wrong construct is extension by definition, a construct appearing almost in every logic studybook without proof. As per Wikipedia [2]:
Let be a first-order theory (with equality) and f(y, x1, …, xn) a formula of T such that y, x1, …, xn are distinct and include the variables free in f(y, x1, …, xn). Assume that we can prove
∀x1…∀xn∃!y:f(y, x1, …, xn).
in T, i.e. for all x1, …, xn there exists a unique y such that f(y, x1, …, xn).
Further Wikipedia (and most studybooks) recommends:
Form a new first-order theory T’ from T by adding a new n-ary function symbol g , the logical axioms featuring the symbol g and the new axiom
∀x1…∀xn∃!y:g(f(y, x1, …, xn), x1, …, xn).
I will prove that following this rule (“extension by definition”) and ZF we can enter into a contradiction.
There is an obvious recursive way to define a function S from strings x to sets such that S is the set encoded by this string (in ZF) or empty set if x isn’t a valid ZF notation for a set. (To do this, first recursively check that the input formula is defining a set, not a trash of symbols in which case we return empty set, then find the encoded set recursively. So, S is a recursive function and therefore can be defined.)
Define f by the formula f(y, x) ⇔ y = S(x). Then the above g = S.
Let M be the set comprehension
`{ X∊set comprehensions | X not in S(X) }`.
Therefore:
M in S(M) ⇔ M not in S(M).
Contradiction.
In predicate logic
Note that this paradox is pertinent not to only to ZF but even to Peano Arithmetic (but only if we encode by the same number formulas differing only by variable names). We can even extend it to arbitrary predicate calculus with equality, if we allow an “external” logic to be used to check the condition:
∀x1…∀xn∃!y:f(y, x1, …, xn).
Let S(x, P) be the logical function from a pair of a variable x and encoding P of a logical formula where x is the only free variable into a one-variable predicate determining trueness of this formula for a given x. Then define Q(P) as encoding of the predicate `not (S(x, P))(P)` (for some variable x not present in P). Then S(y, Q)(Q) = not S(y, Q)(Q) (for some variable y not present in Q), because Q = `not (S(y, Q))(Q)`.
Avoiding the error
The intuition suggests: S is a function in a model of ZF, not in the formal system the proof is written. So, it’s illegal to use it in the proof.
It is an important research question, how to salvage the ZF logic.
In lambda-calculus this paradox seems not to appear: When I tried to model it in a lambda-calculus with dependent types (proof assistant Lean), I was unable to reprise the paradox even having ZF axioms, because S defined in the normal for Lean way is not an object of ZF, and therefore
S(`{ X∊set comprehensions | X not in S(X) }`)
made no sense, as it requires S to be a symbol denoting a ZF set.
Security implications
So, we have a wrong meta-logic in almost every math logic studybook. That’s a hazard.
Security implications of an error in extension by definition are almost as great, as if there were found a contradiction in ZF itself, because ZF is always used together with extension by definition in practice.
I am not yet sure whether automatic proof checkers such as Coq and Lean are affected. As I remember in Lean (maybe, in Coq, too) there is something called metalogic – that could be vulnerable.
Coq, Lean, Isabelle may be used to verify CPUs, OSes, thermonuclear weapons, nuclear power plants, air traffic control, etc. This error is a hazard.
A good news is that modern automated proof checkers (logic verifiers) use lambda-calculus not ZF or predicate logic. But they indeed may use ZF or predicate logic sometimes (in their proof libraries). Moreover, metalogics of proof checkers may have a similar bug to this bug.
The kind of the hazard is: “We built a nuclear plant. Our software is verified with an automatic logic checker, we don’t even need to debug it before turning it on. Debugging is for people who don’t know modern software security. Bump!”
P.S. Hire me! I sent the world-best engineering security bug report, in other words I am to be considered the world best security researcher.
Bibliography
[1]: Wikipedia contributors, Gödel numbering, 4 March 2022 07:24 UTC, https://en.wikipedia.org/w/index.php?title=G%C3%B6del_numbering&oldid=1075161247
[2]: Wikipedia contributors, Extension by definitions, 22 October 2021 23:49 UTC, https://en.wikipedia.org/w/index.php?title=Extension_by_definitions&oldid=1051350724