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