3 ms·

> computer science is a branch of mathematics that deals with large but finite structures (so they need an algorithmic description) Another way to put this is

> computer science is a branch of mathematics that deals with large but finite structures (so they need an algorithmic description) Another way to put this is that computer science deals with mostly constructive mathematics (more precisely, mathematics that uses intuitionistic logic, the kind that is natural to most programmers and computer scientists anyway). For instance, when you prove the fundamental theorem of arithmetic, you actually can translate that into an algorithm for factorizing numbers into products of powers of primes. And the converse holds too, an algorithm is a proof! If you can give me an algorithm that, given a number n, always produces a prime bigger than n, then that actually witnesses the infinitude of primes. Constructive methods are everywhere in CS, for instance, to prove a proposition P, it's possible in classical math to say "assume (not P) is true, then derive a contradiction, hence P", however that would be really unnatural in CS! You never hear "I want to show an algorithm to solve P exists, let's suppose it's not computable, ... contradiction!", because you don't end up with an algorithm at all (what you proved instead was that it's impossible for an algorithm to not exist, without saying what it is). Likewise, you if want to show some number/program/data structure has the properties you care about you almost always give the description explicitly. For more information, I'd say that type theory is a great intersection of math and computer science in a way that's quite accessible to programmers, since we're already used to this kind of thinking, even if we weren't explicitly taught it.

Scarblac 5y ago
Although the standard proof of the incomputability of the halting problem assumes it is computable and then reaches a contradiction. And that's more or less the central proof of everything to do with computability.
- siraben 5y ago
  That's still constructive. This can be a confusion because there's actually two kinds of contradiction proofs: to show ¬ P, assume P then derive a contradiction (false, ⊥) i.e., ¬ P := P -> ⊥. This is actually just fine and constructive, it's just how you prove a negation. OTOH, there's another kind of contradiction proof: to show P, assume ¬ P, then derive a contradiction (false, ⊥) Written with function notation, this becomes P <-> (¬ P -> ⊥) But if we unfold the definition of negation, we have that P <-> ((P -> ⊥) -> ⊥) The left to right direction holds classically and constructive, but the right to left direction uses double negation, which can is equivalent to the law of the excluded middle, AKA classical reasoning.
  - momentoftop 5y ago
    Sometimes, the strategy of proving ~P by showing how P entails absurdity is called "proof by negation". The phrase "proof by contradiction" is then reserved for the strategy of proving P by showing how ~P entails absurdity. On that usage, constructivists are happy with all proofs by negation, but not generally happy with proofs by contradiction.
bitL 5y ago
I find relevance logic much more intuitive than intuitionistic. Intuitionistic has still some weird assumptions that make it fit a lookup table like classical logic.

Scarblac 5y ago

Although the standard proof of the incomputability of the halting problem assumes it is computable and then reaches a contradiction. And that's more or less the central proof of everything to do with computability.

siraben 5y ago
That's still constructive. This can be a confusion because there's actually two kinds of contradiction proofs: to show ¬ P, assume P then derive a contradiction (false, ⊥) i.e., ¬ P := P -> ⊥. This is actually just fine and constructive, it's just how you prove a negation. OTOH, there's another kind of contradiction proof: to show P, assume ¬ P, then derive a contradiction (false, ⊥) Written with function notation, this becomes P <-> (¬ P -> ⊥) But if we unfold the definition of negation, we have that P <-> ((P -> ⊥) -> ⊥) The left to right direction holds classically and constructive, but the right to left direction uses double negation, which can is equivalent to the law of the excluded middle, AKA classical reasoning.
- momentoftop 5y ago
  Sometimes, the strategy of proving ~P by showing how P entails absurdity is called "proof by negation". The phrase "proof by contradiction" is then reserved for the strategy of proving P by showing how ~P entails absurdity. On that usage, constructivists are happy with all proofs by negation, but not generally happy with proofs by contradiction.

bitL 5y ago

I find relevance logic much more intuitive than intuitionistic. Intuitionistic has still some weird assumptions that make it fit a lookup table like classical logic.