Kutta

Yes. To expand a bit, in fact the straightforward way to show that second-order arithmetic isn't complete in the first sense is by using the Gödel sentence G.

G says via an encoding that G is not provable in second-order arithmetic. Since the only model (up to isomorphism) is the model with the standard natural numbers, an internal statement which talks about encoded proofs is interpreted in the semantics as a statement which talks about actual proof objects of second-order arithmetic. This is in contrast to first-order arithmetic where we can interpret an ... (read more)

I'd like to ask a not-too-closely related question, if you don't mind.

A Curry-Howard analogue of Gödel's Second Incompleteness Theorem is the statement "no total language can embed its own interpreter"; see the classic post by Conor McBride. But Conor also says (and it's quite obviously true), that total languages can still embed their coinductive interpreters, for example one that returns in the partiality monad.

So, my question is: what is the logical interpretation of a coinductive self-interpreter? I feel I'm not well-versed enough in mathem... (read more)

You're right, I mixed it up. Edited the comment.

Suppose "mathemathics would never prove a contradiction". We can write it out as ¬Provable(⊥). This is logically equivalent to Provable(⊥) → ⊥, and it also implies Provable(Provable(⊥) → ⊥) by the rules of provability. But Löb's theorem expresses ∀ A (Provable(Provable(A) → A) → Provable(A)), which we can instantiate to Provable(Provable(⊥) → ⊥)→ Provable(⊥), and now we can apply modus ponens and our assumption to get a Provable(⊥).

To clarify my point, I meant that Solomonoff induction can justify caring less about some agents (and I'm largely aware of the scheme you described), but simultaneously rejecting Solomonoff and caring less about agents running on more complex physics is not justified.

The unsimulated life is not worth living.

-- Socrates.

You conflate two very different things here, as I see.

First, there are the preferences for simpler physical laws or simpler mathematical constructions. I don't doubt that they are real amongst humans; after all, there is an evolutionary advantage to using simpler models ceteris paribus since they are easier to memorize and easier to reason about. Such evolved preferences probably contribute to a matemathician's sense of elegance.

Second, there are preferences about the concrete evolutionarily relevant environment and the relevant agents in it. Naturally, t... (read more)

Donated $500.

Survey taken.

Very recently decent fansubs have surfaced for Mamoru Hosoda's new movie The Wolf Children Ame and Yuki. I wholeheartedly recommend it.

I figured that ~36% discount over two months would be way too high.

Thanks for your effort. I'll contact my bank.

I donated 250$.

Update: No, I apparently did not. For some reason the transfer from Google Checkout got rejected, and now PayPal too. Does anyone have an idea what might've gone wrong? I've a Hungarian bank account. My previous SI donations were fine, even with the same credit card if I recall correctly, and I'm sure that my card is still prefectly valid.

Took all of them.

Luminosity, Radiance and Flashes by Alicorn.

What do you mean by real depth? In cinema, isn't skilled cinematography included in that? If I recall correctly, I've read from you somewhere that you think most of NGE's narrative/mythological background is an impromptu, leaky mess (which I mostly agree with), so you might mean that by lack of real depth, but that doesn't subtract much from NGE's overall success at thematic exposition, so I'm still not fully getting it.

Typo: Arrison.

Seconded all three. The health impact of the quality of a particular foodstuff (within the variance allowed by developed country regulations) is often overstated compared to the health impact of the overall composition of the calories you eat.

I first encountered this idea on Terence Tao's excellent slide.