trentmkelly/LessWrong-43k huggingface dataset:
Fixed point theorem in the finite and infinite case
by Vika — 2015-07-06T01:42:56.000Z

Janos and I started working on extending the fixed point theorem to the infinite case at MIRI's June decision theory workshop with Patrick and Benja. This post attempts to exhibit the finite version of the theorem and speculates about a plausible extension.

Algorithm for the finite case

Suppose we're given variables p1,…,pn, and statements pi↔ϕi(p1,…,pn) where each ϕi is fully modalized (no variables occur outside modal subformulas). We will describe an algorithm for constructing sentences ψi with no free variables, such that the original statements are equivalent to p1↔ψ1,…,pn↔ψn.

For simplification purposes, we will assume that each ϕi is only singly modalized (none of the modal subformulas contain further modal subformulas). If not, we can introduce new variables for each subformula of the form □ϕi,j that occurs in a fully modalized context.

Now consider a sequence of theories W0,W1,…, where Wi≡PA∪{□i+1⊥,¬□i⊥}.

In W0, it's easy to determine the truth value of each pi: every modal subformula can be replaced with ⊤, leaving a propositional formula with no variables.

Now suppose we've done this for W0,…,Wn−1. Then, a statement □ϕ will be true in Wn iff

PA⊢(□n+1⊥∧¬□n⊥)→□ϕ⇔□n⊥∨□(□n⊥→ϕ)⇔□n⊥∨□n−1⋀i=0((□i+1⊥∧¬□i⊥)→ϕ)

Therefore □ϕ will be true in Wn iff ϕ is true in W0,…,Wn−1; this will let us evaluate the truth value of pi in all of the theories W1,…,Wn.

It's clearly the case that every modal subformula will have truth value stabilizing, therefore every pi will also. So there is an N such that Wn has the same truth values as WN for n>N. Now if WN⊢pi, construct ψi≡¬⋁i:Wi⊢¬pi(□i+1⊥∧¬□i⊥); otherwise construct ψi≡⋁i:Wi⊢pi(□i+1⊥∧¬□i⊥). These are variable-free formulas.

Infinite case example: Procrastination Bot

def ProcrastinationBotN(X):

if PA+N⊢□X(PBN+1)=C:

return C

else: return D

Constructing the fixed point

Let pij denote whether PBi cooperates with PBj. Then
pij↔□ipj,i+1=□i□jpi+1,j+1
where □i stands for ¬□i⊥→□ (e.g. □0=□).

Then the following statements hold
p00↔□□p11
p11↔□1□1p22≡¬□⊥→□(¬□⊥→□p22)
…

In W0, any statement with a box in front of it is true, so any statement where a boxed statement is implied is also true. Thus, all the relevant statements are true in W0:

Theory
p00
□□p11
p11
¬□⊥→□(¬□⊥→□p22)
¬□⊥→□p22
p22
…

W0

⊤

⊤
⊤

In Wi+1, all the implied statements are boxed statements that were true in Wi, e.g. □p22 or ¬□⊥→□p22. Thus, all the relevan

...
There is no such thing as strength: a parody
by ZoltanBerrigomo — 2015-07-05T23:44:34.228Z

The concept of strength is ubiquitous in our culture. It is commonplace to hear one person described as "stronger" or "weaker" than another. And yet the notion of strength is a a pernicious myth which reinforces many our social ills and should be abandoned wholesale.

1. Just what is strength, exactly? Few of the people who use the word can provide an exact definition.

On first try, many people would say that strength is the ability to lift heavy objects. But this completely ignores the strength necessary to push or pull on objects; to run long distances without exhausting oneself; to throw objects with great speed; to balance oneself on a tightrope, and so forth.

When this is pointed out, people often try to incorporate all of these aspects into the definition of strength, with a result that is long, unwieldy, ad-hoc, and still missing some acts commonly considered to be manifestations of strength.

Attempts to solve the problem by referring to the supposed cause of strength -- for example, by saying that strength is just a measure of muscle mass -- do not help. A person with a large amount of muscle mass may be quite weak on any of the conventional measures of strength if, for example, they cannot lift objects due to injuries or illness.

2. The concept of strength has an ugly history. Indeed, strength is implicated in both sexism and racism. Women have long been held to be the "weaker sex," consequently needing protection from the "stronger" males, resulting in centuries of structural oppression. Myths about racialist differences in strength have informed pernicious stereotypes and buttressed inequality.

3. There is no consistent way of grouping people into strong and weak. Indeed, what are we to make of the fact that some people are good at running but bad at lifting and vice versa?

One might think that we can talk about different strengths - the strength in one's arms and one's legs for example. But what, then, should we make of the person who is good at arm-wrestling but poor at lifting? Arms can move in many ways; what will we make of someone who can move arms one way with great force, but not another? It is not hard to see that potential concepts such as "arm strength" or "leg strength" are problematic as well.

4. When people are grouped into strong and weak accordin...
Shifting guilt
by So8res — 2015-07-05T03:00:00.000Z
Link: https://mindingourway.com/shifting-guilt/

The posts so far have been less about confronting guilt, and more about different tools for shifting it. This is a valuable skill to generalize.

The posts in this series have developed three such tools for shifting guilt. In this post, I'll recast those three tools as members of the same family, so that you can start to see the pattern, and develop similar tools from the same family as you need them.

The tools that I have described so far shift guilt to one particular place: guilt about being unable to act as you desire. This is intentional — that is the one place that I know how to confront guilt head-on.

The first tool for shifting guilt is the tool of refinement. This tool is used on listless guilts in need of pointing.

Imagine finding yourself feeling vaguely guilty the morning after a party, having slept in longer than you intended, your head aching from a slight hangover. Imagine a vague guilt making your body feel heavier. Perhaps it whispers that the night was senseless. Perhaps it murmurs that you're wasting your life away. This is the sort of guilt that's amenable to refinement: ask the guilt what, precisely, it would have had you do instead of what you did. (It is important, when refining, to also possess the virtue of concreteness: do not settle for "I should have been studying." Demand a specific action: Which book? Which chapter?)

Sometimes, when asking the guilt what you could have done instead, you will remember that none of the alternatives were compelling. Maybe the party was for an old friend who you only see once every few years, and fulfilling the social obligation was better than the alternative. Maybe you were exhausted from a day of studying, low on human contact, and needed the party to reinvigorate you. When using the tool of refinement, the guilt sometimes simply disappears.

But often, the guilt gets more pointed. Perhaps you conclude you should have been working overtime so you could donate the money to a worthy cause. Perhaps you conclude that you had the opportunity and the stamina, but simply not the willpower. This is good! This is a success! The refinement has succeeded, and the guilt has come into more focus.

But more often than not, when you succeed at refining guilt, you find yourself left with an obligation ("I should have drank less" or "I should have studied" or "I should have worked overtime.") This has not yet shifted enough...
A Year of Spaced Repetition Software in the Classroom
by tanagrabeast — 2015-07-04T22:30:16.207Z

Last year, I asked LW for some advice about spaced repetition software (SRS) that might be useful to me as a high school teacher. With said advice came a request to write a follow-up after I had accumulated some experience using SRS in the classroom. This is my report.

Please note that this was not a scientific experiment to determine whether SRS "works." Prior studies are already pretty convincing on this point and I couldn't think of a practical way to run a control group or "blind" myself. What follows is more of an informal debriefing for how I used SRS during the 2014-15 school year, my insights for others who might want to try it, and how the experience is changing how I teach.

Summary

SRS can raise student achievement even with students who won't use the software on their own, and even with frequent disruptions to the study schedule. Gains are most apparent with the already high-performing students, but are also meaningful for the lowest students. Deliberate efforts are needed to get student buy-in, and getting the most out of SRS may require changes in course design.

The software

After looking into various programs, including the game-like Memrise, and even writing my own simple SRS, I ultimately went with Anki for its multi-platform availability, cloud sync, and ease-of-use. I also wanted a program that could act as an impromptu catch-all bin for the 2,000+ cards I would be producing on the fly throughout the year. (Memrise, in contrast, really needs clearly defined units packaged in advance).

The students

I teach 9th and 10th grade English at an above-average suburban American public high school in a below-average state. Mine are the lower "required level" students at a school with high enrollment in honors and Advanced Placement classes. Generally speaking, this means my students are mostly not self-motivated, are only very weakly motivated by grades, and will not do anything school-related outside of class no matter how much it would be in their interest to do so. There are, of course, plenty of exceptions, and my students span an extremely wide range of ability and apathy levels.

The procedure

First, what I did not do. I did not make Anki decks, assign them to my students to study independently, and then quiz them on the content. With honors classes I taught in previous years I think that might have worked, but I know my current students too well...
Meetup : Frankfurt Meet-Up
by Aharon — 2015-07-04T16:45:48.383Z

Discussion article for the meetup : Frankfurt Meet-Up

WHEN:
16 July 2015 06:30:00PM (+0200)

WHERE:
Frankfurt Praunheim, exact address available

Hi!

I'm posting on behalf of Janko (see below)

Contact: Tel:0176 3066 164 (Janko)

less-wrong-frankfurt@googlegroups.com

The meetup takes place in the apartment of the Frankfurt lesswrong core group. The exact adress can be found in our google group or by calling me.

After a long period without meetups and some discussions later we decided to start again and do it biweekly.

We decided to focus more on the core ideas of lesswrong by going through Eliezer's book Rationality: From AI to Zombies

What do we mean by rationality (finished)

Feeling rational (finished)

Why truth (finished)

What's a bias again (planned)

Availability (planned)

Burdensome Details (planned)

Planning fallacy (planned)

(more to come in future meetups)

The chapters will be an open discussion rather than a presentaion. I encourage you to have a look at a few of the linked posts beforehand. :-) Other topics are:

short summaries of interesting books anyone of us had read

Some games like Zendo)

hope to see you

Janko

Discussion article for the meetup : Frankfurt Meet-Up
Optimal predictors and propositional calculus
by Vanessa Kosoy — 2015-07-04T09:51:38.000Z

This is a writeup of the stuff Benja and I thought up during the logical uncertainty workshop in May.

An optimal predictor for (D,μ) allows assigning probabilities to logical sentences of the form x∈D but in general it doesn't allow assigning probabilities to propositional formulae constructed from sentences of that form. Here we outline two approaches to defining such probabilities.

Consider D a language. Define BD⊆{0,1}∗ to be the set of words encoding propositional formulae whose variables are labeled by elements of {0,1}∗ such that the formula evaluates to truth if a variable labeled by x is substituted for the truth value of x∈D. We can think of BD as consisting of expressions like ⌈0110∈D⌉∧¬⌈101∈D⌉ which represent true sentences.

Consider μ a word ensemble and suppose P is an optimal predictor for (D,μ). It would be nice to show P satisfies something like the "coherence condition"

Pk(ϕ)=Pk(ϕ∧ψ)+P(ϕ∧¬ψ)

Obviously we cannot expect the exact equality since P is only defined up to similarity relative to μ. Instead, we were able to show that under certain assumptions on μ, we have that (Pk(ϕ)−Pk(ϕ∧ψ)−P(ϕ∧¬ψ))2 is "negligible on average" in some sense.

To see this define the languages

D+={(ϕ,ψ)∣ϕ∧ψ∈BD}
D−={(ϕ,ψ)∣ϕ∧¬ψ∈BD}
D0={(ϕ,ψ)∣ϕ∈BD}

All three languages have reductions to BD:

f+(ϕ,ψ):=ϕ∧ψ
f−(ϕ,ψ):=ϕ∧¬ψ
f0(ϕ,ψ):=ϕ

Assume a word ensemble ν exists s.t. f+, f− and f0 are pseudo-invertible reductions of (D+,ν), (D−,ν) and (D0,ν) to (BD,μ). Then by Theorem 6.1 of [1], f−1+(P) is an optimal predictor for (D+,ν), f−1−(P) is an optimal predictor for (D−,ν) and f−10(P) is an optimal predictor for (D0,ν). Since D0=D+⊔D−, Theorems 5.1 and 4.2 imply that f−10(P)ν∼f−1+(P)+f−1−(P). That is, Eνk[(Pk(ϕ)−Pk(ϕ∧ψ)−P(ϕ∧¬ψ))2] is negligible.

Another approach is considering a language D equipped with a binary operation m:{0,1}∗×{0,1}∗→{0,1}∗ such that χD(m(x,y))=χD(x)χD(y). If μ is a word ensemble and P is an optimal predictor for (D,μ) then Pk(m(x,y)) can be interpreted as the probability of ⌈x∈D⌉∧⌈y∈D⌉. The probability of ⌈x∈D⌉∧¬⌈y∈D⌉ can be taken to be η(Pk(m(x,y))−Pk(y)). Continuing in this manner, it is possible to assign probabilities to all propositional formulae of the sort.

In this case, the coherence condition would hold automatically except for the presence of η. Define

D+={(x,y)∣m(x,y)∈D}
D0={(x,y)∣x∈D}

We can now apply the same method as above combined with Lemma 4.3 (D+⊆D0) to

...
Meetup : LessWrong Scotland
by cjb230 — 2015-07-03T22:47:51.375Z

Discussion article for the meetup : LessWrong Scotland

WHEN:
12 July 2015 02:00:00PM (+0100)

WHERE:
Glasgow: Caffe Nero, Dundas Avenue, at 2pm, then Waxy O'Connor's on West George Street from 3:30 pm

This time we'll be talking about section D ("Mysterious Answers") of the rationality book, plus trying a slightly different format!

As usual, please pass this on to anyone who might be interested.

===========

This post is effectively a mirror. The definitive version is here:

https://www.facebook.com/events/1444230005884572/

Discussion article for the meetup : LessWrong Scotland
The Pre-Historical Fallacy
by Tem42 — 2015-07-03T20:21:31.696Z

One fallacy that I see frequently in works of popular science -- and also here on LessWrong -- is the belief that we have strong evidence of the way things were in pre-history, particularly when one is giving evidence that we can explain various aspects of our culture, psychology, or personal experience because we evolved in a certain way. Moreover, it is held implicit that because we have this 'strong evidence', it must be relevant to the topic at hand. While it is true that the environment did effect our evolution and thus the way we are today, evolution and anthropology of pre-historic societies is emphasized to a much greater extent than rational thought would indicate is appropriate.

As a matter of course, you should remember these points whenever you hear a claim about prehistory:

Most of what we know (or guess) is based on less data than you would expect, and the publish or perish mentality is alive and well in the field of anthropology.

Most of the information is limited and technical, which means that anyone writing for a popular audience will have strong motivation to generalize and simplify.

It has been found time and time again that for any statement that we can make about human culture and behavior that there is (or was) a society somewhere that will serve as a counterexample.

Very rarely do anthropologists or members of related fields have finely tuned critical thinking skills or a strong background on the philosophy of science, and are highly motivated to come up with interpretations of results that match their previous theories and expectations.

Results that you should have reasonable levels of confidence in should be framed in generalities, not absolutes. E.g., "The great majority of human cultures that we have observed have distinct and strong religious traditions", and not "humans evolved to have religion". It may be true that we have areas in our brain that evolved not only 'consistent with holding religion', but actually evolved 'specifically for the purpose of experiencing religion'... but it would be very hard to prove this second statement, and anyone who makes it should be highly suspect.

Perhaps more importantly, these statements are almost always a red herring. It may make you feel better that humans evolved to be violent, to fit in with the tribe, to eat meat, to be spiritual, to die at the age of thi...
Vingean Reflection: Open Problems
by abramdemski — 2015-07-03T18:44:30.000Z

Edit: None of the ideas here should be attributed to me; they all came out of discussions at the workshop or were pre-existing. I've just done a little bit of interpretation and (in some cases) naming.

The summer MIRI workshop on Vingean reflection has drawn to a close, and I think the highest-value thing for me to communicate from it is my sense of what the open problems are. The existing solutions to Vingean uncertainty are by no means satisfactory, but nonetheless, they solve the example problems which are currently on the table (namely, the Löbian obstacle and the procrastination paradox). This state of affairs makes it more difficult than it needs to be to see what is wrong with solutions so far. Based on a discussion with Eliezer, and a table of solutions and their properties which Patrick wrote out, I'll try to discuss the boundary where progress can be made.

Existing Problems/Solutions

A Vingean agent is defined as one which can choose actions without entirely planning what actions it will take in the future. This seems like a necessary condition for a boundedly rational agent. Contrast this with boundlessly rational procedures such as backward induction which must determine plan for all contingencies at time t+1 before it is able to decide what to do at time t, because it's not possible to choose between actions when the expected utility (under the assumption of acting rationally after that point) is not yet computed. Vingean uncertainty is, therefore, a large departure from standard utility theory and game theory.

The Löbian obstacle is, informally, the observation that an agent cannot trust itself generally, thanks to Löb's theorem, and therefore cannot trust its future self to achieve goals. More formally: Löb's theorem implies that trust of its own soundness over any class of sentences entails provability of those sentences. It therefore seems impossible for an agent to trust future selves to prove actions "safe" (for some formal safety predicate) without predicting specifically what action will be taken. A more formal specification of the obstacle is given in the tiling agents paper.

Solutions to the Löbian obstacle include Marcello's Waterfall and Model Polymorphism (previously called Parametric Polymorphism), also detailed in that paper.

Marcello's Waterfall falls prey to the Procrastination Paradox, as a direct result of trusting itself: it beli

...
Weekly LW Meetups
by FrankAdamek — 2015-07-03T18:05:18.340Z

This summary was posted to LW Main on June 26th. The following week's summary is here.

New meetups (or meetups with a hiatus of more than a year) are happening in:

Maine: Automatic Cognition: 29 June 2015 06:30PM
San Antonio New Meetup: 28 June 2015 03:00PM
São Paulo, Brazil - Meetup at Base Sociedade Colaborativa: 27 June 2015 01:00PM

Irregularly scheduled Less Wrong meetups are taking place in:

Australia online hangout: 28 June 2015 07:30PM
Australian Less Wrong Mega Meetup #2: 17 July 2015 07:00PM
Australia-wide Mega-Camp!: 17 July 2015 07:00PM
[Edinburgh] LessWrong Scotland: 28 June 2015 02:00PM
Frankfurt Meetup Revival: 29 June 2015 06:30PM
Hamburg : 17 July 2015 06:30PM
Oslo Meetup at Bitraf.: 18 July 2015 04:00PM
[Prague] Rationality meetup in Prague #3: 30 June 2015 06:30PM
San Francisco Meetup: Keep your identity small: 29 June 2015 06:15PM

The remaining meetups take place in cities with regular scheduling, but involve a change in time or location, special meeting content, or simply a helpful reminder about the meetup:

Austin, TX - Caffe Medici: 27 June 2015 01:30PM
Durham, NC (RTLW) Discussion Meetup: 02 July 2026 07:00PM
London regular meetup: 28 June 2015 09:39AM
[Seattle] Rationality Reading Group (updated): 29 June 2015 06:30PM
Sydney Rationality Dojo - July: 05 July 2015 04:00PM
Sydney Meetup - July: 22 July 2015 06:30PM
Sydney Meetup - August: 26 August 2015 06:30PM
Sydney Meetup - September: 23 September 2015 06:30PM
Vienna: 18 July 2015 03:00PM
Washington, D.C.: Fun & Games: 28 June 2015 03:00AM

Locations with regularly scheduled meetups: Austin, Berkeley, Berlin, Boston, Brussels, Buffalo, Cambridge UK, Canberra, Columbus, London, Madison WI, Melbourne, Moscow, Mountain View, New York, Philadelphia, Research Triangle NC, Seattle, Sydney, Tel Aviv, Toronto, Vienna, Washington DC, and West Los Angeles. There's also a 24/7 online study hall for coworking LWers.

If you'd like to talk with other LW-ers face to face, and there is no meetup in your area, consider starting your own meetup; it's easy (more resources here). Check one out, stretch your rationality skills, build community, and have fun!

In addition to the handy sidebar of upcoming meetups, a meetup overview is posted on the front page every Friday. These are an attempt to collect informati...
An approach to logical counterfactuals inspired by the Demski prior
by Scott Garrabrant — 2015-07-03T17:26:04.000Z

This is a probabilistic approach to logical counterfactuals inspired by the Demski prior. Given a sentence ϕ, we wish to ask what other logical sentences are true in the world C(ϕ) where we correctly counterfactually assume ϕ. I spoke about this before here and here, but now I am going to approach the problem slightly differently. Instead of insisting that every other sentence ψ is either true or false in the counterfactual world C(ϕ), I allow C(ϕ) to assign probabilities to each sentence.

When you try to describe counterfactual worlds as sets of true and false sentences, you necessarily have very sharp boundaries. You will have, for example, counterfactual worlds where ϕ and ψ are true, but ϕ∧ψ is false. Probabilities seem to be more realistic by allowing us to smooth the boundaries. As you look at sentences which are more and more logically distinct from ϕ, you can gradually change probabilities so that they will represent the truth, rather than representing consequences of ϕ.

Let μ be a measure on logical sentences, for example, μ(ϕ)=2−ℓ(ϕ), where ℓ(ϕ) is the number of bits necessary to encode ϕ. Let TN be the theory containing all sentences true about the natural numbers. Consider the following procedure which computes P(ψ|ϕ). This definition is only for ϕ which are consistent by themselves.

Let T0 be the theory containing only the sentence ϕ. For n≥0, compute Tn+1 from Tn by sampling a sentence tn according to μ. If both TN+tn and Tn+tn are consistent, then Tn+1=Tn+tn. Otherwise, Tn+1=Tn. Let T∞ be the union of all of the Tn. P(ψ|ϕ) is the probability that ψ is a consequence of T∞.

As it is, this procedure is not approximable, but you can make a similar thing approximable by replacing TN with PA, or a complete theory sampled from your favorite approximable distribution.

Claim: P(⋅|ϕ) gives a coherent probability assignment which assigns probability 1 to ϕ, and thus represents a probability distribution on complete theories.

Proof: The probability distribution on complete theories is exactly the distribution on T∞. All we need to show is that T∞ is complete (with probability 1). Take a sentence ψ. Either ψ or ¬ψ is consistent with TN. WLOG assume ψ is consistent with TN. The sentence ψ is eventually sampled at some time n. Either ψ is added to Tn, or it is inconsistent with Tn. Therefore, either Tn proves ¬ψ, or Tn+1 proves ψ, so T∞ proves either ψ or ¬ψ. Note

...