Timeline for Barr's theorem and constructivity?
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 15, 2013 at 22:55 | comment | added | Zhen Lin | By the completeness theorem, anything that can be proved with Barr's theorem can be proved without it. There's also the problem that elementary toposes simply do not interpret geometric logic in full – only the coherent fragment. | |
| Sep 15, 2013 at 19:42 | comment | added | Simon Henry | Your example is interesting, but I am interested in something which is specifically a consequence of Barr covering theorem. In this case, this formula is a consequence of the existence of a geometric morphism to set. | |
| Sep 15, 2013 at 16:18 | history | answered | Zhen Lin | CC BY-SA 3.0 |