4 ms·
Not necessarily. It's very possible for one system to embed inside the other. In this case you can often talk about exactly the same axiom/theorem/whatever with
by tel 11y ago
Not necessarily. It's very possible for one system to embed inside the other. In this case you can often talk about exactly the same axiom/theorem/whatever within different inferential systems.
An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic. That said, we can use flattening to embed classical logic inside of intuitionistic logic and then recover a whole family of propositions of which AC is one and also see why it has a difficult time holding in IPL.
- catnaroek 11y ago> An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic. Naïvely encoded in Martin-Löf type theory, that is.
- plutooo 11y agoStill, "axiom of choice is a theorem in intuitionistic logic" is absolutely true whether or not you accept intuitionistic logic.
- pfortuny 11y agoBut thas is not Mathematics, they call it "metamathematics" for something.