5 ms·
But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?
by creata 6y ago
But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?
- auggierose 6y agoI don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.
- deleted 6y ago[deleted]
- auggierose 6y agoHere is an example: after inputing positive integers a, b and c, output all natural numbers n for which a^n + b^n = c^n. My algorithm: If a + b == c then output 1. If a^2 + b^2 == c^2 then output 2. Stop. This algorithm is correct, because Fermat's last theorem holds. Now, try to come up with a simpler algorithm than that, and one that in addition has a constructive proof.
- rssoconnor 6y agoFermat's last theorem holds constructively. This is because we can take the entire proof an rewrite it using the "classical fragment" of constructive logic[1]. I don't know if the proof of FLT (appears) to use the axiom of choice or not, but if it does we use Shoenfield's absoluteness theorem to remove any uses of the axiom of choice from the proof. And we are done, because the statement of the theorem in the "classical fragment" of constructive logic is identical to the constructive statement as it does not involve any existentials or disjunctions. However if the theorem did involve a limited use of these connectives, we could use Goedel's Dialectica interpretation[3] to turn them in to their constructive counterparts, as long as the theorem is Pi_2 or lower, which is going to be the case for the vast majority of theorems about software. [1] https://news.ycombinator.com/item?id=26217587 https://news.ycombinator.com/item?id=26217587 [2] https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_absoluteness_theorem https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_ab... [3] https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf
- auggierose 6y agoHi Russell, thank you for clarifying this! So what you are saying is, if the algorithm and its correctness theorem have a certain form (which is usually the case), we can rewrite any non-constructive proof of it in a constructive way? That is very cool! So, even less reason to demand a constructive proof, a non-constructive one is then often good enough even for hard-core constructivists. Do you know if this has been implemented in any actual (interactive) theorem proving system, for example Lean? It sounds like a great feature to me to allow non-constructive proofs in certain situations, but to have the theorem hold even in a constructive setting.
- rssoconnor 6y agoYes, I realize this arguments cuts both ways. One way is that you can write all these theorems in constructive logic, so there is no need for classical axioms. And the other way, is that users should freely use classical axioms because they can be mechanically removed. Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through by hand to remove uses of classical axioms in Coq proofs of theorems than ought not to be using them. Usually the uses are pretty superficial.
- vcdimension 6y agoHow difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.
- auggierose 6y agoIsabelle also has code generation facilities and very good tooling, and uses classical logic.
- 6y ago