Timeline for Coq: can `tauto` be used to prove classical tautologies?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 24, 2022 at 17:04 | comment | added | Malcolm Sharpe | Thanks, that's very interesting (and to me unintuitive)! | |
| Aug 24, 2022 at 9:30 | comment | added | Meven Lennon-Bertrand♦ | The answer is yes, in the setting of propositional logic. This is usually called Glivenko’s theorem, and is one of many double-negation translations that map classically provable facts to intuitionistically provable ones using double negation at well-chosen places. | |
| Aug 24, 2022 at 4:50 | vote | accept | Malcolm Sharpe | ||
| Aug 24, 2022 at 4:50 | comment | added | Malcolm Sharpe | Thanks for the link, but I think I was unclear with my question: although freely using NNPP gets you the full power of classical logic (as the link explains), the behavior you describe of classical tauto (if I understand correctly) is to use NNPP only once and only on the initial goal. It's not clear to me whether this very limited use of NNPP gives you as much power as using it freely. (At this point though I'm just curious.) | |
| Aug 23, 2022 at 8:26 | comment | added | corwin.amber | @MalcolmSharpe yes, see this proof, which uses only intuitionistic rules. | |
| Aug 22, 2022 at 9:54 | comment | added | Meven Lennon-Bertrand♦ | If the goal is a tautology of propositional logic, yes. The issue with your setting is that this is not a valid strategy any more once your goal falls out of the propositional fragment, which is the case here due to the introduction, hence the failure. | |
| Aug 22, 2022 at 5:35 | comment | added | Malcolm Sharpe |
Is applying NNPP to the goal enough to make every classical tautology provable using only intuitionistic logic?
|
|
| S Aug 20, 2022 at 16:13 | review | First answers | |||
| Aug 20, 2022 at 21:49 | |||||
| S Aug 20, 2022 at 16:13 | history | answered | corwin.amber | CC BY-SA 4.0 |