Replacing logician-constructive with combinatorist-constructive? - MathOverflow

Replacing logician-constructive with combinatorist-constructive?

2010-06-05T10:13:17Z

Logicians interpret the word "constructive" in a very well-defined way: they take it to mean, more or less, "computability". Taking constructivity seriously and working in a world where everything must be constructive, leads to intuitionistic logic, which has been a very productive and fascinating subfield of logic.

On the other hand, combinatorists use "constructive" in a different sense. They use it to mean "better than brute force". For example, Ramsey's theorem is non-constructive from the POV of a combinatorist, since its proof offers no method better than just enumerating the subgraphs until you find a complete monochromatic one. On the other hand, from a logician's POV, it is constructive -- just enumerate the subgraphs until you find a complete monochromatic one! (Or even more simply, the pigeonhole principle has the same flavor.)

So:

Has anyone looked at logics in which only combinatorist-constructive methods are ok?
If not, has anyone done a formal analysis of what "better than brute force" means? (This seems different than the questions typically asked in algorithmics, but I would not be shocked if they've thought about it too.)

Answer by supercooldave for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T11:15:23Z

Addressing question 1: You might want to look at Paul Taylor's Abstract Stone Duality, perhaps starting with Foundations for Computable Topology. He's doing a lot of work which is very constructive in nature, and he seems to get a very long way, essentially recasting a whole load of mathematics and logic from a constructive angle.

Answer by Joel David Hamkins for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T11:46:28Z

I think the entire subject of computational complexity theory, with the concepts of P, NP, PSPACE, EXPTIME and so on, is fundamentally about exploring various precise senses of what "better than brute force" might mean.

For example, combinatorists would regard polytime algorithms as basically constructive, while brute force algorithms are inherently exponential time. The subtle NP class admits a constructive, but nondeterministic flavor, in that solutions can be verified quickly, but are hard to build. There is an entire zoo of complexity classes, whose interrelationships are intensely studied in complexity theory. (See also the petting zoo there, for starters.)

Answer by Noam Zeilberger for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T12:34:32Z

so just to be clear, the reason the finite versions of Ramsey's theorem and the pigeonhole principle are intuitionistic is because you have an explicit bound on the search space. If the search space were a priori unbounded (as in the infinite versions of these theorems), these proofs would be applying Markov's principle. That being the case, in order to ban such "combinatorially non-constructive" proofs I'm pretty sure you have to move to an ultrafinitist logic, i.e., deny the existence of very large numbers. Because whenever we have one, we can iterate on it to perform a constructive search over a very large space.

I think the problem with using the classical complexity classes to approach this is that there is a P-time (indeed constant-time) algorithm for computing the Ramsey number R(6,6), which will not terminate in the lifetime of the universe.

Answer by Gil Kalai for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T13:02:15Z

Although the question of finding explicit constructions was considered in combinatorics very early, theoretical computer science gives a fairly concrete way to say what "constructive" means. Lower bounds for Ramsey numbers is a good example. it was discussed in this MO question. Probabilistic methods shows that there are graphs with $2^{k/2}$ vertices without a complete subgraph or an empty subgraph on k vertices. Explicit constructions are constructions that can be described by a polynomial type (deterministic) algorithm. (But you can demand also a stronger requirement of log-space algorithms.) the best known explicit constructions (that can be described by a log space algorithm) gives such graphs with number of vertices proportional to $2^{k^C}$ vertices for every C>0. In combinatorics explicit constructions are usually related to derandomization. See also this post about derandomization.

I am not sure what are the relation between logician-constructive as described in the question and explicit construction and derandomization in combinatorics. It seems that they are related to the notion of "effective and non effective" proofs where non effective proofs are proofs that gives no algorithm what so ever. A famous non effective proof is the statement (by Nash) that the first player in an n by n HEX game has a winning strategy. (Using stealing strategy argument.) Another example of s similar nature is the argument that there are irrationals a and b so that $a^b$ is rational. (Based on $(\sqrt 2 ^{\sqrt 2})^\sqrt 2=2$.) I think that a famous area where effective proofs are highly desirable is in the context of improvements for Liuville's theorem regarding trancendental numbers. So maybe the distinction between effective and non-effective proofs is closer to the logical issues the question referred to.

Answer by Rob Simmons for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T14:12:20Z

I've always considered the work on logics where normalization characterizes certain complexity classes (espesially Mairson's work on PTIME and linear logic) to fall in this category. I suppose (as Noam's comment points out) that is a complexity-based notion which doesn't seem to capture the notion of "better than brute force" that you're looking for.

Answer by Andrej Bauer for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T17:56:12Z

You are asking about resource-aware logics. You could look at Sam Buss's work and his logics which characterize various complexity classes. There is also a bunch of subsequent work on implicit characterizations of complexity classes. In another line of work you could look at substructural logics, such as linear logic.

I suspect we could characterize "brute force search" in terms of computational complexity. For example, if the state space is of size $N$ and the search takes $O(\log N)$, then presumably it is not brute force. If it is $\omega(N)$ then presumably it is brute force.

Answer by Timothy Chow for Replacing logician-constructive with combinatorist-constructive?

2010-06-05T18:20:45Z

I think the closest thing to what you are looking for are the logical systems studied in Cook and Nguyen's recent book Logical Foundations of Proof Complexity. These are systems in which the provably total functions lie in certain well-defined computational complexity classes. In particular, existence proofs in these systems imply that the object whose existence is asserted can be computed "easily."

This line of research goes back at least to Buss (as mentioned by Andrej Bauer), who defined systems of bounded arithmetic that are closely related to the levels of the polynomial hierarchy (a hierarchy of complexity classes whose lowest levels are $P$ and $NP$). More generally, the field known as "proof complexity" is devoted to studying the relationship between computational complexity classes (particularly circuit complexity classes) and formal systems for arithmetic with suitably weakened induction axioms.

This all assumes that you are satisfied with the idea that "better than brute force" means something like "polytime solvable." There are limitations with the concept of polynomial time solvability, notably its emphasis on asymptotic behavior and its focus on worst-case complexity. (Although average-case complexity has been studied, the natural questions there are very difficult to answer and the theory is much less developed.) Still, a lot of interesting insights have emerged from studying proof complexity and I think it is a very promising avenue for further research.