proof of impossibility of infinite proofs

Stream: lean4

[Andrés Goens]

Is there any way to prove that an inductive proposition is false because proving it is true would require an infinite proof? That's how I would argue informally at least. Concretely, consider something like:

inductive MyProp : Nat → Bool → Prop
  | zero_false : MyProp 0 false
  | n_true (n : Nat) : MyProp n true
  | false_false (n : Nat) : MyProp (n+1) false → MyProp n false

theorem one_not_false : ¬ (MyProp 1 false) := by
  intro h
  cases h with
    | false_false _ hn => sorry -- hn : MyProp (1 + 1) false

Here, I could continue to destruct the proofs infinitely building larger and larger proofs, but there's never going to be a proof of it

[Andrés Goens]

(deleted)

[Andrés Goens]

(deleted)

[Eric Rodriguez]

I want to say that you have to use noConfusion or something of the like but I'm stumped

[Eric Wieser]

We use infinite proofs all the time, it's induction

[Eric Wieser]

But you need to generalize first to the point that Lean allows you to use the induction tactic:

theorem one_not_false : ¬ (MyProp 1 false) := by
  suffices ∀ (n : Nat) b, n ≠ 0 → b = false → ¬ (MyProp n b) by
    exact this _ _ Nat.one_ne_zero rfl
  intro n b hn hb h
  induction h with
  | zero_false => exact hn rfl
  | n_true => cases hb
  | false_false n _hn ih => exact ih (Nat.succ_ne_zero _) rfl

[Andrés Goens]

Eric Wieser said:

We use infinite proofs all the time, it's induction

point taken! although induction is not an infinite proof ofc (by infinite proof I mean an infinite term in Lean's underlying type theory)

[Eric Wieser]

You could argue that induction is a way to avoid such a proof

[Andrés Goens]

Eric Wieser said:

But you need to generalize first to the point that Lean allows you to use the induction tactic:

theorem one_not_false : ¬ (MyProp 1 false) := by
  suffices ∀ (n : Nat) b, n ≠ 0 → b = false → ¬ (MyProp n b) by
    exact this _ _ Nat.one_ne_zero rfl
  intro n b hn hb h
  induction h with
  | zero_false => exact hn rfl
  | n_true => cases hb
  | false_false n _hn ih => exact ih (Nat.succ_ne_zero _) rfl

that makes a lot of sense, thank you!

[Kevin Buzzard]

When teaching induction (just on naturals) to mathematicians, I like to point out that if you know P(0) and that P(n) implies P(n+1), then for any given number t you can prove P(t), but clearly as t gets bigger the proof term gets bigger, and proofs are supposed to be finite, so it's not at all clear that "for all t, P(t)" has a finite proof. Once a student told me after one such lecture that they came into it understanding induction very well and left it totally confused, a comment which I took as a huge compliment.

[Martin Dvořák]

Peano arithmetic states it as an axiom. This axiom is not redundant.

Technically speaking, it is infinitely many axioms, but...

[Kevin Buzzard]

Yes exactly: the argument I present is evidence that some kind of magic is needed, and then I explain that it's OK because induction is an axiom in mathematics. The example is an explanation of why a common "proof" of induction fails. Basically every proof of induction uses induction somehow.

[Jireh Loreaux]

The proof terms for different n don't need to get bigger for this Kevin, they only need to be distinct. So, I'm not sure this is particularly convincing to me. I'm not saying you don't need induction.

[Martin Dvořák]

Let P be a unary relation on ℕ.
Let P(0) and ∀ n, P(n) => P(n+1) hold.

Now, if you don't have the axiom(s) of induction, then...
For each n, you can have a proof of P(n).
However, you cannot have a proof of ∀ n, P(n).

[James Gallicchio]

reminds me of one of Paige's HoTTEST lectures where they talked about how much of HoTT is motivated by the desire to internalize meta-reasoning...

[Yaël Dillies]

Martin, are you sure? What you're describing sounds more like generalisation. Int is a model of Peano arithmetic without induction/recursion, so losing induction is losing basically everything.

[Martin Dvořák]

Are you talking about integers? They are not a model of Robinson arithmetic.

[Pedro Sánchez Terraf]

Martin Dvořák said:

Without the axiom(s) of induction:

For each n, you can have a proof of P(n).
However, you cannot have a proof of ∀ n, P(n).

An instance of this phenomenon is Goodstein's theorem. The proof terms not only grow with n, but the problem is that they do not do so uniformly. So you state it in Peano Arithmetic but not prove it there.

[Martin Dvořák]

Pedro Sánchez Terraf said:

An instance of this phenomenon is Goodstein's theorem. The proof terms not only grow with n, but the problem is that they do not do so uniformly. So you state it in Peano Arithmetic but not prove it there.

That is a different phenomenon. I was talking about the necessity of the induction scheme, i.e., how Peano arithmetic differs from Robinson arithmetic.

[Eric Rodriguez]

Jireh Loreaux said:

The proof terms for different n don't need to get bigger for this Kevin, they only need to be distinct. So, I'm not sure this is particularly convincing to me. I'm not saying you don't need induction.

if you use induction they do have to be different right? I think Kevin means in the case that P(x+1) depends on P(x) explicitly.

[Jireh Loreaux]

Of course. My issue is necessarily informal. Let me try to explain.

1. I agree that the proof terms for P(n) for different n are growing (and distinct) for different values of n.
2. I realize that some form of induction is necessary (whether proven from other principles or as an axiom)

My point had basically two parts: (1) Kevin's argument that you need induction because otherwise the proof is infinite doesn't require that the terms be growing, only that they are distinct. (2) Even for a statement like ∀ n : ℕ, n + 2 = (n + 1) + 1 where P : ℕ → Prop is the predicate, then the proof terms of P 0 and P 1 ... are all distinct because n varies. And yet, because they are just add_assoc 0 1 1, add_assoc 1 1 1, ... , we can just prove the above with fun n ↦ add_assoc n 1 1. (Of course, I realize that add_assoc uses induction under the hood, but that's beside the point.)

So my argument is essentially that just because one way to write a proof doesn't work because it would be infinitely long doesn't mean that there's no way to write it without appealing to magic (i.e., induction). In this case, I agree that induction is necessary, but I would not have been convinced by Kevin's argument were I a student in his class.

[Mac Malone]

Jireh Loreaux said:

Of course, I realize that add_assoc uses induction under the hood, but that's beside the point.)

Isn't that precisely the point, though? At some level, to prove any of these things requires induction.

So my argument is essentially that just because one way to write a proof doesn't work because it would be infinitely long doesn't mean that there's no way to write it without appealing to magic (i.e., induction).

And since they require induction at some level, their soundness rests on the soundness of the induction axiom within the theory (and thus requires appealing to its magic). Some forms of finitism are born from those who find this magic deficient in some way. One such interesting example is elementary finite arithmetic, which prohibits unbounded induction (e.g.,∀ n, P(n)), but is still able to prove a significant subsection of mathematics.

[Jireh Loreaux]

You can remove the add_assoc use of induction in my example though just by adding it as a hypothesis and my argument stands.

Again, I'm not arguing against the actual need for induction, only against the specifics of Kevin's argument about why it's necessary.

[Kevin Buzzard]

I don't tell them this story to convince them, I tell it to confuse them :-)

[Andrés Goens]

Mac Malone said:

Jireh Loreaux said:

Of course, I realize that add_assoc uses induction under the hood, but that's beside the point.)

Isn't that precisely the point, though? At some level, to prove any of these things requires induction.

So my argument is essentially that just because one way to write a proof doesn't work because it would be infinitely long doesn't mean that there's no way to write it without appealing to magic (i.e., induction).

And since they require induction at some level, their sounds rests on the soundness of the induction axiom within the theory (and thus requires appealing to its magic). Some forms of finitism are born from those who find this magic deficient in some way. One such interesting example is elementary finite arithmetic, which prohibits unbounded induction (e.g.,∀ n, P(n)), but is still able to prove a significant subsection of mathematics.

oh interesting, so essentially people build a sort of mathematics without infinite objects whatsoever? I'm curious, do you what is the relationship between the axiom of infinity in ZFC and the induction principle?

[James Gallicchio]

https://en.wikipedia.org/wiki/Ultrafinitism this article is a lovely ride

[Mac Malone]

Andrés Goens said:

I'm curious, do you what is the relationship between the axiom of infinity in ZFC and the induction principle?

As the Wikipedia page on the formalization of Mathematical inductions states, the induction principle is a theorem of ZFC. Perhaps surprisingly, strong induction does not necessarily require the axiom of infinity, and Peano arithmetic and ZF without infinity are much the same. For example, it can be proved with just the axioms of foundation and the axiom schema of restricted comprehension (see this Reddit post for a proof sketch). What the axiom of infinity gets ZF is that class of the (infinite) natural numbers is a set within ZF rather than just a class. In fact, this distinction is also related to the distinction between a classic and strict finitist. A classic finitist just denies infinite sets (i.e., the axiom of infinity), whereas a strict finitist would also deny potential infinites (i.e., the principle of induction). At least, that is how I understand it.