4 ms·
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 negat
by hackandthink 4y ago
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 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-and-consistency-strength https://mathoverflow.net/questions/126002/interpretability-a...
- drdeca 4y agoI 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.
- hackandthink 4y agoThanks, I'm not confused anymore.
- librexpr 4y agoYou 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_negative_translation https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...