Deep thought of the Day - Intuitionalist Type Theory
...just as a canonical set is understood together with its canonical elements, a non-canonical set is understood with its computational rules.
Is not A : set in fact a commissive sentence? Not completely: that one re- cognizes something as possible in principle does not mean that one commits oneself to do it ; put differently, to know that A : set is to know that it is, in principle, possible to compute the value of A, not actually to be prepared to do it. - Granstrom, 2011.
Reminds me of the South Park sequence of steps 1. 2. .... 4. Profit! :)
Actually, when we consider, for example, the results of the referendum in Crimea, we can't logically separate them from the "computational" procedure that was used to attain them. If the procedure was invalid, the results were not valid either.
