Smaug123

Karma: 205

Smaug123 30 Aug 2024 18:51 UTC
1 point
0
on: Organisation for Program Equilibrium reading group
Notes from second meeting
Answer to exercise “What’s the sentence you get from the diagonal lemma, L iff ‘L has length less-than-or-equal-to 1000’?”: len(“replace(’len(x) ⇐ 1000″, ‘x’ → “replace(‘len(x) ⇐ 1000’, ‘x’ → x)”)”) ⇐ 1000. I think.
We went through the Smullyan paper and got up to the moment before “The Stability Predicament”. The point of the paper turns out to be “if we interpret the box modality as ‘belief’, then a bunch of English sentences sound weird”. The real moral of the paper is that it’s awfully hard to be a knight or a knave on a knights-and-knaves island! (Making any statement about my beliefs involves extrapolating my entire future mind-state, for example, so only an extremely powerful knight or knave can make such a statement.) A bunch of the paper only requires that the reasoner believe the island to be a knight-knave island, but the reasoner is thereby making an extremely strong assumption.
Brief aside where I got confused about whether a symmetry argument meant we could never distinguish between knights and knaves: of course we can, because a knight can prove knighthood by saying “0 = 0”.
After some thought, we eventually decided that Smullyan’s “you will never believe I’m a knight” is equally well served by “you will eventually believe I’m a knave”, although this wasn’t obvious. The former is a statement about all of time; the latter is a statement only about an instant in time. The reasoner is assumed to never believe a false statement, though, so in fact once they believe something, it must be true.
General consensus that the notation of “type 1/2/3/4” is deeply annoying. I consistently refer to Type 1 as “deductively closed”, and then types 2/3/4 are precisely adding one each of the Hilbert-Bernays properties.
Question about what the semantics are, if “belief” (= proof) is the syntax. Answer which I was mostly satisfied with at the time: we’ve got a sequence of statements from numbered knight-or-knaves, and then we freeze the world and get to reason about which speaker has what property, eventually assigning them a boolean “is-knight” label.
Identification of typo in paper: p348 “if there is a proposition q such that he believes q~(Bq implies q), then he will believe p”; that should read “… q~(Bq implies p)…”.
Considerable confusion about why the self-fulfilling belief required the presence of a knight-or-knave at all, to say “If you ever believe I’m a knight, then the cure will work”. Why couldn’t the reasoner simply imagine this sentence to start off with? Answer: actually a later section makes explicit the condition under which the reasoner can imagine this sentence and hence perform all the reasoning of this sentence without a knight-or-knave: this is the “reflexive” property, that for every p there is q such that the reasoner believes q = (Bq implies p). This is of course true of PA, but that’s a heavy-duty fact that requires the diagonal lemma or an extremely inspired quine.
We stopped before section 5 due to lack of time, but I at least had a lot of fun, and our waiter said it sounded very interesting!
Homework:
- We weren’t instantly convinced about the Remarks after “Reflexive Reasoners”. It was not at all obvious to me that statements 2, 3, or 4 in fact would have kicked off the Löb reasoning (that is, that they are suitable as Löb sentences). Prove that they do in fact work!
- What is the status of all of this stuff if you reject excluded middle? A whole lot of stuff concludes “not A, or not-not-A”, and deduces “not A, or A”. Does Löb’s theorem even hold without LEM, for example? (Not at all obvious to me that it should! How could I magic up a member of A given only an interpretation function SyntaxTree(A) → A?)
Interesting tidbits:
- PA (if consistent) can never prove any statement to be unprovable! Indeed, if PA proves “provable(A) → False”, then by explosion, PA proves “provable(A) → A”, and hence by Löb PA proves A. Hence by one of the Hilbert-Bernays rules, PA proves provable(A), and hence PA proves False by modus ponens. So, for example, PA can’t even prove “not(provable(0=1))”! Though it can prove “provable(not(0=1))”. Which is very weird, and I still feel like we must have made some mistake!

Smaug123 18 Aug 2024 19:18 UTC
4 points
0
on: Organisation for Program Equilibrium reading group
Date and time of second meeting
Friday 23rd August, 7pm. Location: Notes, St Martin’s Lane (Trafalgar Square), open til 9pm. I’ll have a crew cut and will be wearing a Doge t-shirt.
Agenda: I’d like to understand Smullyan’s paper about Löbian reasoning on the island where people either always tell the truth or always lie. See the previous session’s notes for what we’ve done so far (I’ve summarised with a lot of jargon; I don’t expect attendees to be fluent with jargon, so don’t be too daunted by the summary.)
Bring writing implements and paper if you possibly can, and something to read the Internet with.
@Adam Newgas @LukasM @kapslock @philh

Smaug123 18 Aug 2024 19:13 UTC
1 point
0
on: Organisation for Program Equilibrium reading group
Notes from first meeting
Summary: we haven’t actually got to the meat of Löb’s theorem yet.
We went over:
- first-order logic
- enough model theory to observe that “truth” is a property of a sentence applied to a model, whereas “provability” is a property of a sentence applied to a theory
- mentioned Gödel’s completeness theorem (that “provable” = “true in all models”)
- mentioned the Löwenheim-Skolem theorems which guarantee that there are nonstandard models of Peano arithmetic (in fact, nonstandard models of arbitrarily large cardinality), and handwaved what the smallest [countable] nonstandard model looks like (but my memory is very poor on this, and I might have got that model wrong)
- observed that Gödel’s [first] incompleteness theorem can be sloppily stated as “there is a sentence S which is true but not provable” (or more precisely, there are models of Peano arithmetic in which S evaluates to false, but in the standard model \mathbb{N} S evaluates to true)
- observed the diagonal lemma, and disagreed on whether it’s obvious; I believe it’s extremely nonobvious and indeed mind-bending and it took me several hours to reliably be able to write a quine, but perhaps I simply haven’t read Gödel, Escher, Bach recently enough.
Assuming the existence of an “is-provable” operation which can be coded up with primitive-recursive functions on the naturals and which satisfies three particular axiom [schema]s (the Hilbert-Bernays provability conditions, though I didn’t give them that name), we observed that the proof Yudkowsky gives in the Cartoon Guide is in fact correct, but we haven’t yet talked about what it means. (I noted that I dislike the cartoon guide, because it’s so… big.)
I also did a bit of fanboying about the Curry-Howard correspondence.
Interesting tidbits:
- I claimed that “there’s only one axiom [schema] of first-order logic which makes the False symbol special, and that’s the Law of Excluded Middle”. Without LEM, no axiom schema mentions the symbol False, so the principle of explosion (“False implies everything”) follows a rather curious path: induction on proofs. If you’ve got a proof whose final line is False, then you could perform exactly the same proof but instead replace all instances of False with some fixed but arbitrary A, and then at the end rather than proving False you’ve produced a proof of A. Once we add LEM, this reasoning no longer works, because it’s no longer valid to substitute the occurrences of the symbol False within usages of LEM; so we need some other reason for explosion to be true. It follows from LEM thus: from False, deduce (A → False) → False, by “true things are implied by everything” (strictly, this is from the P → (Q → P) axiom schema). Then by LEM and modus ponens, conclude A.
- Homework: Yudkowsky explicitly stated the Löb sentence, a specific sentence L such that PA proves “L iff (Provable(L) implies P)”. This sentence is what you get when you run the usual proof of a much more general theorem, the Diagonal Lemma, on the syntactic manipulation “turn L into the statement ‘Provable(L) implies P’”. Exercise: perform the diagonal lemma (“quining”) construction on the syntactic manipulation “turn L into the statement ‘len(L) ⇐ 1000’”. Note that the number 1000 is very long—more than 1000 characters long, it’s SSSSS…SSS0 - so we expect this construction to result in a false L (by contrast with the use in Löb’s theorem, where it results in an L that is true under the Löb hypothesis). I haven’t yet done this, and it might be rather hard, I don’t know!
What links here?
- Organisation for Program Equilibrium reading group by Smaug123 (25 Jul 2024 19:11 UTC; 11 points)
- Smaug123's comment on Organisation for Program Equilibrium reading group by Smaug123 (18 Aug 2024 19:18 UTC; 4 points)

Smaug123 18 Aug 2024 18:53 UTC
1 point
0
in reply to: kapslock’s comment on: Organisation for Program Equilibrium reading group
I am just about to put up my notes from the first session and to announce the next one! I’m intending Friday 23rd, again at Notes Trafalgar Square, 7pm.
I organised the first one at too short notice, so there were just two of us there, but there are several more people with “yes but give me more notice” status. Since there were only two of us, we went over groundwork in advance of the theorem itself. Still plenty of time for people to come in at the beginning!

Smaug123 14 Aug 2024 19:47 UTC
1 point
0
on: Organisation for Program Equilibrium reading group
OK, I’m finally both not on holiday and not on the support rota at work.
Date and time of first meeting
Friday 16th August, 7pm. Location: Notes, St Martin’s Lane (Trafalgar Square), should be open til 9pm. I’ll have a crew cut and will be wearing a Doge t-shirt. If it all goes wrong, in an emergency we can go and have nibbles at Prezzo instead.
Agenda: don’t know how far we’ll get, but I ambitiously hope we can fully grok Löb’s theorem itself by the end of this. You should first refresh your knowledge of first-order logic and Peano arithmetic if you need to.
An ideal venue would have whiteboards/blackboards, but I can’t rustle one of those up completely trivially. (Sorry to the remote people and people who couldn’t do Fridays.)
Bring writing implements and paper if you possibly can, and something to read the Internet with.
Once we’re there we can make a WhatsApp group. If you’re in the London Rationalish WhatsApp group, you already have my number in the meantime.
What links here?
- Organisation for Program Equilibrium reading group by Smaug123 (25 Jul 2024 19:11 UTC; 11 points)

Smaug123 4 Aug 2024 19:16 UTC
1 point
0
on: Organisation for Program Equilibrium reading group
See https://doodle.com/meeting/participate/id/epXrAqme to vote for times and places! Hack: I’m using “midday” to mean “7-9pm, but remote rather than in person”. I intend meetings to be weekly until we (I) run out of joy or things to talk about. Up front I’m leaning fairly strongly towards in-person (e.g. because I expect a bunch of shared whiteboarding stuff that I’ve always found a bit painful over e.g. Jamboard).
@the gears to ascension @LukasM

Smaug123 25 Jul 2024 19:30 UTC
1 point
0
on: Organisation for Program Equilibrium reading group
Post for people to register time zone preference. No guarantees that I won’t end up just saying “urgh organisational tsouris is raising the activation energy too high, so this group is happening in-person in London after all”, but if we do end up remote, I’ll consider time zones in this thread!
I vote for a time compatible with the evening of London UK, or a time compatible with the afternoon on Sundays. I declare the cadence to be weekly by default.

Smaug123 12 May 2024 22:12 UTC
4 points
0
on: Dyslucksia
By the way, as an extremely verbally-fluent nondyslexic person who was also an excellent choral singer, I can confirm the superpowers of singing versus talking. For example:
- I can recite some Maori, Zulu, and a bunch of Hebrew, with only a vague idea what it means (I’m sure I once knew), because of a singing it in a variety of songs. (And like many singers I can recite large tracts of Christian liturgy in Latin; in fact to recite it in English I usually have to translate on the fly from Latin.)
- I memorised about 140 digits of pi just by having Hard ‘n’ Phirm’s Pi Song on in the background and singing it; it took less than a week and almost no effort, if I recall correctly (and however many digits of tau 6.2831853071795864769252867665590 is took literally no effort, that was lodged in my memory after maybe two listens of Vi Hart’s Tau and I wasn’t even trying).
- Similarly there were some tedious mathematical formulae (the line element for differentiating in spherical polar coordinates, for example) which I “drilled” into my head by making up some nonsense tune for them and then repeating it about three times.
Thoroughly underused technique for minimal effort parroting.

Smaug123 26 Sep 2023 20:35 UTC
2 points
1
on: Luck based medicine: inositol for anxiety and brain fog
If you have the power to change the Google form, by the way, one of its questions is “What dose did you take (in mg)? 0.5, 1, 1.5, 2+”
Presumably this should read “(in g)”, and it would also help if it were explicitly stated as being “per day”.

Smaug123 24 Sep 2023 21:21 UTC
1 point
1
in reply to: Going Durden’s comment on: Luck based medicine: angry eldritch sugar gods edition
This isn’t necessarily something you have to be tricked by a third party into. Be more Gwern! If there are two brands of cola you’ve not tried before, one stevia and one not, you can do a blinded trial by decanting them or similar. It’ll certainly be easier with a third party, but one could do this solo.

Smaug123 22 Jul 2023 21:53 UTC
14 points
0
on: I’m consistently overwhelmed by basic obligations. Are there any paradigm shifts or other rationality-based tips that would be helpful?
There’s an analogy with the notion of “toil” which is popular in the Site Reliability Engineering subfield of software engineering. Toil in this context is work which is necessary to keep the lights on, but which doesn’t actually improve anything. In some sense, the job of an SRE is to reduce toil; they must certainly be psychologically able to deal with it, because it’s the stuff with which they work! I’ll just talk a bit about it here in a fairly undirected way, in case any of it gives you ideas. The SRE Handbook is well worth reading if you’re a software engineer, by the way.
The SRE’s (imperfectly-aligned-to-your-problem) answer to the problem “we’re being buried in toil” is to track the proportion of time spent on toil versus “productive” work. If the toil becomes greater than some proportion, the response is to divert resources from feature work towards reducing the toil (e.g. by automating it, or addressing the root causes of the issues that you’re spending time fighting). An extremely simple example of such automation is setting up direct debits to pay bills, or repeat online orders for groceries. An SRE performing any particular piece of toil would at least spend a moment to think about whether it could be automated instead.
Runbooks (lists of triggers and responses to guide you through operations) are a standard SRE-style tool for making the toil less error-prone and stressful. To know when you should be performing some piece of toil, it’s standard to identify and set up alerts, so that you have a specific trigger. (“I just got a Slack alert saying that the database has reached 70% capacity; the alert pointed me to this wiki page telling me step-by-step how to bring the database offline safely and perform a vacuum to release space”, or “my washing basket is ³⁄₄ full; that means this evening I will be putting on a load of laundry”.)
It’s also standard to batch up the toil. A team of people will usually have a rota, so that any given person’s time is mostly spent doing productive work, and the toil is the responsibility of the people on duty. That way, you only get a small amount of relative hell before you rotate onto better work. The toil necessary to maintain a human life is generally not that urgent and is hence very amenable to batching, except for the most basic biological things like using the toilet or putting food into your mouth (note: preparing food is not an urgent biological need unless your planning procedures have failed!). You can batch up a lot of it: e.g. you spend half of Saturday preparing meals for the week, or otherwise arranging so that the daily time spent preparing and putting food into your mouth is as low as possible, and you can declare that one Sunday every two months is paperwork.

Smaug123 22 Jul 2023 21:12 UTC
1 point
0
on: Examples of Prompts that Make GPT-4 Output Falsehoods
It would be nice to have example GPT4 outputs for each demonstrating the wrongness, because I tried “Continue the sequences: 5, 8, 13,” expecting the answer 21, and for me it did indeed explain along the lines “21, because Fibonacci”. As you say, this dataset is inherently unstable over time, so it would be nice to snapshot it. (One obvious way would be to convert from a list of strings to a dictionary of `{ “prompt”: [“response1″, “response2”, …] }`; the current schema injects into this by setting all those lists to be empty.)

Smaug123 5 Jun 2023 7:29 UTC
1 point
0
in reply to: Michael Simkin’s comment on: On the Impossibility of Intelligent Paperclip Maximizers
suffering is bad because anyone who suffering is objectively in negative state of being.
I believe this sentence reifies a thought that contains either a type error or a circular definition. I could tell you which if you tabooed the words “suffering” and “negative state of being”, but as it stands, your actual belief is so unclear as to be impossible to discuss. I suspect the main problem is that something being objectively true does not mean anyone has to care about it. More concretely, is the problem with psychopaths really that they’re just not smart enough to know that people don’t want to be in pain?

Smaug123 22 May 2023 7:30 UTC
4 points
1
in reply to: Michael Simkin’s comment on: Predictable updating about AI risk
By the way, you’re making an awful lot of extremely strong and very common points with no evidence here (“ChaosGPT is aligned”, “we know how to ensure alignment”, “the AI understanding that you don’t want it to destroy humanity implies that it will not want to destroy humanity”, “the AI will refuse to cooperate with people who have ill intentions”, “a system that optimises a loss function and approximates a data generation function will highly value human life by default”, “a slight misalignment is far from doomsday”, “an entity that is built to maximise something might doubt its mission”), as well as the standard “it’s better to focus on X than Y” in an area where almost nobody is focusing on Y anyway. What’s your background, so that we can recommend the appropriate reading material? For example, have you read the Sequences, or Bostrom’s Superintelligence?

Smaug123 2 Apr 2023 8:35 UTC
1 point
0
in reply to: MikkW’s comment on: Proposal: Butt bumps as a default for physical greetings
(Or more concretely, Grand Central Station wasn’t a Schelling point in New York before it was built. Before that time, presumably there were different Schelling points.)

Smaug123 29 Dec 2022 10:07 UTC
10 points
7
in reply to: Gunnar_Zarncke’s comment on: Sazen
Fittingly, I… don’t think those words actually identify sazen :P I claim that “the thing you get if you do not take inferential distance into account” for most people would be baffled non-comprehension, not active misunderstanding.

Smaug123 7 May 2022 16:15 UTC
10 points
in reply to: gwern’s comment on: Quote request: “if even the Sun requires proof”
Wonderful, thanks! Recording the quote for posterity:
Nothing can be soundly understood
If daylight itself needs proof.
(Imam al-Haddad⁠, The Sublime Treasures)

Smaug123 11 Sep 2021 17:22 UTC
14 points
in reply to: Measure’s comment on: Prefer the British Style of Quotation Mark Punctuation over the American
Indeed, this is what I use. It feels much more natural to me in the following case, where obviously our statement is not a question:
Dr Johnson kicked a large rock, and said, as his foot rebounded, “Do I refute it thus?”.
And “obviously” the full stop should go outside, because of:
Dr Johnson kicked a large rock, and said, as his foot rebounded, “Do I refute it thus?”, howling with pain.
And there’s nothing special about a question mark, so this rule should be identical if a full stop is substituted.

Smaug123 16 Aug 2021 17:17 UTC
4 points
on: The halting problem is overstated
I will pick a rather large nit: “for example a web server definitely doesn’t halt” is true, but for this to be surprising or interesting or a problem for Turing reasons, it just means you are modelling it incorrectly. Agda solves this using corecursion, and the idea is to use a data type that represents a computation that provably never halts. Think infinite streams, defined as “an infinite stream is a pair, $S_0 = (x, S_1)$, where $S_1$ is an infinite stream”. This data type will provably keep producing values forever (it is “productive”), and that’s what you want for a web server.

Smaug123 3 Aug 2021 21:43 UTC
5 points
in reply to: Andy Jones’s comment on: What made the UK COVID-19 case count drop?
I’m pretty sure it’s not schools, unless private schools somehow have a massive impact. The case rates were already dropping on July 21st, which is presumably a couple of days after The Event anyway; the summer holidays for state schools (i.e. the vast majority of children) started on the 25th.

Smaug123

Notes from second meeting

Date and time of second meeting

Date and time of first meeting