= 27d567bc2d48d9f40e9ccc20ea370b15)
eli_sennesh comments on Rationality Quotes June 2014 - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (279)
-- Johan George Granstrom, Treatise on Intuitionistic Type Theory
The value of these definitions is completely opaque to me. Could you elaborate on why you believe this is a good rationality quote?
Because it emphasizes that logic is a machine with strict laws and moving parts, not a pool of water to be sloshed in any direction. When you lay down what counts as a (hypothetical) cause of a proposition, you define it clearly and subject it to proof or disproof. When you demonstrate that one proposition causes another, you send truth from effects into causes according to the laws of proof.
Implication, deductibility, and computation are thus the exact same thing.
But what does it mean for one proposition to cause another? For instance, here's a true proposition: "Either Hilary Clinton is the President of the United States or there exists a planet in the solar system that is smaller than Earth." What is the cause of this proposition?
Also, when Granstrom says a proposition is true if it has a cause, what does that mean? What is "having" a cause? Does it mean that in order for a proposition to be true, its hypothetical cause must also be true? That would be a circular definition, so I'm presuming that's not it. But what then?
In the sense of implication?
A well-formed OR proposition comes with the two alternatives and a cause for one of the alternatives. So in this case, a cause (or evidence, we could say) for "there exists a planet in the solar system smaller than Earth" is the cause for the larger OR proposition.
In this case, cause is identified with computation. When we have an effective procedure (ie: a computation) taking any cause of A into a cause of B, we say that A implies B.
This is true, but the recursion hits bottom when you start talking about propositions about mere data. Constructive type theory doesn't get you out of needing your recursive justifications to bottom-out in a base case somewhere.
2 is somewhere between wrong and not even wrong. Propositions are regarded, by those who believe in them as abstracta , and as such, non causal. Setting that aside, it's obvious that, say, a belief can have cause but be wrong. Fori instance, someone can acquire a false believe as the causal consequence of being lied to.
I agree that this is how propositions are usually regarded. The impression I got from the quote, though, is that Granstrom is proposing a re-definition of "proposition", so saying it's wrong seems like a category error. It does seem like a fairly pointless re-definition, though, which is why I asked the question.