When you mentioned "recursive" I was reminded of the time when I learnt about the nth Fibonacci number and having my mind blown that it could even be constructed in that way.
I appreciate you taking the time to explain further your idea of "recursive construction" which is new to me. But I am not sold. Here is why: Firstly, the efficiency of construction is not relevant. Secondly, you mentioned Euclid's proof of the infinitude of prime numbers. His proof provides a simple algorithm to generate a sequence of prime numbers. His proof is constructive in essence, although the proof is typically rephrased as proof-by-contradiction. Thirdly, in your proof for tiling a square of order 2^n with L-trominoes and one monomino. You phrase it as non-constructive but the proof provides a simple algorithm for generating a sequence of tilings starting with the 2x2 case and generating an obvious tiling for the square of order 2^n based on the tiling of the order 2^(n-1) square. So it is essentially constructive even though you chose to turn it into a non-constructive (recursively constructive?) proof.
Although there are many branches and interpretations of intuitionistic logic (constructive logic), they all mainly fall into the category of rejecting the law of excluded middle and double negation elimination as a rules of deduction. Thus, instead of Peano Arithmetic, we have Heyting Arithmetic with the same axioms, just with intuitionistic logic instead of classical. However, in PA and HA, we have the axiom schema of induction. Thus, if we follow the trend of logicians, we must conclude that proofs using induction are constructive and thus the proof you have shown above is also constructive.
Just google "constructive proof": "A constructive proof is a proof that directly provides a specific example, or which gives an algorithm for producing an example." You're confusing "proof by exhibition" (show that something exists by explicitly showing an example of it) and "constructive proof" (give a recipe to find an example). Note that the former is a particular case of the latter. And yes, there exists algorithms to find the nth prime number, they're just slow if n is large (actually not even that slow: for most values of n you can solve it in like n^2*log(n) steps). The fact the construction recipe is complicated does mean it does not exist!
@@Yozoru "constructive" does not have a precise definition or a definition that is accepted by all, unless you start going deep into logic. As I said, I make a distinction between constructive and recursively constructive. Functions and recursive functions are two different things, and in logic one can show that recursive functions cannot replace functions, since they are a weaker concept.
It's fine if you want to distinguish "recursively-constructive" from other kinds of constructive proofs in terms of practicality, I don't disagree with you there that recursion may be impractical. But I strongly disagree with your statement that if we call these proofs constructive then every proof is constructive. Non-constructive proofs are ones where basically there's a fork in the road; an "or"/existence statement and you don't know which is the right one, all you know is that one works. Like if a proof hinges on the Axiom of Choice, that would be a non-constructive proof, because you simply know that "out of this function or this function or this function or..." one of them works, and you have no way of knowing, practical or not. The prototypical example of a non-constructive proof is the proof that "an irrational to an irrational can be rational", which you can find on Wikipedia. You know sqrt(2)^sqrt(2) is either rational "OR" irrational, but you have no way of telling, but it doesn't matter, since if either is true, the ultimate statement is true. We didn't conclusively construct an irrational number for the base. That's what (non-)constructivity is about. I think it's better that you discuss this with your colleagues in real life so you can get a clearer idea of what it means, rather than faceless comments online, because things might get needlessly heated and stressful here.
The prime analogy is really weird. First of all what does "proof of the prime numbers" mean? You can't prove a definition. You can prove the existence of a prime number, but proving for instance that 2 is prime non constructively seems somewhat difficult to me. You can also prove the infinitude of prime numbers, but that is not what you do. What it means for a proof to be constructive is that it does not rely on the law of excluded middle or other similar statements like choice (see Diaconescu's theorem) or reductio ad absurdum. Edit: I think it's also useful to mention that induction is constructively valid.
The argument about arbitrary proofs about things that can be checked in finitely many steps is incorrect because the checking part has nothing to do with the original proof. You have to integrate the finitely many steps into the proof itself, such as in this recursive construction. Ultimately it's just a matter of using excluded middle or not. But it is possibly an interesting distinction to make, among constructive proofs, which are recursive versus "direct". Though you could probably just convert any recursive constructive proof into an equivalent "for loop" or iterative version, I don't know if you wouldn't call that "direct".
When you mentioned "recursive" I was reminded of the time when I learnt about the nth Fibonacci number and having my mind blown that it could even be constructed in that way.
I appreciate you taking the time to explain further your idea of "recursive construction" which is new to me. But I am not sold. Here is why: Firstly, the efficiency of construction is not relevant. Secondly, you mentioned Euclid's proof of the infinitude of prime numbers. His proof provides a simple algorithm to generate a sequence of prime numbers. His proof is constructive in essence, although the proof is typically rephrased as proof-by-contradiction. Thirdly, in your proof for tiling a square of order 2^n with L-trominoes and one monomino. You phrase it as non-constructive but the proof provides a simple algorithm for generating a sequence of tilings starting with the 2x2 case and generating an obvious tiling for the square of order 2^n based on the tiling of the order 2^(n-1) square. So it is essentially constructive even though you chose to turn it into a non-constructive (recursively constructive?) proof.
Although there are many branches and interpretations of intuitionistic logic (constructive logic), they all mainly fall into the category of rejecting the law of excluded middle and double negation elimination as a rules of deduction. Thus, instead of Peano Arithmetic, we have Heyting Arithmetic with the same axioms, just with intuitionistic logic instead of classical. However, in PA and HA, we have the axiom schema of induction. Thus, if we follow the trend of logicians, we must conclude that proofs using induction are constructive and thus the proof you have shown above is also constructive.
@@nicolascoballe7550 that's all fine but that's not how many of us use the term constructive
Just google "constructive proof":
"A constructive proof is a proof that directly provides a specific example, or which gives an algorithm for producing an example."
You're confusing "proof by exhibition" (show that something exists by explicitly showing an example of it) and "constructive proof" (give a recipe to find an example). Note that the former is a particular case of the latter.
And yes, there exists algorithms to find the nth prime number, they're just slow if n is large (actually not even that slow: for most values of n you can solve it in like n^2*log(n) steps). The fact the construction recipe is complicated does mean it does not exist!
@@Yozoru "constructive" does not have a precise definition or a definition that is accepted by all, unless you start going deep into logic. As I said, I make a distinction between constructive and recursively constructive. Functions and recursive functions are two different things, and in logic one can show that recursive functions cannot replace functions, since they are a weaker concept.
Interesting nuance!
It's fine if you want to distinguish "recursively-constructive" from other kinds of constructive proofs in terms of practicality, I don't disagree with you there that recursion may be impractical.
But I strongly disagree with your statement that if we call these proofs constructive then every proof is constructive.
Non-constructive proofs are ones where basically there's a fork in the road; an "or"/existence statement and you don't know which is the right one, all you know is that one works.
Like if a proof hinges on the Axiom of Choice, that would be a non-constructive proof, because you simply know that "out of this function or this function or this function or..." one of them works, and you have no way of knowing, practical or not.
The prototypical example of a non-constructive proof is the proof that "an irrational to an irrational can be rational", which you can find on Wikipedia. You know sqrt(2)^sqrt(2) is either rational "OR" irrational, but you have no way of telling, but it doesn't matter, since if either is true, the ultimate statement is true. We didn't conclusively construct an irrational number for the base.
That's what (non-)constructivity is about.
I think it's better that you discuss this with your colleagues in real life so you can get a clearer idea of what it means, rather than faceless comments online, because things might get needlessly heated and stressful here.
The prime analogy is really weird. First of all what does "proof of the prime numbers" mean? You can't prove a definition. You can prove the existence of a prime number, but proving for instance that 2 is prime non constructively seems somewhat difficult to me. You can also prove the infinitude of prime numbers, but that is not what you do.
What it means for a proof to be constructive is that it does not rely on the law of excluded middle or other similar statements like choice (see Diaconescu's theorem) or reductio ad absurdum.
Edit: I think it's also useful to mention that induction is constructively valid.
The argument about arbitrary proofs about things that can be checked in finitely many steps is incorrect because the checking part has nothing to do with the original proof. You have to integrate the finitely many steps into the proof itself, such as in this recursive construction. Ultimately it's just a matter of using excluded middle or not. But it is possibly an interesting distinction to make, among constructive proofs, which are recursive versus "direct". Though you could probably just convert any recursive constructive proof into an equivalent "for loop" or iterative version, I don't know if you wouldn't call that "direct".
To put it another way, you're conflating "constructive" as an adjective that describes proofs versus properties that have constructive proofs.