13
$\begingroup$

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:

  1. Has anyone looked at logics in which only combinatorist-constructive methods are ok?
  2. 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.)
Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ 2. is the main problem here, I believe. Is "brute force minus 10 cases which can be trivially excluded in advance" better than brute force? I think the thing that comes next to your "combinatorist-constructive" is P (as opposed to NP). $\endgroup$
    – darij grinberg
    Commented Jun 5, 2010 at 11:19

7 Answers 7

Reset to default
9
$\begingroup$

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.

Improve this answer
$\endgroup$
6
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Banning combinatorially non-constructive proofs does not require denying the existence of very large numbers. It requires only weakening the induction schema of first-order Peano Arithmetic so that you can no longer prove that overly fast-growing functions are everywhere defined. See the book by Cook and Nguyen that I mention in my answer. $\endgroup$
    – Timothy Chow
    Commented Jun 5, 2010 at 22:47
  • 1
    $\begingroup$ Thanks for the link, and yes, maybe it isn't really necessary to mention ultrafinitism, which is not a well-defined mathematical concept. This is an effect of a weakened induction schema, though, isn't it? I.e., it prevents you from giving feasible proofs of the existence of very large numbers? $\endgroup$
    – Noam Zeilberger
    Commented Jun 6, 2010 at 13:02
  • $\begingroup$ Well, I guess you could phrase it that way, but I prefer to phrase it this way: You write down a definition of something that is supposed to be a function on all the natural numbers, but you can't prove that it is defined everywhere. The point is that there's no specific large number that you can't prove exists. The limitation is on what you can prove about functions that grow too fast. It's entirely analogous to the fact that Goodstein's theorem is unprovable in PA because the function in question grows too fast. I wouldn't call PA is "ultrafinitist" for this reason. $\endgroup$
    – Timothy Chow
    Commented Jun 6, 2010 at 18:13
5
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • 3
    $\begingroup$ The "irrational to irrational = rational" example is bogus, see math.andrej.com/2009/12/28/… $\endgroup$
    – Andrej Bauer
    Commented Jun 5, 2010 at 17:47
  • 1
    $\begingroup$ Interesting post, but I do not think the example, as an example of non effective or non explicit proof, is bogus. It is true that the term "non effective proof" is not always precise or formal. $\endgroup$
    – Gil Kalai
    Commented Jun 5, 2010 at 18:21
  • 1
    $\begingroup$ Neel's point is that "ineffective proof" in the strong sense of providing no algorithm at all is nicely captured by intuitionistic logic. E.g., the finiteness theorem of Faltings gives no algorithm for finding the solutions, and an intuitionist expresses this by saying the solution set is "not infinite" (as opposed to "finite"). The question is, is there a similar way to capture formally the fact that (for example) the probabilistic existence proof of Ramsey graphs yields no polytime construction? The answer is yes: the proof is not formalizable in a certain system of bounded arithmetic. $\endgroup$
    – Timothy Chow
    Commented Jun 5, 2010 at 23:01
  • $\begingroup$ Wow, that Goldwasser/Kilian algorithm is really amazing! It "almost always" quickly terminates, which is neat. Are there any fast "almost always" semi-algorithms? (Ie, you're allowed to not terminate at all on "not many" inputs.) Most semi-algorithms I know come from things like the completeness of first-order logic, so their worst case performance is unspeakable. Are there any algorithms which you know will finish quickly if they finish at all? (The reason I ask is that it would refute the idea that combinatorially constructive methods subset the intuitionistic methods.) $\endgroup$
    – Neel Krishnaswami
    Commented Jun 6, 2010 at 15:33
  • $\begingroup$ Sometimes a constructive move simply involves more carefully stating what it is that a proof shows. In Hex there can be no draw and it is not the case that the second player has a winning strategy. Probably every digit appears equally often in Pi. Classically, at least one appears infinitely often (actually at least two). Constructively, they don't all appear finitely often. Sometime following that discipline actually guides on to stronger proofs (but that is a topic for another question). $\endgroup$
    – Aaron Meyerowitz
    Commented Aug 25, 2010 at 5:34
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ There are a plethora of algorithms which are worst-case doubly-exponential which, in practice, often terminate quickly (Groebner bases being the obvious example). Algorithms in $n^17$ for even moderate n will effectively never terminate. So, in practice, the useful classes are much more subtle than those which theoreticians have decided to study, IMHO. Similarly all sorts of undecidable problems have (large!) decidable fragments [like Halting, which you know better than I do]. $\endgroup$
    – Jacques Carette
    Commented Jun 5, 2010 at 17:15
  • $\begingroup$ Those subtle distinctions you mention, such as the difference between average case complexity and worst-case complexity, are not neglected and are also well studied. For example, see en.wikipedia.org/wiki/Generic-case_complexity. $\endgroup$
    – Joel David Hamkins
    Commented Jun 5, 2010 at 17:40
  • 1
    $\begingroup$ For example, randomized algorithms (see en.wikipedia.org/wiki/Randomized_algorithm) were once regarded as non-standard, but are now completely classical methods, in comparison with more esoteric current considerations, such as quantum computation. $\endgroup$
    – Joel David Hamkins
    Commented Jun 5, 2010 at 18:36
1
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ My aim with ASD is to develop a language that looks as much as possible like "ordinary mathematics" but which has a computable foundation instead of set theory. If only people had known the formal definition of computability, I believe that that was the strength of the traditional foundations before set theory came along, and that natural mathematics is computable, Also, <a href="paultaylor.eu/ASD/lamcra">A lambda calculus for real analysis<a> might be a better place to start with ASD. $\endgroup$
    – Paul Taylor
    Commented Jun 10, 2010 at 13:48
  • $\begingroup$ The question, however, is I think about the difference between computability and feasibility (say polynomial time). Whilst there are resource logics that can talk about this, they would look very much more different from ordinary mathematics than ASD does. I think this needs to be sorted out at the computable level first, leaving the feasible version to another generation. $\endgroup$
    – Paul Taylor
    Commented Jun 10, 2010 at 13:49
1
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .