00:06:26 <kmc> this is the one area where nerds -- usually a fairly intellectual lot -- are extremely proud of ignorance

00:10:18 <kmc> baseball's just on my mind because San Francisco won at baseball and now all the nerds in San Francisco are loudly proclaiming how much they don't know or care about baseball

00:12:50 <pikhq> olsner: Some other countries play baseball. Japan managed to get other bits of Asia in on it, and it's apparently pretty common in the Carribean.

00:13:40 <pikhq> Also, I can't comment about the ignorance: I don't actively *follow* most sports, but I'm not exactly ignorant on them.

00:14:06 <pikhq> (hell, I've been known to nerd out on the origins of (American) football and its relation to other games)

00:15:20 <pikhq> For the most part? Yeah, it's just nerding out about sports instead of something else.

00:16:16 <pikhq> Especially given that for most spectator sports, 99% of the audience doesn't actually *do* the sport in question.

00:16:42 <kmc> baseball in particular is all about the stats and the obsessive knowledge of past games and teams

00:16:57 <Phantom__Hoover> kmc, in that case your workplace is either so relaxed I can't believe someone's going to flip out over some cursing, or you deserve what's coming to you anyway.

00:20:31 <kmc> there's a rule that whenever spots are brought up, you have to be the loudest in proclaiming your utter contempt and ignorance of sports

00:20:56 <kmc> this is one of the aspects of "nerd culture" which I think derives directly from middle school bullying or something

00:23:36 <comex> it's one vote for me, one vote for scshunt, one vote endorsing me, two present, endorse Google Groups, and denounce Google Groups :p

00:24:14 <elliott> comex: well you can arbitrarily declare yourself the winner by having taral decide you'd be good to give the lists :P

00:24:26 <comex> and I started a vote because I felt it was an appropriately Agoran way to do things :p

00:25:01 <quintopia> is there anything a regex can do that a finite list of greedy string substitutions can't?

00:37:38 <kmc> hey elliott do you think i should follow this link to accounts-google-com-id189134acx-ssl-k-emailrenew77.idns.pl and put in my gmail password

00:39:06 <olsner> and emailrenew77 ... if the previous 76 renews got lost, they might give up trying to renew your email any moment

00:54:27 <shachaf> kmc: You can tell it's fake because it doesn't require you to check the "I agree to the Google Terms" checkbox.

00:56:21 <tswett> So guys, you know how there's no computable set of axioms in first-order logic that uniquely determines the natural numbers?

00:59:44 <coppro> shachaf: I prefer wording it as "Every natural number that is not 31 has a successor"

01:00:10 <tswett> Let's define n + 0 as n, and n + (the successor of m) as the successor of (n + m).

01:00:51 <shachaf> tswett: Well, you have to prove that a natural number N isn't 31 before you can say things like "the successor of N"

01:01:04 <shachaf> Just like you have to prove it's not 0 before you can say "the predecessor of N".

01:02:42 <tswett> There exists an operation @ such that for all natural numbers a, b, c, and d, if a @ b = c @ d, then a = c and b = d.

01:06:06 <tswett> 1 is zero, 2 is successors for n != 31, 3 is successors for n = 31, 4 is the predecessor of 0, 5 is that succession is a bijection, and 6 is the @ operation.

01:07:49 <tswett> shachaf: well, yes. How else are we supposed to represent ordered pairs of natural numbers as natural numbers?

01:09:25 <tswett> Consider the natural numbers 0 @ 0, 0 @ 1, 0 @ 2, ..., up through 0 @ 31, as well as 1 @ 0. Assume that 0 @ 0 = 0, 0 @ 1 = 1, 0 @ 2 = 2, ..., up through 0 @ 31 = 31. Then 1 @ 0 can't be any natural number, so we have a contradiction.

01:09:28 <elliott> because tswett does not restrict natural numbers to 0 and successors of natural numbers

01:10:24 <tswett> If we *do* assume that every natural number is either 0 or the successor of a natural number, though, we simply have to go through all 32! permutations there, and we can show that our system is inconsistent.

01:16:07 <Phantom__Hoover> shachaf, supersedes all lesser operating systems and gives you a sensual massage

01:19:23 <tswett> Currently, it's possible to prove that every natural number is equal to 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, or 31.

01:20:18 <tswett> FreeFull: in http://pastie.org/5147243? Given a set of 32 different natural numbers, you can prove that there are no natural numbers different from all of them.

01:22:28 <tswett> Define 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, and 31 as the "standard" natural numbers.

01:22:58 <tswett> Define 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, and 31 as the "standard" Chafian numbers.

01:23:28 <shachaf> The natural numbers are 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 14, 15, 16, 17, 20, 21, 22, 23, 24, 25, 26, 27, 30, 31

01:24:27 <tswett> Well, see. Perhaps there exists a natural number, let's call it i, such that iterating the successor function on i never gets you a standard Chafian number, and iterating the successor function on a standard Chafian number never gets you i.

01:26:42 <tswett> I think we should just call it i. Then we can speak of numbers like i + 5, and i - 480, and so on.

01:28:50 <tswett> It's the set {0, 1, 2, ..., 31} union {i + n where n is an integer}, such that 0 and S are defined in the obvious ways, and then @ is defined just however.

01:29:40 <FreeFull> If there was an axiom stating there were only 32 chafian numbers, then it might be inconsistent

01:30:35 <tswett> Now, this seems to raise a question: what is i + i? I don't think this model admits a consistent definition of addition.

01:38:02 <tswett> But all Chafian numbers corresponding to natural numbers 32 or greater are non-standard.

01:39:30 <tswett> P(32) is clearly not 31. This means that P(32) + 1 = 32. However, 31 + 1 = 32 as well.

01:41:42 <shachaf> 18:23 <shachaf> The natural numbers are 0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 14, 15, 16, 17, 20, 21, 22, 23, 24, 25, 26, 27, 30, 31

01:42:07 <tswett> So, it's impossible for + to satisfy zero-is-identity, commutativity, associativity, compatibility with the successor function, and bijectivity.

01:45:53 <tswett> < tswett> It's the set {0, 1, 2, ..., 31} union {i + n where n is an integer}, such that 0 and S are defined in the obvious ways, and then @ is defined just however.

01:49:11 <tswett> Aren't you contradicting yourself? You said you can't prove that 16 + 16 ≠ 0, but you also said that 16 + 16 is not a standard Chafian number, didn't you?

01:54:10 <tswett> Let 32 = 31 + 1. Suppose 32 ≠ 0; then, by axiom 7, the predecessor of 32, P(32), exists. By axiom 3, P(32) ≠ 31. Therefore, by axiom 14, P(32) + 1 = 32. This means that P(32) + 1 = 31 + 1, so, by axiom 15, P(32) = 31. This is a contradiction.

01:54:50 <FreeFull> tswett: Those axioms don't state what happens when you have something like 3 + 4

01:54:52 <tswett> Axioms 1 through 8 are consistent. You can't prove that there are only 32 natural numbers.

01:57:00 <augur> elliott: if there are (k+2)^2 pairs of numbers, and @ is an endomap on the (k+2) elements of Nat

01:57:09 <tswett> Anyway, I think axioms 1 through 15 are no longer consistent. I think you can prove that i = i + 32, and that i ≠ i + 32.

01:59:52 <tswett> 21:54:10 < tswett> Let 32 = 31 + 1. Suppose 32 ≠ 0; then, by axiom 7, the predecessor of 32, P(32), exists. By axiom 3, P(32) ≠ 31. Therefore, by axiom 14, P(32) + 1 = 32. This means that P(32) + 1 = 31 + 1, so, by axiom 15, P(32) = 31. This is a contradiction.

02:01:57 <tswett> Okay, so, proving that i ≠ i + 32. We know that i + 32 = i + 1 + 1 + ... + 1, where there are 32 1s. Since all of those numbers are undefined, this means that i + 32 is the 32nd successor of i.

02:02:40 <tswett> FreeFull: I said at the beginning, "Let 32 = 31 + 1". I think said "suppose 32 ≠ 0". I then derived a contradiction.

02:06:55 <tswett> Suppose 31 + 1 ≠ 0; then, by axiom 7, the predecessor of 31 + 1, P(31 + 1), exists. By axiom 3, P(31 + 1) ≠ 31. Therefore, by axiom 14, P(31 + 1) + 1 = 31 + 1. This means that P(31 + 1) + 1 = 31 + 1, so, by axiom 15, P(31 + 1) = 31. This is a contradiction.

02:12:52 <FreeFull> tswett: Does this mean that all chafian numbers smaller than 0 or larger than 31 are equal to 0?

02:14:15 <FreeFull> Does one of the axioms imply uniqueness or something like that? This might be used to prove that there are only 32 unique chafian numbers

02:21:30 <coppro> Not all models of the Chafian numbers have 32 elements, if that's what you're asking

02:21:35 <FreeFull> This can be repeated for the value P(i) and the value S(i), extending infinitely in both directions

02:22:07 <tswett> coppro: doesn't axiom 8 imply that there are no finite models of the Chafian numbers?

02:23:10 <tswett> FreeFull: yeah, but you can't consistently have... let me have lambdabot tell you.

02:23:53 <tswett> > "You can't consistently have " ++ concat [show n ++ " < " | n <- [0..31]] ++ "0."

02:25:52 <tswett> FreeFull: wait, no, that's not consistent. Every nonstandard number is the 32nd successor of itself.

02:28:01 <tswett> Because I want them to be presented in a logical order, but I don't want to renumber any of them.

02:30:46 <HackEgo> QuaeroVeritatis: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.)

02:31:34 <HackEgo> shachaf: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.)

02:40:27 <HackEgo> SHACHAF: WELCOME TO THE INTERNATIONAL HUB FOR ESOTERIC PROGRAMMING LANGUAGE DESIGN AND DEPLOYMENT! FOR MORE INFORMATION, CHECK OUT OUR WIKI: HTTP://ESOLANGS.ORG/WIKI/MAIN_PAGE. (FOR THE OTHER KIND OF ESOTERICA, TRY #ESOTERIC ON IRC.DAL.NET.)

02:41:16 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: wELCOME: not found

02:42:45 <FreeFull> tswett: Can you show i = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(i))))))))))))))))))))))))))))))))

02:44:04 <FreeFull> So i is the 32nd successor of itself only if by 32 you mean the chaffian number 31 + 1

02:44:45 <tswett> By "32nd successor", I mean the successor iterated 32 times, where "32" is the ordinary natural number 32.

02:45:57 <tswett> After all, there's no definition of "natural number" in first-order logic that does not also admit things that aren't the natural numbers.

02:46:10 <FreeFull> S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(i))))))))))))))))))))))))))))))))

02:46:32 <tswett> I guess they're perfectly definable in second-order logic, aren't they? But I don't know what the semantics of second-order logic are.

03:14:54 <tswett> You know how there's no computable set of axioms that uniquely defines the natural numbers? And, in particular, the Peano axioms, in first-order logic, admit multiple models?

03:15:12 <tswett> You can kind of define the natural numbers as "the computable model of the Peano axioms".

03:15:56 <elliott> but i hear there's no computable set of axioms that uniquely defines the natural numbers

03:16:17 <tswett> And, in particular, the Peano axioms, in first-order logic, admit multiple models.

03:22:08 <tswett> There exist Booleans x and y such that x ≠ y. There do not exist Booleans x, y and z such that x ≠ y, y ≠ z, and x ≠ z.

03:22:44 <elliott> there exist naturals x and y such that x =/= y. there exist naturals x and y and z such that x =/= y =/= z. there exist ...

03:24:24 <tswett> There do not exist naturals a_0, a_1, ..., a_n such that a_0 ≠ a_1, a_0 ≠ a_2, ..., a_0 ≠ a_n, a_1 ≠ a_2, a_1 ≠ a_3, ..., a_1 ≠ a_n, ... ... ..., a_(n-1) ≠ a_n?

03:26:05 <tswett> Bike: if a computable set of axioms has the natural numbers as a model, then it also has other things as models.

03:28:22 <shachaf> there's no computable set of axioms in first-order logic that uniquely determines the natural numbers

03:42:57 <elliott> `addquote <tswett> But let's ignore the fact that i doesn't exist. Is it even or odd?

03:48:09 <Jafet> Not in the sense that adding it or its negation won't cause the new axioms to be inconsistent

03:51:29 <elliott> Proof: The formal system within which Nelson carries out his proofs requires a theory of syntax. This theory is surely at least as strong as PRA. So:

10:31:54 <Arc_Koen> its only way of branching would be to use lazy evaluation of boolean expressions

10:32:31 <Arc_Koen> (for instance, assuming x always return true, "if (b) {x} else {y}" can be written "(b AND x) OR y")

10:33:01 <Arc_Koen> but this language would do its best to do minimalist; in particular, its only logic gate would be the universal logic gate XOR

11:46:06 <HackEgo> mean: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.)

12:35:14 <FreeFull> When I try to start thunar, I get (thunar:27545): GVFS-RemoteVolumeMonitor-WARNING **: invoking List() failed for type GProxyVolumeMonitorUDisks2: Method `List' returned type `(a(sssbbbbbbbbuasa{ss}sa{sv})a(sssssbbssa{ss}sa{sv})a(sssssbsassa{sv}))', but expected `(a(ssssbbbbbbbbuasa{ss}sa{sv})a(ssssssbbssa{ss}sa{sv})a(ssssssbsassa{sv}))' (g-io-error-quark, 13)

14:40:13 <Arc_Koen> uh, how do I get rid of this horrible scroll bar if my <pre> </pre> is too large?

14:41:17 <Arc_Koen> (that is, how do I tell mediawiki that it should let my browser display a newline if the line is too large for the screen)

14:42:34 <Arc_Koen> of course I could insert newlines my self but that sounds like a bad way to deal with the problem

14:54:31 <atriq> I wonder if I could apply for US citizenship on the basis that my gran was born in California

15:07:25 <Arc_Koen> elliott: if I have a long line in a <pre> block, it all stays in one line, with a horizontal scroll bar to see what's out of the screen

15:46:52 <HackEgo> Hexham is a European town. There are nine people in Hexham, and at least two of them are in this channel. Taneb looks after the ham.

16:22:21 <nooga> IMHO management divisions just learned about his predictions and ordered enginieers to fulfill them

16:31:02 <Jafet> Smaller components get hotter because they have to move more electrons, which makes it harder to move electrons around, which makes it necessary to make the components smaller

16:32:04 <Phantom__Hoover> Don't modern chips generate more power per unit volume than a nuclear reactor?

16:32:42 <Jafet> Well, nuclear reactors can probably generate more if they turned all the safeties off

16:44:48 <Arc_Koen> I thought if you removed the control bars the reaction would chain exponentially

16:45:32 <Phantom__Hoover> They tend to melt through the containment vessel or cause heat-related explosions.

16:46:19 <kmc> the only reason you get so much power out of a nuclear bomb is that you shove all the stuff together at high speed in a very precise way

16:49:38 <Phantom__Hoover> Although a criticality excursion might count as a tiny nuclear explosion? Anyway, not enough to fit into what everyone thinks of as a nuclear explosion.

16:49:49 <kmc> yeah, the manhattan project had originally planned to use a gun-type bomb with plutonium

16:50:06 <kmc> but they couldn't make plutonium pure enough at scale to prevent it from spontaneously fizzling during the detonation process

16:57:07 <Arc_Koen> I honestly have no idea. They usually just link it to some random ship they found, using copper and a lot of tape, and it generates enough power to travel across the galaxy (and sometimes outside)

18:03:22 <Phantom__Hoover> It's run by RBS so doubtless the name will be the most interesting thing about it.

18:05:12 <Phantom__Hoover> <Phantom__Hoover> I have an email notifying me of a "female movable feast".

19:23:35 <zzo38> Do you know what speed the ARMv2a-compatible Amber core can run at? Do you know how to make some of kind of modifications such as hardwiring the cacheable areas and supervisor areas and so on?

19:27:52 <zzo38> I might need to make the computer at first using FPGA, later on it may be replaced with open-source FPGA and/or ASIC components.

19:43:42 <zzo38> Do you like this chess/shogi variants? http://www.chessvariants.org/index/msdisplay.php?itemid=MSkirachesskiras

19:57:38 <zzo38> Arc_Koen: I mean what is sometimes called the "Wazir"; from c3, it can capture on c2, c4, b3, and d3, for example.

19:58:50 <Arc_Koen> from what I understand, you win when both special pieces of your opponents are out

20:00:14 <zzo38> But if you win due to your opponent's L dies from your Kira when they have no Kira, then you win, this is a special win count as double. Same if your L capture opponent's Kira when they have no L, it is win so it count as a double win.

20:03:48 <Arc_Koen> I mean, a win occurs when both L and Kira are dead... but for that, you have to kill one of the two, then the second

20:04:03 <Arc_Koen> and you're saying that when the second dies, if the first was already dead, it's a double-win

20:04:10 <zzo38> Yes, in those cases it is only possible to double win; if the second is captured normally though, then it is a single win.

20:04:21 <kmc> 'Did U know that 1-877-SAF-RAIL dials directly to our Transit Police dispatch center? Put it in ur contacts. #potontrain #crimesinprogress'

20:05:49 <Arc_Koen> so what exactly is the propoer vocabulary? "killing" for the death note, "capturing" for regular chess captures, and "eliminating" when not making the distinction?

20:10:30 <Arc_Koen> if you eliminate your opponent's second special piece using your special power, then it's a double-win

20:28:30 <kmc> '...physics doesn't really need sophisticated stats (unlike biology and medicine) because your data isn't crap. Nobody approves a billion-dollar supercollider because somebody was just slightly able to exclude the null hypothesis at two sigma with a chi-square. People do approve billion-dollar pills that way.'

20:31:12 <kmc> i think in physics you are just expected to get more data until your conclusions are relatively clear

20:33:13 <pikhq> kmc: Well, yes, physics does expect a ton of data. The higgs boson result recently was "5 sigma confirmation of the existence of *a* boson that happens to be consistent with the Higgs boson hypothesis.", no?

20:51:01 <kmc> it sounds like you are emphasizing a distinction between "the higgs boson" and "a boson that happens to be consistent with the higgs boson" and I'm not sure that's a meaningful distinction

20:52:14 <zzo38> I don't think they would be different anyways; if it has the properties of the Higgs boson then it must be the Higgs boson isn't it?

20:53:26 <Phantom__Hoover> If you detected an unknown particle and you only knew it had a charge of -1 it would be consistent with an electron, but it could well be something else.

20:54:41 <pikhq> kmc: I'm saying that the physicists themselves are making that distinction. In the name of being careful.

21:07:29 <kmc> 'What does a $1.6 million explosion sound like? We'll have to ask Fisker Automotive. Sixteen of the luxury carmaker's $100,000 Karma hybrid sports sedans caught fire, blew up and then burned to a crisp after being submerged during Hurricane Sandy. '

21:17:14 <ion> ‘Not a lot of people know this, but the “B” in Benoît B. Mandelbrot’s name stands for “Benoît B. Mandelbrot”.’

21:50:32 <Arc_Koen> (which is not really relevant at all, except very enjoyable for those who were part of the other experiment that got 5.1)

23:57:57 <zzo38> I have had idea before, of a + | ^ operator (these being the C operators), which is allowed only if all are the same result, and its opposite being the - &~ ^ operator.