Constructive proof construct(indicates) object that satisfies given predicate. Question is whether one can give constructive proof of non-existence of an object with given property e.g. that every subset $S$ of natural numbers has smallest number -- as far as I understand such proof must indicates that there is no element $m' < \min(S)$.

  • $\begingroup$ Maybe you could construct every model of the theory and show that none of the objects in those models satisfies the predicate. $\endgroup$ – Jonny Sep 16 '14 at 22:22
  • $\begingroup$ What if there are infinitely many models. $\endgroup$ – Trismegistos Sep 16 '14 at 22:24
  • $\begingroup$ Then the object you construct that contains all models has an infinite cardinality. $\endgroup$ – Jonny Sep 16 '14 at 22:25
  • $\begingroup$ What do you mean by cardinality of the object? $\endgroup$ – Trismegistos Sep 16 '14 at 22:35
  • $\begingroup$ Cardinality roughly = "how many things are in it". $\endgroup$ – ConMan Sep 16 '14 at 23:24

This is a commonly misunderstood aspect of constructive mathematics. The constructive method to prove "there does not exist an object with property $P$" is to assume there is an object with property $P$ and derive a contradiction.

For example, this is a constructive proof:

There is no smallest integer. Proof: Assume there is a smallest integer, $n$. Then $n-1$ is a smaller integer, which is a contradiction. Therefore there is no smallest integer.

This is because, in the constructive reading, the actual meaning of "not X" is "X implies a contradiction" -- "not X" is really an implicational statement. One thus proves a statement of the form "not X" in the same way that one proves any other implication.

  • $\begingroup$ Thanks. I think meaning of negation in classical logic is the same since "not X" is equivalent to "X implies contradiction". $\endgroup$ – Trismegistos Sep 17 '14 at 8:59
  • $\begingroup$ The same method works in classical logic. The main difference is that the fundamental meaning of "not X" in classical logic is "X is false", while in constructive logic it's better not to think about "true" or "false". Instead, proving X means having a constructive demonstration of X, and proving "not X" means having a constructive demonstration that X cannot occur (because it implies something else that we already know cannot occur) $\endgroup$ – Carl Mummert Sep 17 '14 at 10:30

When I want prove the existence of a thing, the simplest method might be to simply produce that thing. Here it is, therefore it exists. If I wanted to prove the existence of unicorns, the most straight forward way would be to produce a unicorn.

When I want to prove the non-existence of an object that satisfies a predicate, I am equivalently saying that all things do not satisfy that predicate. So if I wanted to disprove the existence of unicorns, it would suffice to show that all things are not unicorns.

A "constructive" proof denying the existence of unicorns might entail constructing the entire universe, and demonstrating that at no time was a unicorn constructed. This might be a bit of a stretch of your definition.

Now, it may be that somehow it was proven that if Bigfoot exists, then unicorns do not exist. Then, technically, a constructive proof about the existence of Bigfoot is also a proof of the non-existence of unicorns.

  • $\begingroup$ You said "When I want to prove the non-existence of an object that satisfies a predicate, I am equivalently saying that all things do not satisfy that predicate" But in constructive logic law of double negation does not hold so I am not sure whether this is correct way. $\endgroup$ – Trismegistos Sep 20 '14 at 10:49
  • $\begingroup$ My statement can be represented by the equivalence: $\neg \exists x P(x) \equiv \forall x \neg P(x)$, which is not a "double negative". $\endgroup$ – Jonny Sep 22 '14 at 17:52

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.