Timeline for Difference between provability and the existence of a proof?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 24, 2022 at 4:37 | comment | added | user3840170 | On the other hand, I find the statement that ‘it's not correct to say that $\Box X \to X$ is not a theorem’ a bit pedantic. I took the universal quantifier as implied. | |
| Jul 24, 2022 at 4:35 | comment | added | user3840170 | It may be worth remarking that since the logic is not constructive (and therefore it’s wrong to take $X$ as ‘$X$ is provable’), $X \to \Box X$ is not a theorem either. (Counterexample: Gödel sentences, which may be true in the metatheory, but still not provable.) | |
| Jul 24, 2022 at 0:58 | vote | accept | Glubs | ||
| Jul 23, 2022 at 17:10 | comment | added | provocateur | I agree that in constructive logic this would say nothing about there existing a proof. It would say that from a proof that there is a proof of X, one could construct a proof of X. Maybe this would even be a reasonable principle in the constructive context. | |
| Jul 23, 2022 at 13:04 | comment | added | Will Sawin | @Glubs To me it's clearer to think of things in terms of witnesses, where, e.g. a witness of $\forall x\ in X \exists y\in Y$ is a function from $X$ to $Y$. If a proof is a sequence of logical steps then different proofs can produce the same witness. You can also reason by constructive logic about black-box / oracle functions that input $x$ and output $y$ but are not necessarily computable, and in what sense is a black box a proof? | |
| Jul 23, 2022 at 12:52 | comment | added | Glubs | thank you, this is exactly what I was looking for, Although I'm curious as to why it's dubious to consider X as meaning "there is a proof of X" in constructive logics. I thought that was the whole point? | |
| Jul 23, 2022 at 12:43 | history | answered | Will Sawin | CC BY-SA 4.0 |