Is constructive proof of non-existence possible

Question

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)$.

Answer 1

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.

Answer 2

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.