We don't seem to understand each other yet :-(

If I understand correctly, you are saying that higher order logic cannot prove all theorems about the integers that ZFC can.

The argument wasn't specific to ZFC or HOL, it was intended to apply to any system that can have a proof checker.

Actually, I've never heard of the standard integers -- do you mean a unique standard model of the integers?

Sorry, I screwed up the wording there, meant to say simply "unique model of the integers". People often talk about "standard integers" and "nonstandard integers" within models of a first-order axiom system, like PA or ZFC, hence my screwup. "Standard model" seems to be an unrelated concept.

I've never heard it claimed that second-order logic has a unique model of the standard integers.

The original post says something like that, search for "we know that we have only one (full) model".

The comprehension axiom schema (or any other construction that can be used by a proof checker algorithm) isn't enough to prove all the statements people consider to be inescapable consequences of second-order logic. You can view the system you described as a many-sorted first-order theory with sets as one of the sorts, and notice that it cannot prove its own consistency (which can be rephrased as a statement about the integers, or about a certain Turing machine not halting) for the usual Goedelian reasons. But we humans can imagine that the integers exist as "hunks of Platoplasm" somewhere within math, so the consistency statement feels obviously true to us.

It's hard to say whether our intuitions are justified. But one thing we do know, provably, irrevocably and forever, is that being able to implement a proof checker algorithm precludes you from ever getting the claimed benefits of second-order logic, like having a unique model of the standard integers. Anyone who claims to transcend the reach of first-order logic in a way that's relevant to AI is either deluding themselves, or has made a big breakthrough that I'd love to know about.

Hold on a minute. What does it even mean to speak of proving something in second-order logic? First order has various deduction systems for it, which we usually don't bother to mention by name because they're all equivalent. How does one actually perform deductions in proofs in second-order logic? I was under the impression that second-order logic was purely descriptive (i.e. a language to write precise statements which then may judged true or false) and did not allow for deduction. After all, to perform deductions about sets, one will need some sort of theory of how the sets work, no? And then you may as well just do set theory -- which is after all how we generally do things...

I used Duolingo for a few hours on its first day. (I used to TA for Luis, which helps for getting private invites, at least by knowing to sign up immediately.)

I've basically just gone through passing out of German lessons. This basically consists of taking a 20 question test, in which I translate sentences like "The woman drinks with her cat." and pray I don't make typos on three questions and have to start over. Except that all too often I give correct translations, but their checker isn't attuned to the flexibilities of German word ordering, or I use a different word for "chair." They said they'd teach it the distinction between "essen" ("to eat" for humans) and "fressen" ("to eat" for animals) so that their quizzes would stop recommending wrong answers, but I'm skeptical. I did another one just now, and it now seems to accept answers off by one character. I noticed this in a listening exercise not because I made a typo, but because the word for "is" is approximately homonymous with the word for "eats."

Oh, apparently Duolingo has something to do with translating the web, rather than just going through a bunch of German 1-level exercises. Maybe I have to repeat the above for the remaining 45 lessons before I see an option to do that.

I looked into the Thiel scholarship, being age eligible. The problem is, it's so ridiculously competitive. I did fairly well in school, and certainly got in the top 1% of grades, as well as attending the NYSF. However, I look at the kind of people who won the Thiel fellowship and kind of wither. They're way out of my league. If LessWrong had many teenagers like that around, I suspect we would have heard of them by now.

The other 72.3% of people who had to find Less Wrong the hard way. 121 people (11.1%) were referred by a friend, 259 people (23.8%) were referred by blogs, 196 people (18%) were referred by Harry Potter and the Methods of Rationality, 96 people (8.8%) were referred by a search engine, and only one person (.1%) was referred by a class in school.

Of the 259 people referred by blogs, 134 told me which blog referred them. There was a very long tail here, with most blogs only referring one or two people, but the overwhelming winner was Common Sense Atheism, which is responsible for 18 current Less Wrong readers. Other important blogs and sites include Hacker News (11 people), Marginal Revolution (6 people), TV Tropes (5 people), and a three way tie for fifth between Reddit, SebastianMarshall.com, and You Are Not So Smart (3 people).

I've long been interested in whether Eliezer's fanfiction is an effective strategy, since it's so attention-getting (when Eliezer popped up in The New Yorker recently, pretty much his whole blurb was a description of MoR).

Of the listed strategies, only 'blogs' was greater than MoR. The long tail is particularly worrisome to me: LW/OB have frequently been linked in or submitted to Reddit and Hacker News, but those two account for only 14 people? Admittedly, weak SEO in the sense of submitting links to social news sites is a lot less time intensive than writing 1200 page Harry Potter fanfics and Louie has been complaining about us not doing even that, but still, the numbers look to be in MoR's favor.

For a lot of subjects, it's hard to beat school. You need constant feedback to improve in most areas, and good feedback is hard to come by without paying. I would recommend against trying to learn how to write a proof without a teacher as much as I would against learning piano. (I've tried both.)

I've been taught more things than I've learned on my own, but of the things I've learned poorly, most where things I learned on my own.

Why are so few people interested in applying for the Thiel scholarshp? I feel that it's obviously more educational than going to school. Are you so afraid of not getting it that you don't bother applying?