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?
But what does it mean for one proposition to cause another?
In the sense of implication?
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?
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.
Also, when Granstrom says a proposition is true if it has a cause, what does that mean? What is “having” a cause?
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.
Does it mean that in order for a proposition to be true, its hypothetical cause must also be true?
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.
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.