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

[easwaran.livejournal.com]

I think this position actually gets at least a weak sort of constructivism, so that you have to deny excluded middle. It's possible that there is no computable proof of the Goldbach conjecture, and yet there is no computable procedure that gives an even number that isn't the sum of two primes. Actually, I probably can't even state that in the computable language.

[gustavolacerda.livejournal.com]

I think this position actually gets at least a weak sort of constructivism, so that you have to deny excluded middle.

I'd love to know what you're talking about...

[easwaran.livejournal.com]

That is, if you're only going to admit the existence of things for which a computation can be given, then I think certain existential statements will not be provable, even though a contradiction can be reached from its negation. Thus, neither the statement nor its negation will be "true" in your sense, and this is basically the intuitionist position.

[gustavolacerda.livejournal.com]

even though a contradiction can be reached from its negation

hey, that's a proof to me!

Does this seem somehow inconsistent with my other beliefs here?

[easwaran.livejournal.com]

I think I have to think about this a bit more. There might be some statements that end up with different truth values than their classical counterparts, but maybe you're right that you can do this without ending up denying excluded middle.

Though intuitionists also don't deny any particular instance of excluded middle - they just don't assert every instance. Their idea is that assertion of a negation is just denial of the asserted statement, and there are many statements for which we have no grounds to either assert or deny them.

I think it's possible for your system that there be an existential statement that is not satisfied by any computable real number, but for which this non-existence has no computable proof. In fact, Gödel's theorem might require there to be such statements. On your computational methodology, it seems to make no sense to either assert or deny this statement. Would you then deny that it is a meaningful statement?

[gustavolacerda.livejournal.com]

I'm familiar with intuitionism, although I think it's a terrible way to do math.


I think it's possible for your system that there be an existential statement that is not satisfied by any computable real number, but for which this non-existence has no computable proof. In fact, Gödel's theorem might require there to be such statements. On your computational methodology, it seems to make no sense to either assert or deny this statement. Would you then deny that it is a meaningful statement?

I would consider such a statement as true but not provable. But this can be fixed for any individual instance by adding a new axiom. Of course, you'll always have new undecidable statements... even with infinitely many axioms, I think.

We humans tend to consider ourselves to be outside of any axiomatic system... but I think this is wrong.
For example, when we talk something being true but not provable, we claim to know the theorem in a somehow transcendent way. But we are just a meta-level higher than the system.

Unprovable Truths

[henriknordmark.livejournal.com]

If you are a devoted Platonist, there is no problem with having mathematical statements that are true but not provable. It simply means that in the Platonic Realm the mathematical statement is true, but we will never be able to know that truth by simple deductive reasoning in an axiomatic system like Peano Arithmetic (PA).

However, for me personally, I find this problematic because if we are not using logical deduction in an axiom system to determine an unprovable truth Phi(x), then on what grounds can we really claim that Phi(x) holds? Do you start believing in some mysterious mystical ability to apprehend Phi(x) to be true as the Platonists believe? Woodin has a whole research program around determining whether the Continuum Hypothesis (CH) is true despite that we know that CH is independent of ZF. It seems that Woodin wants to show that (CH) is false because it is mathematically intuitive to have a "healthy dosis of large cardinals", which would contradict CH. But why should we believe we need this healthy dosis of large cardinals in the first place?

[combinator.livejournal.com]

It's possible that there is no computable proof of the Goldbach conjecture, and yet there is no computable procedure that gives an even number that isn't the sum of two primes.

Well, we know that if Goldbach's conjecture is false, there exists an even number which is not the sum of two primes. A computable procedure to find it is to search exhaustively. Better yet, the number itself stands as a computable proof. So what you said is equivalent to "It's possible that there is no computable proof of the Goldbach conjecture, but it is still true." On the other hand, if Goldbach's conjecture is true, a computable procedure to find the "prime decomposition" of any even number is to search exhaustively. Then in what sense would the proof be nonconstructive?

It's almost the same with P versus NP. If P =/= NP, well, there isn't much we can do in the way of computation anyway. If P = NP, even if the proof is "noncomputable", we can actually concoct a Turing machine to compute NP in P, by exhaustively trying all Turing machines in an interleaved fashion and verifying the output of each. This procedure will take a polynomial amount of time, since as N approaches infinity, one finite Turing machine will be able to compute SAT quickly, and the overall procedure will only take a quadratic amount of extra time compared to this optimal machine. Do I need to go into more detail?

[r6.livejournal.com]

combinator is right. In other words, the Goldbach conjecture is a Π₁ sentence. Every true Σ₁ sentence is provable in PA. And every Π₂ sentence that is provable in PA is provable in HA, and hence has a computable procedure associated with it.

[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).

[easwaran.livejournal.com]

I should have chosen as an example some sort of existential statement for real numbers, rather than natural numbers, because of course if you prove that such a number exists, there is an effective search procedure for the naturals.

Perhaps even the least upper bound property for sets of real numbers might not turn out to be true. Certainly for recursive sets of real numbers one can construct a least upper bound, but even just recursively enumerable sets might not give an effective least upper bound.

Constructivism

[r6.livejournal.com]

I’m not sure constructivism is needed for his point of view. Perhaps gustavolacerda is just saying that L=V. Would that be sufficient?

Re: Constructivism

[gustavolacerda.livejournal.com]

what are L and V?