nForum - Discussion Feed (Barr's theorem) 2022-08-10T10:54:56-04:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher Thomas Holder comments on "Barr's theorem" (84490) https://nforum.ncatlab.org/discussion/2603/?Focus=84490#Comment_84490 2020-05-09T09:53:23-04:00 2022-08-10T10:54:56-04:00 Thomas Holder https://nforum.ncatlab.org/account/1185/ Expanded a bit on the eliminability of non-constructive proofs with respect to geometric theories and sequents. diff, v9, current

Expanded a bit on the eliminability of non-constructive proofs with respect to geometric theories and sequents.

]]>
zskoda comments on "Barr's theorem" (22179) https://nforum.ncatlab.org/discussion/2603/?Focus=22179#Comment_22179 2011-04-08T15:18:08-04:00 2022-08-10T10:54:56-04:00 zskoda https://nforum.ncatlab.org/account/10/ Just a reminder. There is also another theorem sometimes referred as Barr's theorem, or more precisely, the Barr embedding theorem. Just a reminder. There is also another theorem sometimes referred as Barr's theorem, or more precisely, the Barr embedding theorem. ]]> Urs comments on "Barr's theorem" (22176) https://nforum.ncatlab.org/discussion/2603/?Focus=22176#Comment_22176 2011-04-08T13:33:31-04:00 2022-08-10T10:54:56-04:00 Urs https://nforum.ncatlab.org/account/4/ created stub for Barr’s theorem (If a statement in geometric logic is deducible from a geometric theory using classical logic and the axiom of choice, then it is also deducible from it in ...

created stub for Barr’s theorem (If a statement in geometric logic is deducible from a geometric theory using classical logic and the axiom of choice, then it is also deducible from it in constructive mathematics.)

]]>