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

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"?

• Why did you ask four times the same question ? Commented Oct 15, 2020 at 14:57
• Sorry for this. My phone was crashing and it somehow did this. (Though I think it's a bit uncharitable to downvote it for this reason. Obviously it was a mistake). Unfortunately SE doesnt allow me to delete it on my phone so I'll have to do it when I'm back at my pc. Sorry for that. Commented Oct 15, 2020 at 15:28
• You mean $\sum N_i$ and not $\sum P_i$ I think? Commented Oct 15, 2020 at 15:57
• I've deleted the dupes, so that part of the accident is handled. Commented Oct 15, 2020 at 16:02
• @DanielFischer thank you:). Apologies for the inconvenience. Commented Oct 15, 2020 at 16:03

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

• I think there are probably ways to state a similar proposition that are not constructively provable. However, they involve weaker notions than 'finite' that are classically equivalent to being finite. Some of the assumptions that the original presentation makes might not make sense, though. For instance, I don't think it makes sense to talk about the natural number of elements of a subfinite set satisfying a predicate. For that to be precise, the set would have to actually be finite, I think, and then your explanation of why this is constructive would work. Commented Oct 15, 2020 at 18:00
• Oh also, I think if all the things stated to be finite in the original problem are actually constructively (Bishop) finite, then it would allow us to decide $P_i$, because it assumes there are exact listings of which values of $S$ do (and therefore which don't) satisfy each one. So the assumptions need to be weakened to even consider $P_i$ not being decidable. Commented Oct 15, 2020 at 18:07
• Thank you for the answer. I have thought about this, and I think my current view is: Yes I agree that if we interpret the goal constructively, then the argument becomes so as well. However, I would say that the goal itself is in fact not “strongly constructive” by my definition: You need to use the decidability of “is an element $x\in [n]$ also an element of $S$” to define the summation $|S|$, and hence this is not a “strongly constructive” property. (I.e. $instance(S,n)$ is not strongly constructive for your example, nor for mine). Commented Oct 16, 2020 at 11:53
• If $S$ is finite, this is witnessed by something like $Σ n:ℕ. \Vert S \simeq \mathsf{Fin}(n) \Vert$ (i.e. $S$ is isomorphic to some particular finite set construction, but the specific choice of isomorphism is unimportant). Then $|S|$ is available by projecting out the specified size part of the witness. However, this implies that equality in $S$ is decidable, via borrowing from $\mathsf{Fin}(n)$. Commented Oct 16, 2020 at 13:44