CIRCLE WITH A DOT

@MartinEscardo I will never be able to top that one.

Y'all noticed the date on that was April 1, right?

(contd.)

Note further that for any such path α and any k ∈ ℕ we have

(∃ n . Prf(k, n)) ⇒ αₖ = 1.

Indeed, if there is n such that Prf(k, n) then from a := [α₀, ..., aₙ] ∈ 𝔾 follows αₖ = aₖ = 1. Moreover, since α is Turing-computable by some x ∈ ℕ, as above, Peano arithmetic proves

(∃ n . Prf(k, n)) ⇒ ∃ i . T(x, k, i) ∧ U(i) = 1. (1)

Similarly, it proves

(∃ n . Rft(k, n)) ⇒ ∃ j . T(x, k, j) ∧ U(j) = 0. (2)

We are now ready to put it all together. It suffices to show that Peano arithmetic proves

¬ ∃ k . (∃ n . Prf(k, n)) ∧ (∃ m . Rft(k, n))

which informally states that there is no sentence ξₖ that is both provable and refutable. This is (intuitionistically!) equivalent to

∀ k . ¬ ((∃ n . Prf(k, n)) ∧ (∃ m . Rft(k, n))).

By (1) and (2), the statement follows in PA (already in HA) from

∀ k . ¬ ((∃ i . T(x, k, i) ∧ U(i) = 1) ∧ (∃ j . T(x, k, j) ∧ U(j) = 0)).

But this is easy to prove: if T(x, k, i) and T(x, k, j) for some i and j, then i = j because execution traces are unique, which yields a contradiction 1 = U(i) = U(j) = 0.

2/2

In the effective topos Peano arithmetic (assuming it is consistent) defies Gödel's second incompleteness theorem, which states that Peano arithmetic cannot prove its own consistency. This is made possible by the effective topos validating “everything is computable”.

We argue internally in the effective topos. The argument is a bit long but it uses only standard techniques.

We need some notation first. Let ξ₀, ξ₁, ξ₂, ξ_3, ... be a standard enumeration of the sentences of Peano arithmetic. Let Prf(k, n) be the arithmetical statement coding “n is a Gödel code of a proof of ξₖ” and Rft(k, n) be the arithmetical statement coding “n is a Gödel code of a proof of ¬ξₖ”.

If a ∈ {0,1}* is a finite binary sequence, let |a| be its length. Define the binary tree

𝔾 := { a ∈ {0,1}* | ∀ k, n < |a| . (Prf(k, n) ⇒ aₖ = 1) ∧ (Rft(k, n) ⇒ aₖ = 0) }

In words, a ∈ 𝔾 when the sequence a approximates the decidability of the first |a| sentences of Peano arithmetic.

The tree 𝔾 is obviously infinite: to get a ∈ 𝔾 of any desired length m, consider the sequence a of length m defined by aₖ := 1 ⇔ ∃ n < m, Prf(k, n), noting that the condition is decidable and that Prf(k, n) and Rft(k, n) cannot both hold simultaneously.

Any infinite path α : ℕ → {0,1} through 𝔾 is computable by formal Church's thesis (valid in the effective topos), i.e., there is x ∈ ℕ such that ∀ k ∃ j . T(x, k, j) ∧ U(j) = αₖ, where T and U are Kleene's predicates (which are primitive recursive and so expressible in Peano arithmetic). Recall that T(x, k, j) expresses “j encodes a terminating computation of the x-th Turing machine on input k”. For every x and k there is at most one such j, and Peano arithmetic proves this fact.

1/2

@mc @JacquesC2 @cbaberle @johncarlosbaez @dougmerritt @MartinEscardo @pigworker @xenaproject I'd go further and "blame" the philosophers of language, too.

@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject Well, it should be obvious, but let me say it anyway.

We need mathematicians of every kind: the thinkers, the dreamers, the formalizers, and even physicists.

@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker Somewhat unexpectedly, I find myself on the same side as @xenaproject on this one, I suppose because I read "the right way" differently from @johncarlosbaez

Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty.

Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule.

Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each peddling its own foundation, has only contributed to plurality of mathematical thought.

Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @MartinEscardo and myself), testifying to their creative potential.

Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is a hollow one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.