computational philosophy of mathematics

[gusl]

I only believe in mathematical objects with finite information (i.e. with a finite expression). Things can expressed in any way you wish, intensionally, extensionally, whatever. So, while the natural numbers exist, not all subsets of it do.

While the set of real numbers exists (R can be expressed as the power set of N), not all of the traditional real numbers exist (only the computable ones do). So, in my definition, the cardinality of R is aleph_0 (i.e. the same as N). In fact, no set can have greater cardinality, for that would imply it had non-existing elements (since only computable things exist).

Can we design a set theory this way? How much of traditional set theory can be translated? Does we lose any good mathematics this way?

Whereas people seem to view uncomputability as a fundamental property of a problem, I tend to view it as another form of self-reference paradoxes. All "well-defined" problems are computable. Again, this is not a theorem or mathematical insight, but a re-definition, just like my "R only has countably many existing numbers" is a definition. But the point isn't just to change names and keep everything the same... it's to change the intuition that goes with the names.

Comments

[rdore.livejournal.com]

How about if the Goldbach conjecture is true, but it's only provable in noncomputable ways? Then certainly there's no computable proof that it's false as well. (It's not exactly clear to me what we'd mean by a noncomputable proof in any case.)

Also I don't see why P =/= NP would have any interesting consequences on what is or isn't computable - just consequences on what is computable efficiently.

[combinator.livejournal.com]

Re your first comment: I don't see the difference between what I was saying and what you are saying. "the Goldbach conjecture is true, but it's only provable in noncomputable ways" versus "there is no computable proof of the Goldbach conjecture, but it is still true". I guess by "noncomputable" we mean "the proof cannot be verified by a computer"? I guess I was starting to blur the line between that and "the proof does not give a computable construction for the objects it proves the existence of".

Re your second comment: Right, my statement of "there isn't much we can do in the way of computation anyway" was meant to convey that there isn't a constructive computation procedure that you would want to get out of the proof that P =/= NP. Rather, this would be a proof that a certain object (a Turing machine) could not be constructed. Both P and NP are computable, but we only believe P is effectively computable (and really only parts of P, but that's harder to quantify).

[gustavolacerda.livejournal.com]

AFAIK proofs are always finite, by any definition. And thus computable.

What *would* be interesting was if we had a proof theory result that when you add an axiom, some "infinite proofs" in the weak theory can be turned into finite proofs (i.e. "real" proofs) in the stronger theory. So stronger theories prove more things because they make more proofs small enough (i.e. finite).

I posted a related result a few entries back.

[rdore.livejournal.com]

Of course they are. I'm stupid.

[gustavolacerda.livejournal.com]

you should know that I'm immune to sarcasm. (in other words, I believe whatever you say)

[rdore.livejournal.com]

The "Of course they are," part was meant seriously. The "I'm stupid," was meant seriously, but only in a locally way (i.e. that comment was stupid of me).