4 ms·

I have to strongly disagree with your first paragraph. Proofs by humans are finite objects, even if they speak about properties of infinite sets. This differenc

by sold 14y ago

I have to strongly disagree with your first paragraph. Proofs by humans are finite objects, even if they speak about properties of infinite sets. This difference does not make proofs for computers more difficult than for humans. You can encode cardinality theorems easily in interactive theorem provers. Formally, a proof is a sequence of assertions, where each one is an axiom or follows from previous ones. Humans are better at proofs because they have good and well-developed intuition; it's bit like coding in assembly vs coding in a high level language. The fact that you deal with infinite objects is not relevant.

dalke 14y ago
I was trying to come up with a example where a theorem prover would have to be extended or rewritten in order to handle new types of mathematics. My imaginary scenario is a theorem validator built by mathematicians from pre-Cantor days, where I conjecture that it would be hard to encode transfinite proofs. As I know nothing about how theorem provers work, this is purely conjectural. In more concrete terms .. and I am so far outside my knowledge that I barely know what I am saying ... I read in the Coq FAQ that "The axiom of unique choice together with classical logic (e.g. excluded-middle) are inconsistent in the variant of the Calculus of Inductive Constructions where Set is impredicative. As a consequence, the functional form of the axiom of choice and excluded-middle, or any form of the axiom of choice together with predicate extensionality are inconsistent in the Set-impredicative version of the Calculus of Inductive Constructions." In other words, proofs involving "axiom of unique choice together with classical logic" cannot be expressed in at least Coq. While it might be possible to use a machine to check tools which assume the axiom of unique choice, it would no doubt take a lot of work if one needs to build such a system from scratch. And that is the scenario - where it's much more difficult to develop a mechanical tool than to come up with a proof that enough for humans - that I am contemplating.
- sold 14y ago
  What do you mean by "transfinite proofs"? Let's look at Cantor's proof. It is: For every set A and function f : A -> P(A) there exists y in P(A) such that for all x, f(x) /= y. Proof: Define y = {a: a is not in f(a)}. If f(x) = y, then f(x) = {a: a is not in f(a)}, but this implies x is in f(x) <=> x is not in f(x), contradiction. It does not mention infinity anywhere! It only says that there cannot be a surjection between one set and the other. We could call this situation "transfinite" but this is only a name; under the hood, this is a normal proof of properties of functions, using very natural reasoning rules. That's why I disagreed - there's nothing special in Cantor's proof from a formal viewpoint, possible concerns are of psychological/historical nature, which are not relevant to a machine. It is true that changing foundations might require rewriting the prover. However, humans also need time to adjust to a new formal system. For example, it takes a lot of effort to get a good grasp of intuitionistic logic. This might be a concern, but ZFC is a very well-grounded common framework for mathematicians, and this is extremely unlikely to change. Perhaps calculus of constructions, as a version of lambda calculus, is closer to computation, and this is why it was chosen in Coq. I'm not sure. Mizar (another theorem-proving environment) is based on an extension of ZFC. [ZFC is untyped - everything is a set, while CoC has a rich type system.] Small nitpick: It's not like proofs involving unique choice + excluded middle cannot be expressed in Coq; they can, but as the system is inconsistent, they have no value, as everything is provable.

by sold 14y ago

dalke 14y ago

I was trying to come up with a example where a theorem prover would have to be extended or rewritten in order to handle new types of mathematics. My imaginary scenario is a theorem validator built by mathematicians from pre-Cantor days, where I conjecture that it would be hard to encode transfinite proofs. As I know nothing about how theorem provers work, this is purely conjectural. In more concrete terms .. and I am so far outside my knowledge that I barely know what I am saying ... I read in the Coq FAQ that "The axiom of unique choice together with classical logic (e.g. excluded-middle) are inconsistent in the variant of the Calculus of Inductive Constructions where Set is impredicative. As a consequence, the functional form of the axiom of choice and excluded-middle, or any form of the axiom of choice together with predicate extensionality are inconsistent in the Set-impredicative version of the Calculus of Inductive Constructions." In other words, proofs involving "axiom of unique choice together with classical logic" cannot be expressed in at least Coq. While it might be possible to use a machine to check tools which assume the axiom of unique choice, it would no doubt take a lot of work if one needs to build such a system from scratch. And that is the scenario - where it's much more difficult to develop a mechanical tool than to come up with a proof that enough for humans - that I am contemplating.

sold 14y ago
What do you mean by "transfinite proofs"? Let's look at Cantor's proof. It is: For every set A and function f : A -> P(A) there exists y in P(A) such that for all x, f(x) /= y. Proof: Define y = {a: a is not in f(a)}. If f(x) = y, then f(x) = {a: a is not in f(a)}, but this implies x is in f(x) <=> x is not in f(x), contradiction. It does not mention infinity anywhere! It only says that there cannot be a surjection between one set and the other. We could call this situation "transfinite" but this is only a name; under the hood, this is a normal proof of properties of functions, using very natural reasoning rules. That's why I disagreed - there's nothing special in Cantor's proof from a formal viewpoint, possible concerns are of psychological/historical nature, which are not relevant to a machine. It is true that changing foundations might require rewriting the prover. However, humans also need time to adjust to a new formal system. For example, it takes a lot of effort to get a good grasp of intuitionistic logic. This might be a concern, but ZFC is a very well-grounded common framework for mathematicians, and this is extremely unlikely to change. Perhaps calculus of constructions, as a version of lambda calculus, is closer to computation, and this is why it was chosen in Coq. I'm not sure. Mizar (another theorem-proving environment) is based on an extension of ZFC. [ZFC is untyped - everything is a set, while CoC has a rich type system.] Small nitpick: It's not like proofs involving unique choice + excluded middle cannot be expressed in Coq; they can, but as the system is inconsistent, they have no value, as everything is provable.