/sci/ - Science & Math

[petarded No.6710269]

Hi /sci/ What is your opinion on Constructive Mathematics? Is someone of you maybe involved in research in that area?

[Anonymous No.6710280]

>>6710269
What is Constructive Mathematics?

[petarded No.6710289]

>>6710280
Mathematics in which existence of an object means one can construct such an object. Every object is an algorithm, and proofs have to contain a construction and a formal proof of the properties the construction should have.

[Anonymous No.6710290]

>>6710280
http://lmgtfy.com/?q=Constructive+Mathematics

[Anonymous No.6710343]

bump

[Anonymous No.6710364]

>can't do proofs by contradiction

dropped.

[Anonymous No.6710373]

>>6710364
sure you can, just not proves about existence

[Anonymous No.6710419]

>>6710364
You might want to do some reading.
If you show "P leads to a contradiction", then you have shown not(P), also in the intuitionistic framework. In fact not(P) is defined this way.
What you can't do it so conclude P from " 'P leads to a contradition' leads to a contradition". If you show the latter, you've shown not(not(P)), which isn't the same as P.

Saying "P or not(P)" should be dropped is reasonable for description of many things, while other logical relations are more robust. E.g. "My bath tub is either good or bad at teaching logic" is a shitty proposition, you'd want to drop excluded middle altogher. Classical logic is not suitable for some things.

You can think of propositions P as tasks and proofs as their corresponding possible realization (= Curry-Howard isomophism).
not(P) is similar to a task which one can't finish.
You can establish that an algorithm never ends (e.g. by reading C code and observing someone coded an unending for-loop), and that corresponds to your proof by contradiction.
What you can't to is to gain insight on how to do a task, just by observing that an unending algorithm leads to another unending algorithm (unending subroutines might fuck up your code).

Here's a nice example:
http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation

Given that intuitionistic logic is a proper subsystem of classical logic and the distinction is a clear one, it's hard not to like.
(I'm less enthusiastic of the modern considerations on identity and its computational contents. That doesn't mean I'd reject it, just that it's too tedious for me. And since "second order logic is set theory in disguise", as they say, and since sets are used everywhere, the "naive" substitution rules which come with "is equal to", together with the axiom of extensionality, is everything I need in my day to day life.)
I think excluded middle restricts your horizon - good riddance. I'm ambivalent on choice.

[Anonymous No.6710423]

>>6710289
I don't use anything else.
unless I'm being lazy

[Anonymous No.6710434]

>>6710423
you calling erdös lazy?

[Anonymous No.6710453]

Before someone jumps my throat, I've made the bath tub up on the spot freely replaced not being good with being bad. The point I want to bring home is that you might choose to not make your logic capable of reasoning about silly things like a bath tubs teaching skills. You can try to pull up everything intuitionistically, obtain nice algorithms* and then add excluded middle later, if you need it, and that's a clean approach. So say the comp. sci people.
*Obligatory link: http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

[Anonymous No.6710464]

>>6710434
No I'm calling myself lazy.
When I study I'm nice and constructive.
When I'm working, a convincing argument is enough.

[Anonymous No.6710469]

>>6710464
so youre being lazy when youre working? interesting.