Item — HN Reader

I am confused:

"From a proof-theoretic perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed" (1)

"Intuitionistic logic can be understood as a weakening of classical logic, meaning that it is more conservative in what it allows a reasoner to infer" (1)

How is this compatible with:

"The systems ZF and IZF (ZF but without LEM) are equiconsistent." ?

(1) https://en.wikipedia.org/wiki/Intuitionistic_logic

Seems to be quite subtle (proof theoretic strength and consistency strength)

(2) https://mathoverflow.net/questions/126002/interpretability-a...

2 comments

You might want to check out the Gödel–Gentzen negative translation[0], which is an interpretation of classical logic in intuitionistic logic, which can be (somewhat inaccurately) summarized as "if P is provable in classical logic, then not not P is provable in intuitionistic logic".

[0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...

I think “equiconsistent” just means that (one can prove that) if one is consistent, then the other is also consistent.

Doesn’t mean the collections of things they can prove can’t differ.

For a weak example, aiui, a formal system is equiconsistent with any conservative extension of it, but the conservative extension can (in the cases one would usually speak of) prove some statements that aren’t in the language of the original system.

Thanks, I'm not confused anymore.