Post by @mei@donotsta.re

2026-09-22 16:35 UTC

@zwarich@hachyderm.io hm, it should be possible to use the double-negation/continuation monad to eliminate the use of LEM entirely, right? after all, Con(ZF) is of the form "there does not exist a derivation of ZF |- False", so it's stable under double-negation, no?

Replies (3)

@zwarich@hachyderm.io 2026-09-22 16:42

@mei@donotsta.re He discusses this in detail in section 8 of the paper (and it's included in a branch of https://github.com/digama0/ConZF), but accessibility is not stable, and he quotes me as showing that the natural accessibility hypothesis for stable membership implies the double negation of Markov's Principle (and the accessibility hypothesis itself can be viewed as a transfinite form of Markov's Principle).

Open ##5431307
@ncf@types.pl 2026-09-22 16:43

@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

Open ##5431309
@typeintype@types.pl 2026-09-22 22:11

@mei@donotsta.re @zwarich@hachyderm.io A crucial ingredient of this proof is large elimination of accessibility (in fact, we do know that CIC is weaker than ZFC without large elim of accessibility). Unfortunately, this ingredient does not play nicely with the standard double-negation translation, because we do not have a large eliminator for ¬¬Acc.

Open ##5431311