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