gusl: (Default)
I'd like to see probability and measure theory reformulated in a theory where the Axiom of Choice isn't used. Non-measurable sets would never come up.

http://en.wikipedia.org/wiki/Non-measurable_set
<< In 1965, Solovay constructed Solovay's model, which shows that it is consistent with standard set theory, excluding uncountable choice, that all subsets of the reals are measurable. >>


Now every subset of the reals is measurable, and has the Baire property. Thus: a lot fewer concepts to worry about! And no more Banach-Tarski paradox.

Do we lose anything, really?

The idea that the only objects that exist are the constructible ones is, I think, a central idea in the worldview of computer scientists, who are, afterall, the current bearers of the intuitionistic flame; besides being central figures in ideas like cognition is computation, and so is the universe. To me, it's a direct consequence of thinking of the world (including ourselves) as machines; and the alternative borders on mysticism (a.k.a. metaphysics).

Coming back to mathematics, why don't I see any computer scientists working on Choice-free mathematics? And why don't I see mathematical librarians cataloging which bits of mathematics are still kosher, according to constructivists? I'd love to see a choice-free graduate mathematics curriculum, but I'd be happy to just see a book on Probability.
gusl: (Default)
In a philosophical conversation with [livejournal.com profile] spoonless today, I expressed my view succinctly:

"To me, the purpose of axioms should be to discover truths about mathematics, not to make truths."


If the Goldbach conjecture is false, all good axiom systems will agree about this. (You can replace "Goldbach conjecture" with any statement about the integers)

The situation is not the same for infinitary questions. The truth of statements like the Continuum Hypothesis, the determinacy of infinite games, etc is axiom-dependent. Therefore, these statements don't have an objective truth-value. Their meaning is thus relative to a model.

---

UPDATE:
I found someone talking about the phenomenon of axioms making truths:
"Their existence is axiomatic" -Robert Alain, about the non-standard integers

Such fictional objects are useful to the extent that they can give us information about the real objects.

Of course, even standard real analysis deals with non-real objects (the real real numbers are the computable real numbers, which form a countable set). Theorems in real analysis are useful because they tell us something about the computable real numbers.
gusl: (Default)
It is my opinion that the Russian school of intuitionism, founded by A. A. Markov Jr, deserves more attention than it gets... especially among those who subscribe to "computational thinking".

The philosophical motivation for CRM is that an operation is considered "constructive" if and only if it is recursive.
I like this because it suggests new way of formalizing mathematical statements, not in terms of unconstructive foundations like set theory, but in terms of computer programs: every mathematical statement φ gets translated into a statement about a single computer program T(φ) of the form "this assert never fails for any input".

One might point out that for any given axiom set, the set of theorems is RE (since we can build a theorem pump), and conclude that by this definition, all mathematics is constructive... but this is not sound given the above definition.

A theorem statement is constructive only if all the functions it calls and all sets it quantifies over are recursive (or, in terms of functional programming languages: a function is implemented iff all the functions it calls are implemented).

Much of higher math, as it's practiced, involves doing computable things on uncomputable oracles, and vice-versa, in a soup of definitions; and much of the goal of the constructive movements (as I understand it) was to "clean out" that stuff. Perhaps their concern was epistemic hygiene. My concern is meaningfulness and effectiveness: what good is a piece of mathematics if it doesn't say anything about any imaginable situation?

Now I should discuss the status of traditional axiomatic theories (i.e. theories that state the existence of unconstructible objects, and give them names). Of course, we can imagine a universe in which mathematicians talk "meaningfully" about non-constructible objects such as higher infinities (we are in one!). It's tempting for me to say that truth of such statements is defined by their provability... but truth is normally defined in terms of models, and the model-checking procedure, while always recursive (AFAIK), may involve calling uncomputable oracles.

My current intuition is this: uncomputability creates a gap between mathematical statements, and provability (via non-constructive operations) closes this gap.

My view is that uncomputable oracles, such as usages of the full axiom of choice, are useful only to the extent that their results transfer faithfully to the computable universe. (Results in computable analysis reassure me that I don't need to spend my time computationalizing every analysis theorem that I come across)

Unfortunately, many early sources from the Markov school are only available in Russian. Since any copyright should be expired by now, I would encourage anyone who can to translate them and make them freely available. I'm happy to host.


Here are some key references, courtesy of A.S. Troelstra:
"A constructive logic" (Russian), Usp. Math. Nauk 5(3) 1950, 187-188 (reviewed JSL 18,p.257)

"On the continuity of constructive functions" (Russian) Usp Math Nauk 9(3), 226-230 (1954), (review JSL 21, p.319).

See for bibliographical information Vol VI of the Omega-Bibliography of Mathematical Logic, edited by Gert H. Müller+ Springer Verlag, Heidelberg 1987.

A good introduction to the ideas and results of the Markov school is the book B.A. Kushner, Lectures on Mathematical Analysis, American Math. Soc.1984
gusl: (Default)
This week, I had the pleasure of chatting with [livejournal.com profile] 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.
gusl: (Default)
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... )
gusl: (Default)
It's impossible to prove Pi_1 statements without axioms that talk about infinity.

If it were possible, I would like to do it right now with Lisp. I have implemented a refuter for general Pi_1 statements, but even though implementing a verifier would never be successful, I still firmly believe in some proofs of Pi_1 statements. That means that I must implicitly accept axioms about infinity, much as I'd like not to.

Here's a nice theorem:
;;;All numbers with an odd number of divisors are perfect squares:
(forall #'(lambda (n) (implies (not (perfect-square-p n)) (evenp (n-divisors n)))))


And here's a nice proof:

(Lemma 1) Forall n in N, n is a perfect square IFF its prime factorization has an even power at all the primes.
(Lemma 2) Forall n in N, n-divisors(n) = PRODUCT (power(p_i,n) + 1) for each prime p_i in the factorization of n

Suppose n is not a perfect square (1)
Then there is a prime p in the prime factorization of n such that its power is odd. (by 1, L1)(2)
Since power(p,n) is odd, then power(p,n) + 1 is even. (3)
Then n-divisors(n) is even. (by 3, L2) (4)


But which axioms am I using in this proof? Are they too hard to dig out of the lemmas? My justification for the lemmas is my visual intuitions. Somewhere in proving them in any kind of system, you would need an axiom about infinity, right?


in case you want the rest of the Lisp code:
Read more... )
gusl: (Default)

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.
gusl: (Default)
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 [livejournal.com profile] 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.
gusl: (Default)
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.
gusl: (Default)
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).

Profile

gusl: (Default)
gusl

December 2016

S M T W T F S
    123
45678910
11121314151617
18 192021222324
25262728293031

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags