4 ms·
> "Not proven" isn't the same as implies bottom/Falsum? The article states: ¬A is A → ⊥. But how would you logically express "A is neither proven nor disprove
by tunesmith 5y ago
> "Not proven" isn't the same as implies bottom/Falsum?
The article states: ¬A is A → ⊥.
But how would you logically express "A is neither proven nor disproven"?
It seems to me that if "A" is proven, and "~A" is disproven, then maybe "~~A" is neither proven nor disproven. Is that right? Since intuitionist logic doesn't have the double negation elimination axiom?
- drdeca 5y ago> The article states: ¬A is A → ⊥. Indeed, that is what ¬A means. "¬A" does not mean "not proven". It means that A implies a contradiction. I.e. It means not A. To have a proof of ¬A is to have a disproof of A. "A is not proven" is not a statement in the language. You can't express it in the language. (if you want to add on some provability logic on top of intuitionistic logic, you can do that, but the basic language of intuitionistic logic does not have any way of expressing "it hasn't been proven that A".) The "either it has been proven, or it hasn't been proven" isn't a statement made in the language, but a statement about, how to reason using the language. "~~A" does not mean "neither proven nor disproven", it means -- -- well, it means what it says. It means not(not(A)) . If you have a proof of A, you can use that to produce a proof of ~~A , but not the other way around. A proof of ~~A is, a disproof of ~A, essentially saying "if it could be shown that A implied a contradiction, that implication itself would imply a contradiction".
- tunesmith 5y agoThanks, that makes sense to me.