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 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.