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.
-
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
-
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
(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
@andrejbauer If you know about the Kleene tree it's not too hard to spot the problem with this one.
-
@andrejbauer If you know about the Kleene tree it's not too hard to spot the problem with this one.
@aws Why will I never learn to check the date when reading posts by @andrejbauer ?
-
(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
Y'all noticed the date on that was April 1, right?
-
Y'all noticed the date on that was April 1, right?
@andrejbauer Yeah, like when you posted about the countable reals in a previous April fools?
-
@andrejbauer Yeah, like when you posted about the countable reals in a previous April fools?
@MartinEscardo I will never be able to top that one.
-
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
@andrejbauer@mathstodon.xyz I'll admit that this is very cool stuff that is on the edge of my comprehension.
-
R relay@relay.infosec.exchange shared this topic
