book
book copied to clipboard
HoTT
Replace 'mere proposition' with 'truth value'
To be clear, I'm not saying that we will or even necessarily that we should do this. We should think carefully about the implications before making a decision, and probably experiment on a branch to see how it looks. But it seems to have broad support on the mailing list, and no one has objected to it yet, so we should seriously consider it (for the second edition, of course). Along with the terminology change, I imagine we would explain more clearly what we consider a 'proposition' to be, and how such things can be interpreted both as general types and as truth values.
I have in the past used truth value where it was customary to say "propostion". For instance $\Omega$ in a topos is the object of truth values, although I heard people say it was the object of propositions. To me a proposition is a syntactic notion. It is a formula of a certain kind. A truth value, however, is a semantic notion. I support this issue.
On a related note, I'd be in favor of @vladimirias's way of differentiating the two kinds of existence;
- Σ (x : A) P(x) is "there is given x in A such that P(x)"
- ∃ (x : A) P(x) is "there exists x in A such that P(x)".
We should probably open a separate issue.
Sent from my iPhone
On Mar 7, 2015, at 12:44 PM, Andrej Bauer [email protected] wrote:
I have in the past used truth value where it was customary to say "propostion". For instance $\Omega$ in a topos is the object of truth values, although I heard people say it was the object of propositions. To me a proposition is a syntactic notion. It is a formula of a certain kind. A truth value, however, is a semantic notion. I support this issue.
The syntactic thing is often called a sentence (= closed formula). A proposition is someting determined by a sentence (its "intension") and determining the truth value (the "extension" of the sentence). The intension is what the sentence "means" or it's "content", and the truth-value is,well, whether it is true.
I'm not saying we are bound by these usual ways of using the terms, but we should be aware of them if we propose doing something else.
Steve
On a related note, I'd be in favor of @vladimirias's way of differntiating the two kinds of existence;
Σ (x : A) P(x) is "there is given x in A such that P(x)" ∃ (x : A) P(x) is "there exists x in A such that P(x)". We should probably open a separate issue.
— Reply to this email directly or view it on GitHub.
I think that if we adopt "truth value" for the book, we probably don't want or need to say "proposition" very much in the book at all -- I think of it as a logician's word that the ordinary mathematician isn't very familiar with. We may not even need to take a particular stand on whether a "proposition" is literally a syntactic object or its "meaning".
My brain is probably a bit skewed by computer science. I suspect computer scientists don't distinguish much between "proposition" and "boolean formula", but maybe I am just personally sloppy. In any case, thanks for point this out.
By the way, if we go with 'truth value' we will need to rename some other things too, like 'propositional truncation' and 'propositional resizing'.
For me, "truth value" refers to either "true" or "false", that we can identify with the terms of type 2 (as mentionned in chapter 1.8). So with my background, I see two problems with your proposal:
- a proposition in classical logic HAS a truth value (true or false), but cannot be said to BE a truth value. May be this is the opinion of a (amateur) logician, and mathematicians use 'proposition' with a different meaning ?
- I feel that 'truth value' implicitely refers to LEM, which we would like to avoid in HoTT.
If something must be changed, I would propose instead to:
- explain that a type is a sort of 'higher proposition'
- replace 'mere proposition' with just 'proposition' (as it is done in Coq with the Prop type).
"Every truth value is either true or false" is precisely excluded middle. Intuitionistic logic however only validates "No truth value is different from both true and false". This is perhaps a subtle difference, but my point is that your view is not contradictory with intuitionistic logic if you are willing to rephrase it a little bit.
There is definitely a difference between propositions and truth values. Unfortunately, even logicians are sometimes sloppy about making the distinctions between them.
@louisGarde: Using “truth-value” in non-classical settings is very well-established; e.g. in topos theory, referring to Ω as an “object of truth-values”. So I don’t think “truth-value” is understood to implicitly refer to LEM, in most non-classical traditions.
