Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added to decidable equality some remarks on the difference between the propositions-as-types version and the propositions-as-some-types version.
Nice!
Over here somebody shows that he found the paragraph at decidable equality on Applications confusing.
I suppose the paragraph was okay in itself and no expert would have found it confusing, but I see how for a novice it may not have been clear enough that throughout the entry the word “set” means different things depending on whether it is understood that one speaks constructively or not.
In any case, I have edited ever so slightly in an attempt to clarify. But please feel invited to edit further.
Removed incorrect statement that “(though the same is not true for finitely-indexed or subfinite sets)”
Subfinite sets have decidable equality because they are subsets of a finite set, and equality is preserved and reflected for the canonical injection of a subfinite set into the corresponding finite set, by definition of injection.
Anonymouse
Added examples of the Cantor space having decidable equality if and only if WLPO holds and the Dedekind reals having decidable equality if and only if analytic WLPO holds, and a remark that these represent examples of sets with decidable equality but where negation of equality is not an apartness relaiton
Anonymouse
Countable really means “countably indexed” in the Bauer and Swan paper, since they defined it as having a surjection rather than a bijection with a decidable subset of the natural numbers and countably indexed sets do not in general have decidable equality. In fact, Andrej Bauer and James Hanson constructed a topos in which the Dedekind real numbers do not have decidable equality but are still countably indexed.
Countably indexed sets are not to be confused with the countable sets which are the sets in bijection with a lower decidable subset of the natural numbers, which do come with decidable equality.
Anonymouse
“Working with decidable subsets of sets with decidable equality makes constructive mathematics very much like classical mathematics.”
This statement isn’t true either. Analytic WLPO implies that the Dedekind real numbers and every decidable subset of the Dedekind real numbers have decidable equality, but the constructive strict order meaning “less than” does not satisfy trichotomy, which is a very important theorem in classical mathematics.
“This is why constructivism has few consequences for basic combinatorics and algebra (although it does have important consequences for more advanced topics in those fields).”
There are also potentially other sets with decidable equality and a tight apartness not provably equivalent to the negation of equality. So this sentence isn’t true either - Heyting fields are still important in basic algebra here even for sets with decidable equality. (And if we’re talking about high school algebra - that is real analysis, so the third sentence of the paragraph arrives). One wants to work with decidable subsets of sets with decidable tight apartness to make algebra like that in classical mathematics.
Thus, I will move the “Applications” section from this article to the decidable tight apartness article.
Anonymouse
1 to 10 of 10