Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

Comment author: gallabytes 20 September 2014 07:40:51PM *  2 points [-]

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

Comment author: gelisam 21 September 2014 05:10:08AM 3 points [-]

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

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

I agree, that part does look hard to implement.

Comment author: gallabytes 20 September 2014 08:07:10AM *  3 points [-]

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

Comment author: gelisam 20 September 2014 01:38:20PM *  7 points [-]

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.

Comment author: yli 24 December 2012 11:08:28AM *  9 points [-]

Maybe it's just that volunteers that will actually do any work are hard to find. Related.

Personally, I was excited about doing some LW development a couple of years ago and emailed one of the people coordinating volunteers about it. I got some instructions back but procrastinated forever on it and never ended up doing any programming at all.

Comment author: gelisam 24 December 2012 04:27:20PM 3 points [-]

I understand how that might have happened. Now that I am no longer a heroic volunteer saving my beloved website maiden, but just a potential contributor to an open source project, my motivation has dropped.

It is a strange inversion of effect. The issue list and instructions both make it easier for me to contribute, but since they reveal that the project is well organized, they also demotivate me because a well-organized project makes me feel like it doesn't need my help. This probably reveals more about my own psychology than about effective volunteer recruitment strategies, though.

Comment author: kodos96 24 December 2012 07:59:05AM 1 point [-]

This would be a poor investment of time without first getting a commitment from Eliezer that he will accept said patch.

Comment author: gelisam 24 December 2012 03:40:49PM *  2 points [-]

After finding the source and the issue list, I found instructions which indicate that there is, after all, non-zero engineering resources for lesswrong development. Specifically, somebody is sorting the incoming issues into "issues for which contributions are welcome" versus "issues which we want to fix ourselves".

The path to becoming a volunteer contributor is now very clear.

Comment author: Eliezer_Yudkowsky 24 December 2012 05:00:00AM 5 points [-]


Comment author: gelisam 24 December 2012 07:24:29AM 12 points [-]

Are you kidding? Sign me up as a volunteer polyglot programmer, then!

Although, my own eagerness to help makes me think that the problem might not be that you tried to ask for volunteers and didn't get any, but rather that you tried to work with volunteers and something else didn't work out.

Comment author: gelisam 24 October 2012 04:07:14AM 0 points [-]

I'm pretty sure I would come up with a reason to continue behaving as today. That's what I did when I discovered, to my horror, that good and bad were human interpretations and not universal mathematical imperatives. Or are you asking what the rational reaction should be?

In response to comment by gelisam on SotW: Be Specific
Comment author: beoShaffer 07 April 2012 03:08:24PM 0 points [-]

The whole seeing with fresh eyes subsequence is relevant, cached thoughts and the genetic fallacy are probably the most relevant.

Comment author: gelisam 12 April 2012 10:34:28PM 0 points [-]

Thanks for the suggestion. This is not, however, what I was looking for.

Cached thoughts explains that hearing a phrase might be enough for our brain to remember it as true, while genetic fallacy warns that the original cause of a belief is not as important as the sum-total of evidence for or against that belief.

I am not, however, looking for evidence that our past taints our beliefs. I have come to realize that finding the historical cause of a thought is a good first step towards getting rid of an unwanted thought, and I wanted to know whether this strategy was covered yet. If not... I'll accumulate a bit more evidence, and then maybe I'll write a post!

In response to SotW: Be Specific
Comment author: gelisam 06 April 2012 05:14:00PM *  0 points [-]

search for the historical causes of your thoughts, rather than their justifications.

Is there a standard name or LW article on the subject? I first stumbled upon the importance of that skill here, on this site, and I wish I knew more about it than just that one personal anecdote.

Comment author: gelisam 12 August 2010 09:19:35PM 6 points [-]

Great case study, in that studying my own reaction to your article has thought me a lot about my own decision making. And my conclusion is that reading a rationalist blog isn't sufficient to become rational!

I am thin, despite having very bad eating habits (according to conventional dietary wisdom). I had not heard of Taubes before. Specifically, I have never considered that conventional dietary wisdom could be incorrect; people say that I eat unhealthily, and I have simply taken their word for it. The fact that I continue to eat unhealthily has more to do with laziness than rationality.

How much have I shifted my beliefs now that I have read this article? I don't think in probabilities yet, but... by a lot. Probably more than I should. Neither Taubes' belief nor bentarm's belief nor Eliezer's belief nor Taubes' lack of biological credentials has affected my own degree of belief, not by much anyway. Just the fact that there exists an alternative theory of food has succeeded in demolishing the confidence I had in the conventional theory.

How could such a weak amount of evidence cause such a large shift? By relying on a bias which happened to be pushing in the same direction. Just ask me: "since you have decreased your belief in the conventional theory after reading an article on Taubes, you must have correspondingly increased your belief in Taubes' theory, right?"

Well, let me google whether the fatty food I currently eat is high-carb or low-carb, and I'll get back to you on that.

Comment author: lsparrish 29 July 2010 01:49:54PM 0 points [-]

I don't think the post was banned out of concern for influencing the future AI's actions, so much as out of concern that it would destabilize the mentality of some community members and distract from its mission.

It's a shame too because it contains an idea that could be productively developed, i.e. acausal disciplinary action. Within strict limits, I don't have a problem with that concept (given sufficient reward).

Comment author: gelisam 29 July 2010 03:48:33PM 11 points [-]

Unfortunately, I think the ban might have the inverse effect. Just reading the post wasn't particularly frightening to me, because I didn't really understand its implications. But Eliezer is a specialist, so if he thinks the post might be dangerous, then damn, maybe it is dangerous, and maybe reading it has put me in danger!

This line of thought has indeed managed to frighten me, and it frequently returned during the remainder of the day. I feel much better now, thank you very much; but I can easily imagine how people who understood the post better than I did could still be very worried. Best of luck!

View more: Next