4 ms·

Are there mathematical proofs that are incapable of being expressed in Coq? Isn't there a limit to kind of ideas a computer could verify? Curious about the boun

Are there mathematical proofs that are incapable of being expressed in Coq? Isn't there a limit to kind of ideas a computer could verify? Curious about the boundaries of this language.

curryhoward 9y ago
Practically all of mathematics can be formalized in Coq. One notable exception is the internal consistency of Coq itself (due to Gödel's first incompleteness theorem, I believe). Coq's logic is intuitionistic, which means it's impossible to prove the following: forall P, P or ~P. But this actually makes Coq more powerful than classical logic, not less, because: a) If you want, you can add that proposition (called the law of the excluded middle) as an axiom. Now you have classical logic. b) By not adding that axiom, you can show that certain results do not depend on it. You couldn't do this if it were built-in.
yaseer 9y ago
This question gets at the heart of computation, logic and provability. Coq is based on a logic system called the "Calculus of constructions" https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions. As such it has the same limitations as that logical system. Most notably, Gödel's incompleteness theorems place a limit on what's provable in Coq, or indeed many other systems. There are various kinds of logic systems, each with different kinds of 'power'. Power is a double-edge sword in logic systems, as with power comes the capacity to introduce paradoxes and inconsistencies. As with programming languages, certain logic systems and automated logics are suited for particular cases. For example, there is a system 'MetiTarski' like a Domain Specific Language, designed to prove theorems about real-valued special functions.(https://www.cl.cam.ac.uk/~lp15/papers/Arith/ https://www.cl.cam.ac.uk/~lp15/papers/Arith/).
pbhjpbhj 9y ago
>"Are there mathematical proofs that are incapable of being expressed in Coq?" // Like the proof that there are proofs incapable of being expressed in Coq?!

Are there mathematical proofs that are incapable of being expressed in Coq? Isn't there a limit to kind of ideas a computer could verify? Curious about the boundaries of this language.

curryhoward 9y ago

Practically all of mathematics can be formalized in Coq. One notable exception is the internal consistency of Coq itself (due to Gödel's first incompleteness theorem, I believe). Coq's logic is intuitionistic, which means it's impossible to prove the following: forall P, P or ~P. But this actually makes Coq more powerful than classical logic, not less, because: a) If you want, you can add that proposition (called the law of the excluded middle) as an axiom. Now you have classical logic. b) By not adding that axiom, you can show that certain results do not depend on it. You couldn't do this if it were built-in.

yaseer 9y ago

This question gets at the heart of computation, logic and provability. Coq is based on a logic system called the "Calculus of constructions" https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions. As such it has the same limitations as that logical system. Most notably, Gödel's incompleteness theorems place a limit on what's provable in Coq, or indeed many other systems. There are various kinds of logic systems, each with different kinds of 'power'. Power is a double-edge sword in logic systems, as with power comes the capacity to introduce paradoxes and inconsistencies. As with programming languages, certain logic systems and automated logics are suited for particular cases. For example, there is a system 'MetiTarski' like a Domain Specific Language, designed to prove theorems about real-valued special functions.(https://www.cl.cam.ac.uk/~lp15/papers/Arith/ https://www.cl.cam.ac.uk/~lp15/papers/Arith/).

pbhjpbhj 9y ago

>"Are there mathematical proofs that are incapable of being expressed in Coq?" // Like the proof that there are proofs incapable of being expressed in Coq?!