Тем временем Рэндалл Холмс, профессор математики из Айдахо, объявил, что придумал доказательство противоречивости PA (арифметики Пеано), причём второго порядка; это значит по сути дела, что натуральных чисел в том виде, в каком мы их обычно понимаем, нет модели; или, иными словами, он нашёл противоречие внутри стандартной модели натуральных чисел N.
Это ещё несравнимо менее вероятно, чем противоречие в теории множеств. Доказательство Холмса можно сгрузить в формате PDF с его домашней страницы, в самом начале её.
Это меня совсем уж возмутило, так что я распечатал доказательство Холмса (небольшое, 6 страниц), прочитал его и нашёл ошибку. В рассылку отправлять не стал, написал прямо ему. Копию помещаю внизу под lj-cut'ом (но её бесполезно читать, если вы не прочитали док-во Холмса, так как я использую введённую им терминологию; само же доказательство я рекомендую читать только особо любопытным или желающим самим найти ошибку. Математической пользы в нём нет).
Dear Prof. Holmes, Let I be an interpretation for (U,n) and I' an interpretation for (U',n). I' is said to extend I if U(i) and I(i) are subsets of U'(i) and I'(i) for all i<=n. What does it mean for a subset of I(i) to be a subset of I'(i)? I(i) is a pre-interpretation for (U(i),n): a mapping which sends every assignment of variables <=n to members of the set U(i), plus a formula <=n, to {0,1}. Members of I(i) are pairs < <assignment,formula>, truth-value >. So technically speaking, I(i) being a subset of I'(i) means that truth values of formulas stay the same as long as assignments remain within original U(i)'s. That won't preserve correctness. For example, consider a true (in the standard model) existential sentence (Ex)phi(x), which is mapped to "false" under some I(i) because U(i-1) is not large enough to contain the witness for phi(x). Since it's a sentence, it'll have the same truth value under any assignment (provided I is correct, of course). You want this sentence to be mapped to "true" when you extend U(i-1) to include the witness for phi(x); but under your definition the truth value of (Ex)phi(x) can't change when I is extended to I'. Perhaps what you mean by I' extending I is that each U'(i) extends U(i), and the set of those pairs <assignment, formula> which are mapped to "true" by I to remain so mapped by I'. That won't help you though, because correctness demands not only conversion of some "false" formulas to "true" formulas under same assignments as I is extended to I', but also conversion of some "true" formulas to "false" formulas - for instance, negations of existential formulas (negation being suitably defined with the help of your neither/nor operator). Basically, as you extend U(i) to U'(i), some formulas on which I(i+1) acts change from "false" to "true", and others from "true" to "false", under their original assignments within U(i+1). There is no relation between I' and I that you can formalise and that will allow you to preserve truth of formulas under extension (assuming correctness of interpretations). You can still formalise "correct", and you can still define a veridical interpretation to be such that it can be gradually extended, preserving correctness, to encompass any given sets, but since the interpretations aren't conservative extensions of each other, it doesn't follow that a formula true in such a veridical interpretation is true in the standard model (and in fact, "veridical" simply collapses to "correct"). The only thing that can be salvaged from the proof is definability of truth for purely existential formulas (meaning those that only have existential quantifiers in the prenex form), which is trivial.