3 ms·

Can you expand? Many proofs assume the axiom of choice, and I'm missing how this one does.

by mbroshi 10y ago

paulddraper 10y ago
It doesn't. For one thing, the axiom of choice is only necessary in situations with infinite sets, and this has none.
- 4ad 10y ago
  Of course it has infinite sets, N is an infinite set, and the proof makes a statement about another infinite set, the set of primes. This proof is non-constructive because proof-by-contradiction proofs that can't be changed into proof-by-negation proofs are not allowed in constructive math, because there's no law of excluded middle with infinite sets in constructive math, which follows from a lack of a strong axiom of choice. This proof says that the set of prime numbers can't be finite. Only in classical logic you can deduce from this that the set of prime numbers must be infinite. In intuitionistic logic you can't deduce this. This is interesting because most "normal" proofs and results can be written so that they are valid both in classical logic and intuitionistic logic. Only "crazy" results like the Banach–Tarski theorem are different. An yet this is a trivial proof of a trivial result that can't be easily converted to constructivism. That is why it screams of axiom of choice.
  - paulddraper 10y ago
    > Only in classical logic you can deduce from this that the set of prime numbers must be infinite. In intuitionistic logic you can't deduce this. ? I was not aware of any system where proof by contradiction isn't acceptable. The opposite of false is true. But apparently you are right. https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic > intuitionistic logic has no interpretation as a two-valued logic
    - deleted 10y ago
      [deleted]
    - 4ad 10y ago
      One thing to note is that theorem provers/proof assistants like Coq and Agda are based on constructive mathematical foundations (calculus of constructions). Type theory (related to types in programming languages, lambda calculus is one potential example) is also fundamentally constructive.

Can you expand? Many proofs assume the axiom of choice, and I'm missing how this one does.

by mbroshi 10y ago

Can you expand? Many proofs assume the axiom of choice, and I'm missing how this one does.

paulddraper 10y ago

It doesn't. For one thing, the axiom of choice is only necessary in situations with infinite sets, and this has none.

4ad 10y ago
Of course it has infinite sets, N is an infinite set, and the proof makes a statement about another infinite set, the set of primes. This proof is non-constructive because proof-by-contradiction proofs that can't be changed into proof-by-negation proofs are not allowed in constructive math, because there's no law of excluded middle with infinite sets in constructive math, which follows from a lack of a strong axiom of choice. This proof says that the set of prime numbers can't be finite. Only in classical logic you can deduce from this that the set of prime numbers must be infinite. In intuitionistic logic you can't deduce this. This is interesting because most "normal" proofs and results can be written so that they are valid both in classical logic and intuitionistic logic. Only "crazy" results like the Banach–Tarski theorem are different. An yet this is a trivial proof of a trivial result that can't be easily converted to constructivism. That is why it screams of axiom of choice.
- paulddraper 10y ago
  > Only in classical logic you can deduce from this that the set of prime numbers must be infinite. In intuitionistic logic you can't deduce this. ? I was not aware of any system where proof by contradiction isn't acceptable. The opposite of false is true. But apparently you are right. https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic > intuitionistic logic has no interpretation as a two-valued logic
  - deleted 10y ago
    [deleted]
  - 4ad 10y ago
    One thing to note is that theorem provers/proof assistants like Coq and Agda are based on constructive mathematical foundations (calculus of constructions). Type theory (related to types in programming languages, lambda calculus is one potential example) is also fundamentally constructive.