4-way dialogue between Me, Henrik and our Duals about computational philosophy of math

[gusl]

In the philosophy of mathematics...

I am a formalist...

but let me tell you a story.


The characters are:

* Strawman Platonist
* We(1) is a mathematician who believes that if mathematical objects exist at all, then infinite-information mathematical objects exist too.
* We(2) takes a computer scientists' view. He's a total reductionist and in particular, believes in digital physics.


We(2) subscribes to an ontology of mathematics which says that only recursive objects exist:
* Infinite things do not really exist. We can talk about them as what would happen in the limit.
e.g. The set of natural numbers does not exist. What does exist is an algorithm which generates "them".

We(2) believes that the reason We(1) talks about infinite things is because it is simpler to talk about them as if they existed. The set N is a convenient fiction. Talking about algorithms just makes life more complicated. We(2) says that if We(1) were right, then We(1)'s access to it would be mediated through an oracle. Like most normal mathematicians, We(1) normally talks about mathematics as if oracles existed.

We(2) believes that oracles don't exist.

We(2) believes that the set N is an idealization of the algorithm which produces 0, S0, SS0, SSS0, etc. All sets are lists, and thus well-ordered.


WE(2)'s ONTOLOGY:

* Recursive objects. The algorithm producing it terminates.
* r.e. objects, which are the limit of what the algorithm would produce.
* co-r.e. objects, which are the same, since in the limit, a set can defined by its elements as well as by its non-elements.

While recursive objects really exist (or can be directly perceived by mathematical cognition), r.e. and co-r.e. objects live in the Platonic realm.

We(2) has read his Kevin Kelly and believes that the channel through which we communicate with the Platonic realm is restricted by computability. (Kelly talks about the scientific process as a channel between the scientist and nature... here we talk about the channel between mathematician and *** THE PLATONIC REALM ***)

BUT, since We(2) thinks it doesn't make sense to talk about unknowable things (especially in mathematics!), then the only mathematical objects that it makes sense to say exist are the ones which are somehow knowable (i.e. through this channel)!



In We(2)'s ontology, is pi recursive or r.e.?

In a sense, pi is r.e.... pi is an algorithm which successively approximates the Platonic pi.
However, proofs about pi are recursive. (proofs are always recursive!)
So, we could say that proofs about pi only make reference to Pi.
But do proofs ever do anything other than refer? Sure, when are objects are computable: e.g. a proof that 2 + 3 = 5 in PA uses the senses of 2, 3 and 5. (at least, a formalist would agree that "SS0" is the sense of 2)

So We(2) makes a distinction between sense and reference for all mathematical objects. While some references can be reduced to their senses (e.g. any finite number or any finite set), some references have senses that are "transcendental" and can only be accessed through an oracle (e.g. any infinite set)

While pi's reference is recursive, pi itself (i.e. its sense) is r.e.
All mathematical objects have recursive reference (at least I've never seen a non-recursive reference printed anywhere ;-) ). Just like you're sending me an email this very moment... I've never been contradicted on this either! (stolen from fare)


A little dialogue

Gustavo: Isn't it paradoxical that R has finite information (afterall it's easy to check whether something is in R), and yet some elements in it have infinite information? All objects used in mathematical discourse, even Platonic discourse, have finite information.

Henrik: No, we can reference R in a finite way, but R itself has infinite information.

Gustavo: and, also, sometimes it may be very hard to check whether a number is in R... especially if the input is coded in terms of a difficult question (like the Riemann hypothesis)

Henrik: but in principle, even the Riemann hypothesis could be decidable axiomatically. O buraco é mais embaixo. (The real problem is worse than you think)


Gustavo is struggling with his intuitions about which mathematical statements are meaningful, and therefore should be provable. Gustavo is not comfortable with mathematics being semi-empirical. He wants an algorithmic way of coming up with new axioms.

Tentative definition: A statement is meaningful iff it is in principle verifiable or falsifiable. It would be nice to have a logic of which statements are meaningful:

"A /\ B" is meaningful iff "A" is meaningful and "B" is meaningful
"A \/ B" is meaningful iff "A" is meaningful and "B" is meaningful
"A -> B" is meaningful iff "A" is meaningful and "B" is meaningful
"~A" is meaningful iff "A" is meaningful
"forall x in X, phi(x)" is meaningful iff it is meaningful for each "phi(x)" for each x in X.

(is it not an accident that I had to bring the X outside of the quote for the definition of the universal, unlike all good definitions of semantics?)



Interlude: The diagonalization argument according to our view of infinite objects as non-terminating algorithms...

Given any algorithm producing infinitely-many infinite decimal expansions (each of which is really an algorithm) (i.e. given any infinite list of real numbers) (NB: lists are necessarily countable),

our construction algorithm outputs an algorithm which produces an infinite decimal expansion which differs from all decimal expansions above in at least one place (i.e. a real number which will never be produced by the algorithm above)

So the set R of all real numbers is not even r.e.

Let's look at the types of these algorithms, so that we may see something about the nature of R. (Can we talk about types when algorithms don't terminate?)

A number from 0-9 : D (e.g. 5 : D)
An infinite decimal expansion is of type A, (decimal expansion : list_of D) (e.g. pi : list_of D)
An algorithm producing decimal expansions : list_of (list_of D) (e.g. any list of real numbers)
Our diagonal construction algorithm returning a novel real number : (list_of (list_of D)) -> (list_of D)

list_of is a dependent type, taking a type as input.

Gustavo is hoping that we can somehow dismiss R as meaningless, using the fact that it's not r.e.


Reinterpreting the Quantifiers

forall is an infinite conjunction, e.g. forall x in N.phi(x) is actually phi(0) /\ phi(1) /\ phi(2) /\ ...
exists is an infinite disjunction, e.g. exists x in N.phi(x) is actually phi(0) \/ phi(1) \/ ...

so, "forall x in N. phi(x)" is not verifiable (it may be provable using axioms, but that's a different story)
likewise, "exists x in N. phi(x)" is not refutable.

To verify "forall x in N. phi(x)", we would need a machine that checks phi for all natural numbers.... such a machine requires an oracle. Remember: oracles don't exist!



Topological semantics

verifiable : open
refutable : closed
/\ : intersection
\/ : union
~ : complement

Suppose phi(x) is verifiable for all x. i.e. forall x, phi(x) is an open set.
Can we say that "forall x in N. phi(x)" is verifiable? No, because an infinite intersection of open sets is not necessarily open.