Constructive logic and witnesses

Under the propositions-as-types interpretation used here, conjunction is represented by a pair, and an implication by a function taking evidence of its hypothesis to evidence of its conclusion. An untruncated disjunction includes a tag indicating the chosen alternative and evidence for that alternative. An untruncated existential includes an object and evidence that it satisfies the predicate. These descriptions concern proof-relevant data; later we will distinguish them from mere propositions and truncated existence.

The introduction and elimination rules must agree. To use a conjunction, project its components; to use a disjunction, handle either possible tag. A function proves an implication only when it works for every admitted input, rather than for a favorable example. The empty type represents falsity, and negation means a function into that empty type. Thus proving a negative statement is itself constructive when the proposed counterexample is transformed into a contradiction.

A proof of P always yields a proof that P cannot be refuted: send any proposed refutation the supplied proof. The reverse conversion is not a rule of intuitionistic logic for arbitrary P. In particular, refuting the claim that no witness exists need not provide a witness. Adding a general conversion from double negation to positive evidence recovers a classical principle, so an argument that uses it should declare the extra assumption.

Even the excluded-middle disjunction has a constructive double negation. Suppose a refutation rejects every proof of either P or its negation. It would reject any proof of P through the left tag, thereby itself providing a negation of P. The right tag containing that negation is then also rejected, giving a contradiction. This argument constructs double-negated excluded middle without deciding P. Keeping the tags and function types visible makes the difference precise.

For a decidable predicate on a finite list, compare each candidate in order and stop at the first success. A successful run returns the candidate, a verification of its predicate, and the failed comparisons for all preceding candidates. If the list is exhausted, it returns a proof that no member of that list works. Every branch is justified by the supplied decision procedure, so this algorithm needs no unrestricted decision principle for arbitrary mathematical propositions.

The finiteness qualification matters. Searching all natural numbers for a decidable property may never terminate when no witness exists. A proof that a bounded search succeeds can supply a termination bound, while a bare promise that the property is not refutable may not do so. Constructive proof design therefore records both the predicate and the information guaranteeing that its search completes. The resulting certificate can be checked independently of the strategy used to discover it.