Timeline for Validity of equations in a topos
Current License: CC BY-SA 3.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 29, 2014 at 13:48 | comment | added | Eduardo J. Dubuc | So, for example, if we want to prove that the validity of some equation follows from the validity of other equations in the real interval [0, 1] (equations in any geometric language interpretable in [0, 1]), then we can proceed by cases, for example, (x = 1) or (not x = 1). Even though that [0, 1] is not decidable. So this proof using classical logic which is not valid intuitionistically will in practice be accepted as a proof in the internal language of any topos, since we accept the conclusion as true without requiring any other proof. | |
| Apr 28, 2014 at 0:08 | history | answered | Andreas Blass | CC BY-SA 3.0 |