Strongly constructive proofs: Proofs that don't make use of decidability?

Question

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic:

A typical counting argument might have the following pattern: Suppose we have a finite set $S$ and $n$ properties (subsets) $P_i$ on it. Let $N_i$ be the number of elements of $S$ that satisfy property $P_i$. Let $P=P_1\land ...\land P_n$, and let $N$ be the number that satisfy $P$. Then $N\leq\sum N_i$ by a simple argument. So if $\sum N_i<|S|$ then there is an $s\in S$ with $\neg P(s)$.

Intuitively, this seems like an unconstructive argument: we are not actually constructing an example of an $s$ with the desired property.

However, if all of the properties $P_i$ are decidable (we can define a program that checks for any $s$ if they are satisfied), then the summations are computable and I think then we can actually write a formal proof that doesn't use the law of excluded middle. Hence we have to conclude that the proof is constructive (given those assumptions).

My question is whether we can save the former informal notion that this is not a "constructive proof" (which is clearly not equivalent to the standard definition of constructive proof in intuitionistic logic).

One idea I've seen is that the proof is non-constructive because it is a computationally complex (e.g. NP-hard or EXPTIME). I don't think this is satisfying because it's easy to define algorithms that construct an object in a wildly inefficient manner, but that are still "direct".

One proposal I have is of "strongly constructive":

• A proof is strongly constructive if it doesn't use the decidability of any particular property.

• A proof is weakly constructive if it doesn't use LEM in any way. (But may use the decidability of a specific property for which this has been constructively proven).

I think the counting argument is not strongly constructive because to define the summation I think you need to assume decidability of the propositions.

Is this a known notion? Does it capture the sense in which counting arguments are "non-constructive"?

Answer 1

I disagree with the premise of the question: I don't see a reason to "throw out" this sort of argument. I think the issue it highlights is the need to consider implications in a balanced way, with the hypothesis being construed in the same way as the conclusion and overall statement.

To explain, let me focus on a simpler proposition:

$(*)\quad$ If $S$ is a finite subset of $[n]=\{1,2,...n\}$ and $\vert S\vert<n$ then there is some $k\in [n]$ such that $k\not\in S$.

Considering more properties doesn't seem to add any nonconstructivity, so I'm dropping that aspect for simplicity.

When we think of $(*)$ constructively, what we intuitively want is an algorithm for taking in an instance $(S,n)$ of the problem and outputting a solution $k$. However, there's a "second level constructivity" here: namely, in the notion of an instance of the problem in the first place. Abstracting a bit, $(*)$ has the form:

$$\forall S,n([instance(S,n)]\implies \exists k(solution(S,n,k))).$$ So a constructive proof of $(*)$ should be a construction which, when fed a pair $(S,n)$, provides a construction for transforming any construction witnessing $instance(S,n)$ into a $k$ and a construction witnessing $solution(S,n,k)$.

The key point is that bolded phrase: part of the data we're allowed to use in constructing (and verifying!) our desired $k$ is constructive evidence of the fact that $(S,n)$ is actually an instance of the problem - that is, that $\vert S\vert<n$. And this is basically telling us right at the outset what we're looking for!

My point is that I don't see a way to interpret the goal in a constructive way without also making the proof constructive. I think that issues only arise when we try to "partially constructivize" that goal ... which isn't something which seems natural to me in the first place.