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