I'm 17 and just got into a top U.S. college, where I want to major in math and economics. I am a bit worried that I haven't learned good work habits and that I waste too much time on the internet, since high school was mostly a breeze for me. I've heard from a lot of people that kids like me get hit hard in college when they have to work hard for the first time, and while I can think of lots of reasons I'm different, this is probably a good situation to take the outside view.

So in short, I'd love a mentor. How does this work, exactly?

I'm in my last year of studying CS/Math as an undergradate at MIT (I'm going to do a Master's next year though). I'd really like some advice about what I should do after I graduate - Grad school? Industry? Any alternative?

I care a fair amount about reducing xrisk, but I am also fairly skeptical that there is much I can do about it right now.

I have job offers with Google and some tech start-ups, and I suspect I could get a job in finance if I tried. I personally have some desire to start a tech company one day. I'm not sure what the tradeoff between doing good work and making money is, but I suspect my main goal should be maximizing expected income. I'd try to use most my money to support people doing good things. (Though I'm not sure money is the limiting factor here. Perhaps discovering what to do would be better...)

I'm not sure whether I can get into a top graduate school - I have a 5.0 technical GPA (4.8 overall), but no research record or particularly good recommendations at the moment. I believe I am much better than most mathematicians/computer scientists, but I am also not sure what sort of research I could do that I would consider worthwhile. Realistically, I am at least 2 huge leaps down from being as good as, say, John Von Neumann (that is, people far from as good as him are far better than me). I also have really bad attention span, and tend not to think about problems for extended periods of time. I'm not sure this is worth factoring in, as it can probably be remedied. Even if I am not suited for solving the really hard theory problems out there, but minimally, I can code and do math better than most people in most labs. I'm basically open to going to graduate school in any field, as long as I'd make an impact, and hopefully have a comparative advantage.

I've talked to a number people about this, but I'm still pretty uncertain about what to do. I'd love to hear people's thoughts. Thanks in advance!

I'm in the Cambridge area, and haven't been attending meetups, but this seems like the most awesome possible way to start. What is the mailing list/point of contact to work things out with Cambridge meet-up guys?

Are you confusing soundness with consistency? omega-consistency is much weaker than soundness.

Consistency: a syntactic claim that it's impossible to derive a contradiction. Doesn't require a notion of truth to be useful.

Omega-consistency: a syntactic claim that it's impossible to prove certain statements together. Doesn't need a notion of truth, but is motivated by the standard model of natural numbers.

Soundness: a semantic claim that given a specific notion of "true" as applies to a statement, e.g. truth in the model N of natural numbers, all the axioms of the theory are true. Automatically implies both consistency and omega-consistency. Requires a notion of the "intended model" or a "standard model" for the theory in which we consider the truth of propositions. For example, soundness is meaningless to talk about in the case of ZFC, which doesn't have an intended model.

I think this argument holds as long as the other formal system is recursively enumerable, and if PA is omega-consistent.

Look at this sentence from the argument:

"If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts."

If the oracle for a formal system S says "yes" on a given statement S that encodes the proposition "a Turing machine T will halt on this input", this means that S proves this proposition. It does not mean that the proposition is true and T will in fact halt! For that to be true, you need the formal system S to be sound. S could easily be omega-consistent and not sound, in which case it'll lie to you (example, assuming you believe PA to be consistent: the formal system.

If they were, the oracle would never be more helpful than a halting oracle, no?

But we want the oracle to be less helpful than the halting oracle...

Anyway, the question is settled now, thanks a lot :-)

I'm a little out of my depth here, so sorry if my comments don't make sense.

Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.

That's supposed to be a r.e. set of axioms, not a single axiom, right? I can easily imagine the program that successively prints the axioms R(x) for all x in L, but how do you enumerate the axioms not R(x) for all x not in L, given that L is only r.e. and not recursive? Or am I missing some easy way to have the whole thing as a single axiom without pulling in the machinery for running arbitrary programs and such?

On second thought, maybe we don't need the second part. Just having R(x) for all x in L could be enough.

It seems pretty clear that the only things this theory proves are things that FOL proves, silly things about the successor function, and silly things about R, like "forall x, R(x) -> R(x)" and "(R(14) and R(12)) -> R(17)" where R(14) is false. So an oracle for the logical implications of this theory is basically the same as an oracle for L.

I don't completely understand why there won't be an accidental smart thing among all the silly things...

I believe the answer to your question is yes. I'm going to just interpret "formal system" as "first order theory", and then try to do the most straightforward thing.

Take a language L of intermediate degree, as constructed via the priority method. I'd like to just take the strings (or numbers) in this language to be the theory's axioms. So let the theory have some 1-ary relation, call it R, as well as +, and constants 0 and 1. Assert that everything has a successor, just to get the "natural numbers" (without having multiplication though). Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.

It seems pretty clear that the only things this theory proves are things that FOL proves, silly things about the successor function, and silly things about R, like "forall x, R(x) -> R(x)" and "(R(14) and R(12)) -> R(17)" where R(14) is false. So an oracle for the logical implications of this theory has the same degree as an oracle for L.

Don't feel like thinking about how to say/prove this part formally, but maybe someone can help (or correct) me. Also, for reference, Presburger arithmetic is basically arithmetic without multiplication, and is decidable.

Right. Also there's always the freaky possibility that there's no such thing as the "standard integers". After all, we don't really have any formal grounds to believe that they exist, only unreliable evolved intuitions about counting apples, and these have already let us down many times (e.g. Russell's paradox).

So having a provability oracle for PA, or any other formal system that has a model containing the standard integers (like ZFC), is equivalent to having a halting oracle

No, you need guarantees on the formal system's complexity, similar to the ones in Godel's incompleteness theorem(s). You also need the formal system to be sound for your argument to carry through. This is stronger than your "has a model containing the standard integers", and is equivalent to "has the standard integers as a model".

In other words, if you knew all about the logical implications of PA, then you would also know all about the logical implications of ZFC

Note that you're assuming here that PA is sound and in particular consistent.

Is there a formal system (not talking about the standard integers, I guess) whose provability oracle is strictly weaker than the halting oracle, but still uncomputable?

The halting oracle's uncomputability degree is the smallest possible uncomputable degree, so no.