This week, I had the pleasure of chatting with metaeducat10n for the first time.

[00:53] metaeducation: When people bitch about how hard it is to write those analysis tools, they overlook the idea that if the tools were written to have allowed the user to enter the information in a structured form in the first place...it would make the intractable problems disappear entirely
[00:54] GusLacerda: yup, I agree very much
[00:54] GusLacerda: but they say "our users shouldn't have to learn programming!"
[00:55] GusLacerda: ultimately, though, there's no getting around that.... you need to be a "programmer" in order to express certain things
[00:55] GusLacerda: but I digress
[00:57] metaeducation: Yes, I wish schools focused on teaching people clearer expression. Math classes as they are don't have a lot of value. People will become interested in sine and cosine if they have more fundamental knowledge.
[00:57] metaeducation: A lot of that knowledge is on what it means to formalize something
[00:58] metaeducation: Being clear to a computer isn't just about programming--it's about being clear to yourself, and others.
[00:58] metaeducation: A computer is just a good straight-man
[00:58] GusLacerda: yes!
[00:58] GusLacerda: exactly

Related thoughts of mine:
* GIGO
* "Computer Science" is actually a very natural thing: while many people think of computers as a contingent product of western culture, just like any other technology, Computer Science is actually about universal mathematical patterns: real computers provide merely an embodiment of this. This is why computer science is not about computers.
* the main goal of programming languages should be to express human thoughts as directly and naturally as possible. If a simple thought can only be expressed by a complex program, then there is something wrong with the language.

Required plug: Sussman - The Legacy of Computer Science, whose message is that the main contribution of CS to civilization isn't technological, but cultural. Knowledge of formal concepts makes us powerful. Creating words for such concepts makes them easy to access.

A couple weeks ago I made a big edit on the Wikipedia article titled "Mathematical_models_in_physics", deleting some stuff that seemed to imply that "mathematics is not always faithful to physics" because of the Banach-Tarski Paradox.

I posted my justification for this here

Also here:
( Read more... )

Greenspun's tenth law of programming: Any sufficiently complicated C or Fortran program contains an ad-hoc, informally-specified, bug-ridden, slow implementation of half of CommonLisp.

Trying to do science without mathematics is analogous. When Hartry Field tries to formulate science in terms of nominalistic theories (he wanted to demonstrate that one can do science without referring to abstract entities), those theories can't avoid using abstractions (e.g. you could encode PA in terms of his space-points).

Number theory, like Lisp, is a sort of universal structure, just waiting to be discovered. See Minsky - "Alien Intelligence" (search for "A REAL LIFE EPISODE")

It's possible to do science without mathematics, but you might as well develop mathematics on the way.

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.

I am a realist-in-truth-value for recursively-enumerable statements. i.e. I believe that statements for which counterexamples could be found if they existed must be either true or false.

For example, the Goldbach conjecture must be either true or false (since if it were false, you could find a number >4 which is not a sum of two primes). Also, whether any Turing Machine halts is a recursively-enumerable problem.

Basically, it seems to me that any meaningful problem is recursively-enumerable.

A consequence of Gödel's Incompleteness:
If a set of axioms expressing PA is recursively-enumerable, there will be statements which are undecidable.

I believe there should be an algorithmic way of deciding all recursively-enumerable statements, i.e. an algorithmic way of proceeding in making mathematics prove more true things whenever you run into undecidabilities (i.e. whenever you correctly prove, using a meta-method, that a sentence G is true but not provable in the original system). But this seems not to be possible, for if there were any such algorithm, we could construct its halting problem, and *that* problem would be undecidable in the new system.

So I do think that Gödel's theorem is significant for the philosophy of mathematics. And it seems like Chaitin is onto something when he says that mathematics must be semi-empirical.


Again, thanks to Benedikt Löwe for reciting me the theorem above.

There are two kinds of ways of looking at mathematics... the Babylonian tradition and the Greek tradition... Euclid discovered that there was a way in which all the theorems of geometry could be ordered from a set of axioms that were particularly simple... The Babylonian attitude... is that you know all of the various theorems and many of the connections in between, but you have never fully realized that it could all come up from a bunch of axioms... Even in mathematics you can start in different places... In physics we need the Babylonian method, and not the Euclidian or Greek method.
— Richard Feynman

The physicist rightly dreads precise argument, since an argument which is only convincing if precise loses all its force if the assumptions upon which it is based are slightly changed, while an argument which is convincing though imprecise may well be stable under small perturbations of its underlying axioms.
— Jacob Schwartz, "The Pernicious Influence of Mathematics on Science", 1960, reprinted in Kac, Rota, Schwartz, Discrete Thoughts, 1992.

When I say I'm an advocate of formalization, I'm not saying we need to understand all the precise details of what we're arguing for (although this usually is the case in mathematics, at least more so than in physics). What I want to do is to formalize the partial structure that does exist in these vague ideas. Favoring a dynamic approach, I hold that we must accept formalizing theories in small steps, each adding more structure. We will need "stubs", and multiple, parallel stories to slowly evolve into a formal form. The point is that a vague, general idea *can* be formalized to a point: this is evidenced by the fact that we humans use precise reasoning when talking about them.
Again, the idea is about doing what humans do, formally. If the humans' idea is irremediably vague, we don't hope to do any better, but we do hope to formalize it as far as the ideas are thought out / understood (even if vaguely). To the extent that there exists a systematic (not necessarily "logical", but necessarily normative) in the way we reason and argue, it will be my goal to formalize this in a concrete form.

Regarding the normative aspect, the reason we need one is: not all ideas make sense! For fully-formalized mathematics (i.e. vagueness-free mathematics), it's easy to come up with a normative criterion: a mathematical idea or argument is fully-formalized if it corresponds to a fully-formal definition or a fully-formal proof. One of the challenges of this broader approach is to define what it means for an idea to "make sense": what does it attempt to do? What is its relation with related concepts?

The "natural" medium expression of these ideas is English. The idea is to connect English words to concepts in the formal knowledge system. We say an English sentence makes sense in a given context iff it addresses the goal / there is sound reasoning behind it (not all may be applicable).