Re: Constructive Proofs (Bishop)

Hi

If you want simple algorithms, use bounded
quantifiers. A lot of constructive analysis
is using this, and not intuitionistic logic.

Bye

guyontheinet@xxxxxxxxx wrote:

Does the difference between Bishop-Constructive mathematics and
classical mathematics arise only in the case of a proof that shows
that a particular kind of thing exists. If a theorem doesn't assert
that a particular kind of object exists are classical and
Bishop-constructivist proofs of that theorem interchangeable in
the sense that a Bishop proof gives an _exact_ classical proof
and vice verse for theorems of that type?

If one avoids proof-by-contradiction to prove that something
exists is that enough to ensure that his proof gives an algorithm
of how to construct that something? Does the algorithm just
"fall out" naturally if one follows that guideline or are there more
things that a constructivist must do to ensure that his proof
gives an algorithm?

Thanks & Happy Holidays.

.

Relevant Pages

  • Re: Constructive Proofs (Bishop)
    ... Jan Burse wrote: ... classical mathematics arise only in the case of a proof that shows ... Bishop-constructivist proofs of that theorem interchangeable in ... exists is that enough to ensure that his proof gives an algorithm ...
    (sci.logic)
  • Re: Constructive Proofs (Bishop)
    ... If a theorem doesn't assert ... Bishop-constructivist proofs of that theorem interchangeable in ... For example, for natural sumbers, for showing constructively that ... exists is that enough to ensure that his proof gives an algorithm ...
    (sci.logic)
  • Re: Provability
    ... terminates with a well-defined and asserted result. ... the definition of algorithm. ... computer science does consider a partial recursive function is to be "an ... situations exist is most of classical mathematics: ...
    (sci.math)
  • Re: Provability
    ... terminates with a well-defined and asserted result. ... the definition of algorithm. ... fact is that standard terminology in mathematics and theoretical ... situations exist is most of classical mathematics: ...
    (sci.math)
  • Re: Provability
    ... An algorithm is a procedure that takes input and ... That it does terminate with the asserted result must be ... to be no more than a partial recursive function. ... situations exist is most of classical mathematics: ...
    (sci.math)