Re:An intutive counterexample to the axiom of choice
by drdeca on Monday January 23, 2023 @12:51PM
(#34492327)
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.
Re:An intutive counterexample to the axiom of choice
by hackandthink on Monday January 23, 2023 @01:06PM
(#34492535)
Thanks, I'm not confused anymore.
Re:An intutive counterexample to the axiom of choice
by librexpr on Monday January 23, 2023 @01:18PM
(#34492735)
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...
"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...