“Strange” proofs of existence theorems

The name of the pictureThe name of the pictureThe name of the pictureClash Royale CLAN TAG#URR8PPP











up vote
3
down vote

favorite












This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, proofs involving contradiction/contrapositive, and proofs involving the axiom of choice.



I'm convinced that there must be some existence theorem that can be proven without any of these techniques (and I'm fairly confident that I've probably encountered some myself in the past haha), but I can't come up with any examples at the moment. Can anyone else come up with one? I'd also like to stipulate the following conditions:



  1. The proof can't piggyback on another existence theorem whose proof involves one of the above-mentioned devices.

  2. It has to be a theorem of ZF - no exotic and "high power" axioms allowed!

Now for the interesting question: is there any existence theorem (again in ZF) such that every proof of it meets all the criteria above? Has anyone done any work in this direction? If so, what results do we have around this?










share|cite|improve this question

















  • 3




    To make this question precise, you would need to carefully define what you mean by "constructive proof".
    – Alex Kruckman
    15 hours ago






  • 1




    “25 has a square root in integers.” When existence is obvious enough to need no elaborate argument, it’s just not called a theorem...
    – Francois Ziegler
    14 hours ago






  • 2




    @Francois The point is that you exhibit an explicit object (in your example, 5).
    – Andrés E. Caicedo
    14 hours ago






  • 4




    Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction).
    – Qiaochu Yuan
    10 hours ago







  • 2




    @Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.)
    – Andrés E. Caicedo
    4 hours ago














up vote
3
down vote

favorite












This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, proofs involving contradiction/contrapositive, and proofs involving the axiom of choice.



I'm convinced that there must be some existence theorem that can be proven without any of these techniques (and I'm fairly confident that I've probably encountered some myself in the past haha), but I can't come up with any examples at the moment. Can anyone else come up with one? I'd also like to stipulate the following conditions:



  1. The proof can't piggyback on another existence theorem whose proof involves one of the above-mentioned devices.

  2. It has to be a theorem of ZF - no exotic and "high power" axioms allowed!

Now for the interesting question: is there any existence theorem (again in ZF) such that every proof of it meets all the criteria above? Has anyone done any work in this direction? If so, what results do we have around this?










share|cite|improve this question

















  • 3




    To make this question precise, you would need to carefully define what you mean by "constructive proof".
    – Alex Kruckman
    15 hours ago






  • 1




    “25 has a square root in integers.” When existence is obvious enough to need no elaborate argument, it’s just not called a theorem...
    – Francois Ziegler
    14 hours ago






  • 2




    @Francois The point is that you exhibit an explicit object (in your example, 5).
    – Andrés E. Caicedo
    14 hours ago






  • 4




    Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction).
    – Qiaochu Yuan
    10 hours ago







  • 2




    @Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.)
    – Andrés E. Caicedo
    4 hours ago












up vote
3
down vote

favorite









up vote
3
down vote

favorite











This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, proofs involving contradiction/contrapositive, and proofs involving the axiom of choice.



I'm convinced that there must be some existence theorem that can be proven without any of these techniques (and I'm fairly confident that I've probably encountered some myself in the past haha), but I can't come up with any examples at the moment. Can anyone else come up with one? I'd also like to stipulate the following conditions:



  1. The proof can't piggyback on another existence theorem whose proof involves one of the above-mentioned devices.

  2. It has to be a theorem of ZF - no exotic and "high power" axioms allowed!

Now for the interesting question: is there any existence theorem (again in ZF) such that every proof of it meets all the criteria above? Has anyone done any work in this direction? If so, what results do we have around this?










share|cite|improve this question













This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, proofs involving contradiction/contrapositive, and proofs involving the axiom of choice.



I'm convinced that there must be some existence theorem that can be proven without any of these techniques (and I'm fairly confident that I've probably encountered some myself in the past haha), but I can't come up with any examples at the moment. Can anyone else come up with one? I'd also like to stipulate the following conditions:



  1. The proof can't piggyback on another existence theorem whose proof involves one of the above-mentioned devices.

  2. It has to be a theorem of ZF - no exotic and "high power" axioms allowed!

Now for the interesting question: is there any existence theorem (again in ZF) such that every proof of it meets all the criteria above? Has anyone done any work in this direction? If so, what results do we have around this?







proof-theory






share|cite|improve this question













share|cite|improve this question











share|cite|improve this question




share|cite|improve this question










asked 15 hours ago









Joseph G

522




522







  • 3




    To make this question precise, you would need to carefully define what you mean by "constructive proof".
    – Alex Kruckman
    15 hours ago






  • 1




    “25 has a square root in integers.” When existence is obvious enough to need no elaborate argument, it’s just not called a theorem...
    – Francois Ziegler
    14 hours ago






  • 2




    @Francois The point is that you exhibit an explicit object (in your example, 5).
    – Andrés E. Caicedo
    14 hours ago






  • 4




    Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction).
    – Qiaochu Yuan
    10 hours ago







  • 2




    @Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.)
    – Andrés E. Caicedo
    4 hours ago












  • 3




    To make this question precise, you would need to carefully define what you mean by "constructive proof".
    – Alex Kruckman
    15 hours ago






  • 1




    “25 has a square root in integers.” When existence is obvious enough to need no elaborate argument, it’s just not called a theorem...
    – Francois Ziegler
    14 hours ago






  • 2




    @Francois The point is that you exhibit an explicit object (in your example, 5).
    – Andrés E. Caicedo
    14 hours ago






  • 4




    Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction).
    – Qiaochu Yuan
    10 hours ago







  • 2




    @Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.)
    – Andrés E. Caicedo
    4 hours ago







3




3




To make this question precise, you would need to carefully define what you mean by "constructive proof".
– Alex Kruckman
15 hours ago




To make this question precise, you would need to carefully define what you mean by "constructive proof".
– Alex Kruckman
15 hours ago




1




1




“25 has a square root in integers.” When existence is obvious enough to need no elaborate argument, it’s just not called a theorem...
– Francois Ziegler
14 hours ago




“25 has a square root in integers.” When existence is obvious enough to need no elaborate argument, it’s just not called a theorem...
– Francois Ziegler
14 hours ago




2




2




@Francois The point is that you exhibit an explicit object (in your example, 5).
– Andrés E. Caicedo
14 hours ago




@Francois The point is that you exhibit an explicit object (in your example, 5).
– Andrés E. Caicedo
14 hours ago




4




4




Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction).
– Qiaochu Yuan
10 hours ago





Maybe proofs using the probabilistic method might count. They're not constructive and they don't involve the axiom of choice but it's a bit unclear to me how to evaluate whether they use contradiction / contrapositive (these are really not similar at all, by the way; in a proof by contrapositive every statement you write down along the way is still true, unlike in a proof by contradiction).
– Qiaochu Yuan
10 hours ago





2




2




@Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.)
– Andrés E. Caicedo
4 hours ago




@Dirk But typical proofs of uncountability do not seem to be by contradiction: given an enumeration, you explicitly exhibit a real not in the list, for instance. (It seems like splitting hairs in any case.)
– Andrés E. Caicedo
4 hours ago










5 Answers
5






active

oldest

votes

















up vote
12
down vote













There are probabilistic proofs of existence. Do they fall into one of your three categories?



For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost all" proof is easier than constructing an explicit example.



See some nice examples due to Erdōs in the cited Wikipedia page which use only finite probability spaces. If we show that a probability is $ > 0$, then the set is not empty.






share|cite|improve this answer






















  • I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
    – Noam D. Elkies
    16 mins ago

















up vote
3
down vote













I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $mathbbN$. In Peano artithmetic, Goodstein's theorem is unprovable.






share|cite|improve this answer




















  • I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
    – Carl Mummert
    16 mins ago


















up vote
2
down vote













While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.



It is (reasonably) clear what it means that a theorem has a constructive proof.



"All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."



Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.



Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.



Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.






share|cite|improve this answer



























    up vote
    2
    down vote













    There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$. The proof considers two cases: $sqrt2^sqrt2$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.



    You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.



    (By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)



    EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.






    share|cite|improve this answer




















    • Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
      – Sam Hopkins
      1 hour ago










    • I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
      – Carl Mummert
      19 mins ago

















    up vote
    0
    down vote













    I think applications of the Yoneda lemma fit your criteria.



    We often prove the existence of some isomorphism $f:Arightarrow B$ in a category $mathcalC$ by embedding $mathcalC$ in $Sets^mathcalC^OP$ using the Yoneda lemma $y$ and finding an iso $g:y(A)rightarrow y(B)$, then concluding that there exists some unique iso $f:Arightarrow B$ with $y(f)=g$ since $y$ is full and faithful.



    Exhibiting an arrow in $Sets^mathcalC^OP$ is often easier than in $mathcalC$ since $Sets$ is complete and cocomplete and Cartesian closed, which makes $Sets^mathcalC^OP$ complete and cocomplete and Cartesian closed even if $mathcalC$ isn't.



    We can thusly use 'higher order' tools like limits/colimits in $Sets^mathcalC^OP$ which we aren't allowed to use in $mathcalC$ to find arrows, then still infer the existence of an arrow in $mathcalC$ if the resulting arrow in $Sets^mathcalC^OP$ is between two contravariant representable functors.






    share|cite|improve this answer
















    • 1




      I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
      – Todd Trimble♦
      2 mins ago










    Your Answer




    StackExchange.ifUsing("editor", function ()
    return StackExchange.using("mathjaxEditing", function ()
    StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
    StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
    );
    );
    , "mathjax-editing");

    StackExchange.ready(function()
    var channelOptions =
    tags: "".split(" "),
    id: "504"
    ;
    initTagRenderer("".split(" "), "".split(" "), channelOptions);

    StackExchange.using("externalEditor", function()
    // Have to fire editor after snippets, if snippets enabled
    if (StackExchange.settings.snippets.snippetsEnabled)
    StackExchange.using("snippets", function()
    createEditor();
    );

    else
    createEditor();

    );

    function createEditor()
    StackExchange.prepareEditor(
    heartbeatType: 'answer',
    convertImagesToLinks: true,
    noModals: false,
    showLowRepImageUploadWarning: true,
    reputationToPostImages: 10,
    bindNavPrevention: true,
    postfix: "",
    noCode: true, onDemand: true,
    discardSelector: ".discard-answer"
    ,immediatelyShowMarkdownHelp:true
    );



    );













     

    draft saved


    draft discarded


















    StackExchange.ready(
    function ()
    StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f312439%2fstrange-proofs-of-existence-theorems%23new-answer', 'question_page');

    );

    Post as a guest






























    5 Answers
    5






    active

    oldest

    votes








    5 Answers
    5






    active

    oldest

    votes









    active

    oldest

    votes






    active

    oldest

    votes








    up vote
    12
    down vote













    There are probabilistic proofs of existence. Do they fall into one of your three categories?



    For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost all" proof is easier than constructing an explicit example.



    See some nice examples due to Erdōs in the cited Wikipedia page which use only finite probability spaces. If we show that a probability is $ > 0$, then the set is not empty.






    share|cite|improve this answer






















    • I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
      – Noam D. Elkies
      16 mins ago














    up vote
    12
    down vote













    There are probabilistic proofs of existence. Do they fall into one of your three categories?



    For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost all" proof is easier than constructing an explicit example.



    See some nice examples due to Erdōs in the cited Wikipedia page which use only finite probability spaces. If we show that a probability is $ > 0$, then the set is not empty.






    share|cite|improve this answer






















    • I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
      – Noam D. Elkies
      16 mins ago












    up vote
    12
    down vote










    up vote
    12
    down vote









    There are probabilistic proofs of existence. Do they fall into one of your three categories?



    For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost all" proof is easier than constructing an explicit example.



    See some nice examples due to Erdōs in the cited Wikipedia page which use only finite probability spaces. If we show that a probability is $ > 0$, then the set is not empty.






    share|cite|improve this answer














    There are probabilistic proofs of existence. Do they fall into one of your three categories?



    For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost all" proof is easier than constructing an explicit example.



    See some nice examples due to Erdōs in the cited Wikipedia page which use only finite probability spaces. If we show that a probability is $ > 0$, then the set is not empty.







    share|cite|improve this answer














    share|cite|improve this answer



    share|cite|improve this answer








    edited 3 hours ago

























    answered 3 hours ago









    Gerald Edgar

    27.1k269154




    27.1k269154











    • I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
      – Noam D. Elkies
      16 mins ago
















    • I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
      – Noam D. Elkies
      16 mins ago















    I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
    – Noam D. Elkies
    16 mins ago




    I thought of that, but it's a kind of proof by contradiction -- the sum (or integral) over the set is positive, so if the set were empty we'd get 0>0.
    – Noam D. Elkies
    16 mins ago










    up vote
    3
    down vote













    I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $mathbbN$. In Peano artithmetic, Goodstein's theorem is unprovable.






    share|cite|improve this answer




















    • I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
      – Carl Mummert
      16 mins ago















    up vote
    3
    down vote













    I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $mathbbN$. In Peano artithmetic, Goodstein's theorem is unprovable.






    share|cite|improve this answer




















    • I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
      – Carl Mummert
      16 mins ago













    up vote
    3
    down vote










    up vote
    3
    down vote









    I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $mathbbN$. In Peano artithmetic, Goodstein's theorem is unprovable.






    share|cite|improve this answer












    I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $mathbbN$. In Peano artithmetic, Goodstein's theorem is unprovable.







    share|cite|improve this answer












    share|cite|improve this answer



    share|cite|improve this answer










    answered 2 hours ago









    Dominic van der Zypen

    13.2k43172




    13.2k43172











    • I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
      – Carl Mummert
      16 mins ago

















    • I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
      – Carl Mummert
      16 mins ago
















    I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
    – Carl Mummert
    16 mins ago





    I view this as an example of "moving to a higher space" in order to prove something. In Goodstein's theorem we move from the naturals to the collection of countable ordinals. Another example is in dynamical systems, when we begin with a compact dynamical system and move to the enveloping semigroup, or when we work with the Stone-Cech compactification of the naturals in combinatorics.
    – Carl Mummert
    16 mins ago











    up vote
    2
    down vote













    While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.



    It is (reasonably) clear what it means that a theorem has a constructive proof.



    "All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."



    Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.



    Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.



    Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.






    share|cite|improve this answer
























      up vote
      2
      down vote













      While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.



      It is (reasonably) clear what it means that a theorem has a constructive proof.



      "All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."



      Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.



      Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.



      Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.






      share|cite|improve this answer






















        up vote
        2
        down vote










        up vote
        2
        down vote









        While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.



        It is (reasonably) clear what it means that a theorem has a constructive proof.



        "All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."



        Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.



        Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.



        Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.






        share|cite|improve this answer












        While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.



        It is (reasonably) clear what it means that a theorem has a constructive proof.



        "All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."



        Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.



        Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.



        Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.







        share|cite|improve this answer












        share|cite|improve this answer



        share|cite|improve this answer










        answered 2 hours ago









        Arno

        1,2791120




        1,2791120




















            up vote
            2
            down vote













            There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$. The proof considers two cases: $sqrt2^sqrt2$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.



            You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.



            (By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)



            EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.






            share|cite|improve this answer




















            • Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
              – Sam Hopkins
              1 hour ago










            • I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
              – Carl Mummert
              19 mins ago














            up vote
            2
            down vote













            There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$. The proof considers two cases: $sqrt2^sqrt2$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.



            You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.



            (By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)



            EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.






            share|cite|improve this answer




















            • Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
              – Sam Hopkins
              1 hour ago










            • I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
              – Carl Mummert
              19 mins ago












            up vote
            2
            down vote










            up vote
            2
            down vote









            There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$. The proof considers two cases: $sqrt2^sqrt2$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.



            You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.



            (By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)



            EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.






            share|cite|improve this answer












            There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$. The proof considers two cases: $sqrt2^sqrt2$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.



            You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.



            (By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)



            EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.







            share|cite|improve this answer












            share|cite|improve this answer



            share|cite|improve this answer










            answered 1 hour ago









            Sam Hopkins

            3,76312346




            3,76312346











            • Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
              – Sam Hopkins
              1 hour ago










            • I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
              – Carl Mummert
              19 mins ago
















            • Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
              – Sam Hopkins
              1 hour ago










            • I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
              – Carl Mummert
              19 mins ago















            Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
            – Sam Hopkins
            1 hour ago




            Whoops, I didn’t see this was mentioned by Carl Mummert in the comments.
            – Sam Hopkins
            1 hour ago












            I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
            – Carl Mummert
            19 mins ago




            I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained.
            – Carl Mummert
            19 mins ago










            up vote
            0
            down vote













            I think applications of the Yoneda lemma fit your criteria.



            We often prove the existence of some isomorphism $f:Arightarrow B$ in a category $mathcalC$ by embedding $mathcalC$ in $Sets^mathcalC^OP$ using the Yoneda lemma $y$ and finding an iso $g:y(A)rightarrow y(B)$, then concluding that there exists some unique iso $f:Arightarrow B$ with $y(f)=g$ since $y$ is full and faithful.



            Exhibiting an arrow in $Sets^mathcalC^OP$ is often easier than in $mathcalC$ since $Sets$ is complete and cocomplete and Cartesian closed, which makes $Sets^mathcalC^OP$ complete and cocomplete and Cartesian closed even if $mathcalC$ isn't.



            We can thusly use 'higher order' tools like limits/colimits in $Sets^mathcalC^OP$ which we aren't allowed to use in $mathcalC$ to find arrows, then still infer the existence of an arrow in $mathcalC$ if the resulting arrow in $Sets^mathcalC^OP$ is between two contravariant representable functors.






            share|cite|improve this answer
















            • 1




              I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
              – Todd Trimble♦
              2 mins ago














            up vote
            0
            down vote













            I think applications of the Yoneda lemma fit your criteria.



            We often prove the existence of some isomorphism $f:Arightarrow B$ in a category $mathcalC$ by embedding $mathcalC$ in $Sets^mathcalC^OP$ using the Yoneda lemma $y$ and finding an iso $g:y(A)rightarrow y(B)$, then concluding that there exists some unique iso $f:Arightarrow B$ with $y(f)=g$ since $y$ is full and faithful.



            Exhibiting an arrow in $Sets^mathcalC^OP$ is often easier than in $mathcalC$ since $Sets$ is complete and cocomplete and Cartesian closed, which makes $Sets^mathcalC^OP$ complete and cocomplete and Cartesian closed even if $mathcalC$ isn't.



            We can thusly use 'higher order' tools like limits/colimits in $Sets^mathcalC^OP$ which we aren't allowed to use in $mathcalC$ to find arrows, then still infer the existence of an arrow in $mathcalC$ if the resulting arrow in $Sets^mathcalC^OP$ is between two contravariant representable functors.






            share|cite|improve this answer
















            • 1




              I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
              – Todd Trimble♦
              2 mins ago












            up vote
            0
            down vote










            up vote
            0
            down vote









            I think applications of the Yoneda lemma fit your criteria.



            We often prove the existence of some isomorphism $f:Arightarrow B$ in a category $mathcalC$ by embedding $mathcalC$ in $Sets^mathcalC^OP$ using the Yoneda lemma $y$ and finding an iso $g:y(A)rightarrow y(B)$, then concluding that there exists some unique iso $f:Arightarrow B$ with $y(f)=g$ since $y$ is full and faithful.



            Exhibiting an arrow in $Sets^mathcalC^OP$ is often easier than in $mathcalC$ since $Sets$ is complete and cocomplete and Cartesian closed, which makes $Sets^mathcalC^OP$ complete and cocomplete and Cartesian closed even if $mathcalC$ isn't.



            We can thusly use 'higher order' tools like limits/colimits in $Sets^mathcalC^OP$ which we aren't allowed to use in $mathcalC$ to find arrows, then still infer the existence of an arrow in $mathcalC$ if the resulting arrow in $Sets^mathcalC^OP$ is between two contravariant representable functors.






            share|cite|improve this answer












            I think applications of the Yoneda lemma fit your criteria.



            We often prove the existence of some isomorphism $f:Arightarrow B$ in a category $mathcalC$ by embedding $mathcalC$ in $Sets^mathcalC^OP$ using the Yoneda lemma $y$ and finding an iso $g:y(A)rightarrow y(B)$, then concluding that there exists some unique iso $f:Arightarrow B$ with $y(f)=g$ since $y$ is full and faithful.



            Exhibiting an arrow in $Sets^mathcalC^OP$ is often easier than in $mathcalC$ since $Sets$ is complete and cocomplete and Cartesian closed, which makes $Sets^mathcalC^OP$ complete and cocomplete and Cartesian closed even if $mathcalC$ isn't.



            We can thusly use 'higher order' tools like limits/colimits in $Sets^mathcalC^OP$ which we aren't allowed to use in $mathcalC$ to find arrows, then still infer the existence of an arrow in $mathcalC$ if the resulting arrow in $Sets^mathcalC^OP$ is between two contravariant representable functors.







            share|cite|improve this answer












            share|cite|improve this answer



            share|cite|improve this answer










            answered 27 mins ago









            Alec Rhea

            7681414




            7681414







            • 1




              I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
              – Todd Trimble♦
              2 mins ago












            • 1




              I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
              – Todd Trimble♦
              2 mins ago







            1




            1




            I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
            – Todd Trimble♦
            2 mins ago




            I really don't see how this is an example. In every possible instance, if one can write down an isomorphism between representables, one can straight away write down the corresponding isomorphism between representing objects.
            – Todd Trimble♦
            2 mins ago

















             

            draft saved


            draft discarded















































             


            draft saved


            draft discarded














            StackExchange.ready(
            function ()
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f312439%2fstrange-proofs-of-existence-theorems%23new-answer', 'question_page');

            );

            Post as a guest













































































            Comments

            Popular posts from this blog

            Long meetings (6-7 hours a day): Being “babysat” by supervisor

            Is the Concept of Multiple Fantasy Races Scientifically Flawed? [closed]

            Confectionery