In the context of intuitionistic logic, the property of a theory $T$ holding when for any existentially quantified formulae $\exists x\phi \left(x\right)$ provable in $T$ in which $x$ is the only free variable in $\phi \left(x\right)$, there exists an effective procedure to construct a constant term $t$ such that $\phi \left(t\right)$ is provable from $T$. As $t$ witnesses the truth of $\exists x\phi \left(x\right)$, this is also known as the witness property.