What counts as a witness in constructive mathematics?

133 Views Asked by At

In order for a mathematical object to be accepted by a constructivist, a witness of a such object much be constructed. For example, we may let points be witnesses for natural numbers. For a real number $r$, a Turning machine capable of outputting $r$ to any arbitrary precision is seen as a witness for $r$.

But what counts a witness, and why, seems quite arbitrary to me and sometimes already pre-supposes the existence of the mathematical object we are trying to construct a witness for.

Is there a more precise definition and requirements for a witness, and why or why not something counts as a witness?