2026-09-22 16:43 UTC
@mei@donotsta.re @zwarich@hachyderm.io well, this tells you that you can replace the assumption of LEM with one of ¬¬LEM (as done in §8), but you can't eliminate it completely a priori. note that ¬¬LEM is not a constructive tautology, only ¬¬(A ∨ ¬A) for a fixed A is
Replies (1)
-
@juli@mathstodon.xyz 2026-09-22 16:55
@ncf@types.pl @mei@donotsta.re @zwarich@hachyderm.io This is why theories like synthetic differential geometry can prove ¬LEM without being paraconsistent, as even though you can prove ¬LEM, you cannot actually construct a closed type A such that ¬(A ∨ ¬A)