Hmm… so, interestingly enough, the proof is actually much simpler than both yours and the one on Wikipedia when written up in Agda.
Interestingly enough though, just the notion of provability being equivalent to proof doesn’t actually lead to an inconsistency in Agda—the positivity checker prevents the declaration of a Löb sentence. But, if you admit the sentence, everything breaks in about the way you’d expect.
EDIT 1: So I seem to have misunderstood Löb’s theorem. Going to redo it and update the gist when I think it makes more sense.
EDIT 2: Updated the gist, should actually contain a valid proof of Löb’s theorem now
When you make a data declaration like this, you are essentially postulating (A → □ A) and (□ A → A), for any formula A. This essentially removes the distinction between A (the formula A is “true”) and □ A (the formula A is “provable”), meaning you are not working inside the modal logic you think you are working in. We made the same mistake in the /r/haskell thread at first.
It’s an easy mistake to make, because the first rule of inference for provability logic is
⊢ A
------
⊢ □ A
So it looks like (A → □ A) should be a theorem, but notice that the left-hand side of the turnstile is empty. This means that the rule is only valid when there are no assumptions in context; or equivalently in a programming language, when there are no variables in scope. Since Agda doesn’t know how to talk about which Agda variables are in scope, we cannot implement this rule as an Agda function, which would be available whether the scope is empty or not.
A few examples would probably help. A valid use of inference rule 1 would look like this:
----- variable rule
A ⊢ A
--------- deduction rule
⊢ (A → A)
----------- inference rule 1
⊢ □ (A → A)
Here, we have used inference rule 1 and a few other common rules to prove that the trivial implication (A → A) is “provable”. By comparison, here is what happens when we try to use the same technique to prove that all “true” statements are “provable”, i.e. (A → □ A). (I put “true” and “provable” in quotes in order to distinguish “provable according to the map” from provable in the territory. Provability logic is a map we use to understand provability.)
----- variable rule
A ⊢ A
------- inference rule 1 (invalid, the context is not empty)
A ⊢ □ A
--------- deduction rule
⊢ A → □ A
As you can see, the proof is invalid. And that’s a good thing, too, because if we could prove that all “true” statements were “provable”, then our provability logic would have allowed us to prove something which we know to be false, so the logic would have been a poor model of real-world provability.
Anyway, the conclusion of all this is that we should not represent inference rule 1 by an Agda function from A to □ A, but by an object of type “Theorem (A ⇾ Provable A)”, where “⇾” is a syntactic construct representing implication, not an Agda function.
I’m not really seeing the importance of the separate construct Theorem (A → B) vs (A → B). It seems to get manipulated in the exact same way in the code above. Is there some extra capability of functions that Theorem + postulates doesn’t include?
Also, I think you’re misunderstanding what a function A → B means in Agda. A → □ A doesn’t mean “all true statements are provable”, it means “all statements we can construct a proof term for are provable”—you don’t get an element of type A to apply that to without a proof of A, so it’s actually a pretty trivial implication. I’m actually tempted to say that the notion of provability is actually wholly unnecessary here because of the Curry-Howard Correspondence, and that the real issue is the construction of the fixpoint
A → □ A doesn’t mean “all true statements are provable” [...]
I agree! You are right, the formula “A → □ A” does not mean that all true statements are provable. It means that all “true” statements are “provable” :)
Discussing the math of provability is tricky, because there are many notions of truth and many notions of provability. There are true-in-the-real-world and provable-in-the-real-world, the notions we are trying to model. True-in-the-real-world does not imply provable-in-the-real-world, so ideally, we would like a model in which there are no rules to infer provable-in-the-model from true-in-the-model. Provability logic provides such a model: it uses “A” for true-in-the-model, and “□ A” for provable-in-the-model.
One extra level of complexity is that “provable-in-the-model” is not the same as “provable-in-the-real-world by following the rules of the model”, which I’ll abbreviate as “derivable”, or “PL-derivable” when the model is Provability logic. The reason the two are different is that “□ A” only represents provability; the actual rules of the model don’t care what meaning we assign to the symbols. If the rules were poorly chosen, it could very well be that a formula “□ A” was PL-derivable but that the formula “A” wasn’t.
A → □ A [...] means “all statements we can construct a proof term for are provable”
Yes and no. Yes, at runtime, all the values we will actually receive will have been constructed by our callers. No, Agda implications do not always mean that if the left-hand side is constructible, so it the right-hand side. Implications of the form (A → ⊥), for example, mean that the left-hand side is not constructible. In that case, we never receive any value from our callers, and we implement (A → ⊥) by writing a constructive proof that all possible inputs are absurd.
But even if we ignore this corner case, it would only be justified to conclude that receiving an A as input implies that an Agda proof for A exists. Löb’s theorem is not about Agda, but about a specific model of provability encoded by the rules of provability logic. If your proof uses (A → □ A) as an assumption (as opposed to ⊢ A → ⊢ □ A), then your proof is not a proof of Löb’s theorem, because that theorem makes no such assumption.
EDIT 2: Updated the gist, should actually contain a valid proof of Löb’s theorem now
Your latest version at the time of writing is revision 6, which uses a postulate
postulate
ev : ∀ {A} → A → □ A
instead of the data declaration
data □_ (A : Set β) : Set (suc β)
ev : A → □ A
That is, you have removed the (□ A → A) direction, but kept the (A → □ A) direction. That’s a bit better, but you’re still using the forbidden assumption.
the real issue is the construction of the fixpoint
Is there some extra capability of functions that Theorem + postulates doesn’t include?
Oh yes, tons. Try constructing a value with type Theorem Integer :-) The world under Theorem is much more restricted.
A→□A doesn’t mean “all true statements are provable”, it means “all statements we can construct a proof term for are provable”
Well, not quite. The □ operator in the original proof doesn’t mean provability from the premises of the theorem, it means provability in bare bones PA, starting from nothing. We want to only use assumptions that are true under that interpretation of □, which means they must hold in provability logic (GL). And the assumption A→□A doesn’t hold in GL.
The assumptions used in the original proof are ⊢A→⊢□A and ⊢(□A→□□A), both of which hold in GL. I think the simplest way to encode these is to use separate constructs for ⊢ and □, as I did in the post.
I don’t completely understand how your code corresponds to a proof of Löb’s theorem. Are you assuming that ⊢(☐A→A) holds for all sentences A? In Löb’s theorem it’s assumed to hold only for the sentence P.
Hmm… so, interestingly enough, the proof is actually much simpler than both yours and the one on Wikipedia when written up in Agda.
Interestingly enough though, just the notion of provability being equivalent to proof doesn’t actually lead to an inconsistency in Agda—the positivity checker prevents the declaration of a Löb sentence. But, if you admit the sentence, everything breaks in about the way you’d expect.
I’ve uploaded it as a gist here
EDIT 1: So I seem to have misunderstood Löb’s theorem. Going to redo it and update the gist when I think it makes more sense. EDIT 2: Updated the gist, should actually contain a valid proof of Löb’s theorem now
When you make a data declaration like this, you are essentially postulating (A → □ A) and (□ A → A), for any formula A. This essentially removes the distinction between A (the formula A is “true”) and □ A (the formula A is “provable”), meaning you are not working inside the modal logic you think you are working in. We made the same mistake in the /r/haskell thread at first.
It’s an easy mistake to make, because the first rule of inference for provability logic is
So it looks like (A → □ A) should be a theorem, but notice that the left-hand side of the turnstile is empty. This means that the rule is only valid when there are no assumptions in context; or equivalently in a programming language, when there are no variables in scope. Since Agda doesn’t know how to talk about which Agda variables are in scope, we cannot implement this rule as an Agda function, which would be available whether the scope is empty or not.
A few examples would probably help. A valid use of inference rule 1 would look like this:
Here, we have used inference rule 1 and a few other common rules to prove that the trivial implication (A → A) is “provable”. By comparison, here is what happens when we try to use the same technique to prove that all “true” statements are “provable”, i.e. (A → □ A). (I put “true” and “provable” in quotes in order to distinguish “provable according to the map” from provable in the territory. Provability logic is a map we use to understand provability.)
As you can see, the proof is invalid. And that’s a good thing, too, because if we could prove that all “true” statements were “provable”, then our provability logic would have allowed us to prove something which we know to be false, so the logic would have been a poor model of real-world provability.
Anyway, the conclusion of all this is that we should not represent inference rule 1 by an Agda function from A to □ A, but by an object of type “Theorem (A ⇾ Provable A)”, where “⇾” is a syntactic construct representing implication, not an Agda function.
I’m not really seeing the importance of the separate construct Theorem (A → B) vs (A → B). It seems to get manipulated in the exact same way in the code above. Is there some extra capability of functions that Theorem + postulates doesn’t include?
Also, I think you’re misunderstanding what a function A → B means in Agda. A → □ A doesn’t mean “all true statements are provable”, it means “all statements we can construct a proof term for are provable”—you don’t get an element of type A to apply that to without a proof of A, so it’s actually a pretty trivial implication. I’m actually tempted to say that the notion of provability is actually wholly unnecessary here because of the Curry-Howard Correspondence, and that the real issue is the construction of the fixpoint
I agree! You are right, the formula “A → □ A” does not mean that all true statements are provable. It means that all “true” statements are “provable” :)
Discussing the math of provability is tricky, because there are many notions of truth and many notions of provability. There are true-in-the-real-world and provable-in-the-real-world, the notions we are trying to model. True-in-the-real-world does not imply provable-in-the-real-world, so ideally, we would like a model in which there are no rules to infer provable-in-the-model from true-in-the-model. Provability logic provides such a model: it uses “A” for true-in-the-model, and “□ A” for provable-in-the-model.
One extra level of complexity is that “provable-in-the-model” is not the same as “provable-in-the-real-world by following the rules of the model”, which I’ll abbreviate as “derivable”, or “PL-derivable” when the model is Provability logic. The reason the two are different is that “□ A” only represents provability; the actual rules of the model don’t care what meaning we assign to the symbols. If the rules were poorly chosen, it could very well be that a formula “□ A” was PL-derivable but that the formula “A” wasn’t.
Yes and no. Yes, at runtime, all the values we will actually receive will have been constructed by our callers. No, Agda implications do not always mean that if the left-hand side is constructible, so it the right-hand side. Implications of the form (A → ⊥), for example, mean that the left-hand side is not constructible. In that case, we never receive any value from our callers, and we implement (A → ⊥) by writing a constructive proof that all possible inputs are absurd.
But even if we ignore this corner case, it would only be justified to conclude that receiving an A as input implies that an Agda proof for A exists. Löb’s theorem is not about Agda, but about a specific model of provability encoded by the rules of provability logic. If your proof uses (A → □ A) as an assumption (as opposed to ⊢ A → ⊢ □ A), then your proof is not a proof of Löb’s theorem, because that theorem makes no such assumption.
Your latest version at the time of writing is revision 6, which uses a postulate
instead of the data declaration
That is, you have removed the (□ A → A) direction, but kept the (A → □ A) direction. That’s a bit better, but you’re still using the forbidden assumption.
I agree, that part does look hard to implement.
Oh yes, tons. Try constructing a value with type Theorem Integer :-) The world under Theorem is much more restricted.
Well, not quite. The □ operator in the original proof doesn’t mean provability from the premises of the theorem, it means provability in bare bones PA, starting from nothing. We want to only use assumptions that are true under that interpretation of □, which means they must hold in provability logic (GL). And the assumption A→□A doesn’t hold in GL.
The assumptions used in the original proof are ⊢A→⊢□A and ⊢(□A→□□A), both of which hold in GL. I think the simplest way to encode these is to use separate constructs for ⊢ and □, as I did in the post.
I don’t completely understand how your code corresponds to a proof of Löb’s theorem. Are you assuming that ⊢(☐A→A) holds for all sentences A? In Löb’s theorem it’s assumed to hold only for the sentence P.