Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: general

Topic: counterfactuals

sarahzrf (Apr 23 2020 at 18:15):

david lewis :o

sarahzrf (Apr 23 2020 at 18:16):

im dimly aware of his work on counterfactuals

sarahzrf (Apr 23 2020 at 18:16):

reading about it a while back when i was working on this draft i never totally finished of a paper abt a counterfactual conditional thing

sarahzrf (Apr 23 2020 at 18:21):

i was interpreting "nearest possible world" for a counterfactual as initiality in an under category

sarahzrf (Apr 23 2020 at 18:21):

but it only kinda worked

Henry Story (Apr 23 2020 at 18:58):

Yes, David K. Lewis' book counterfactuals was the one I first read.(collection of papers online). He there analyses "If Kangaroos had no tails, they would topple over" as If In the closest world (to the actual world) where kangaroos have no tails they do topple over" then the sentence is true. For this he adds to normal modal logic a closeness relation (also a system of spheres that collect equally close worlds). This is very useful to analyze knowledge in a way that allows one to take account of epistemic black holes (the brain-in-a-vat example, in older days dreaming). But it also gives a very interesting analysis of causality, though that has been very much debated since then, and was clearly an inspiration to Judea Pearl's work. He also uses the same distance relation in Counterfactuals to give an interesting analysis of deontic logic, and one for denoting.
It is not difficult to understand counterfactuals if one maps things out on a paper.
But it would be good to find a category theoretic explanation of it.

sarahzrf (Apr 23 2020 at 19:44):

yeah i saw the spheres thing

sarahzrf (Apr 23 2020 at 19:45):

for the purposes i wanted, it seemed too... fuzzy? not qualitative enough?

sarahzrf (Apr 23 2020 at 19:46):

i wanted to exhibit, like, the complex numbers as a counterfactual where $x^2 = -1$ has a root

sarahzrf (Apr 23 2020 at 19:46):

...but the setup i used didn't actually manage to capture that one :\ because C is not initial under R, since it has nontrivial automorphisms that fix R

sarahzrf (Apr 23 2020 at 19:47):

you have to equip it with a choice of either i or -i as the witness to the counterfactual for things to work

sarahzrf (Apr 23 2020 at 19:47):

but i wasnt sure how you could generalize that

sarahzrf (Apr 23 2020 at 19:48):

check it out if u want
(altho it is rly more model-theoretic than category-theoretic)

Henry Story (Apr 23 2020 at 20:06):

I am doubt that counterfactuals work that well with mathematical truths. They are better for empirical ones, which is what possible worlds model,
Modal logic using possible worlds tends to have problems with mathematical truths as they are all necessary, and so identical. Unless one adds impossible worlds to the mix.

sarahzrf (Apr 23 2020 at 20:08):

i don't see what's wrong with mathematical counterfactuals

sarahzrf (Apr 23 2020 at 20:09):

well, i mean

sarahzrf (Apr 23 2020 at 20:10):

i'm not a philosopher, and i don't know whether Real Mathematical Truth is Genuinely Subject To Counterfactuals or anything like that

sarahzrf (Apr 23 2020 at 20:11):

although i am rather suspicious of the idea that mathematical truth is necessary

sarahzrf (Apr 23 2020 at 20:11):

depending on what you mean by "mathematical truth"

Henry Story (Apr 23 2020 at 20:12):

I wonder if work on Modal HoTT will get us there. In his book "Modal Homotopy Type Theory" David Corfield write:

The slogan here is that, where HoTT itself is the internal language of (∞,1)-toposes, modal HoTT is the internal language for collections of (∞,1)-toposes related by geometric morphisms

sarahzrf (Apr 23 2020 at 20:13):

but more concretely, i mean, like

sarahzrf (Apr 23 2020 at 20:14):

people have historically used counterfactual reasoning with great success in math all the time, before the advent of modern rigor—maybe afterward too, idk?—and that probably means something

sarahzrf (Apr 23 2020 at 20:14):

think about imaginary numbers and infinitesimals

sarahzrf (Apr 23 2020 at 20:17):

maybe i'm mistaken, but i had the impression that historically there was much more of a tendency to view math as something that investigated pre-existing objects in places where we now think of it as building new ones

Henry Story (Apr 23 2020 at 20:19):

Usually mathematical truths are meant to hold in all possible worlds.
But I guess if you are a constructivist, you may argue as Kaspner does in Logics and Falsifications that proofs are constructions that when verified lead to a mathematical truth. Then in the proof you can use counterfactuals regarding the proof, but not the final result.

Henry Story (Apr 23 2020 at 20:20):

(That book is very interesting but sadly he does not know about Category Theory, and so does not know which dualities to choose, and also a bit arbitrarily rejects topology as a model of constructive logic -- that can teach us something about our everyday use of language I should add.)

sarahzrf (Apr 23 2020 at 20:21):

weird

sarahzrf (Apr 23 2020 at 20:23):

anyway, is "$-1$ has a square root" true in all possible worlds? :)

sarahzrf (Apr 23 2020 at 20:23):

i'm being a little flippant

sarahzrf (Apr 23 2020 at 20:25):

here, check this out image.png

Reid Barton (Apr 23 2020 at 20:28):

[movie announcer voice] In a world... in which 2 = 0...

T Murrills (Apr 23 2020 at 20:29):

I (personally) think possible worlds are only coherent when formulated with respect to something which has the capability of “imagining”, more or less; like, the whole idea of another world being “possible” might not make any sense to begin with in “reality” (it might be the case that all truths are necessary) but only make sense with respect to something that can apprehend the current actual world somehow and then “construct” that possible world. Likewise with mathematical constructions!

sarahzrf (Apr 23 2020 at 20:32):

well, if by "possible worlds" you mean "kripke semantics", then kripke semantics are just the (0, 1)-truncation of presheaves, and every presheaf category is coherent 🤭

Henry Story (Apr 23 2020 at 20:35):

The book "Logics and Falsifications" and Traffords Meaning in Dialogue argue that the Kripke semantics of constructive logic should be applied to proof construction. This could open the door to counterfactual readings in mathematics I guess. Because proof construction is empirical. Instead of thinking of a proof as stating a fact (e.g 2=-1) one should think of it rather as write that down, and through dialogue (internal or external) looking to see if it can answer all attacks. Negation in constructive logic is then seen as $A \to \emptyset$, that is a statement that a certain proof construction leads to an impossible proof. (Note: Trafford does incorporate work from Category Theory and Topos theory)

T Murrills (Apr 23 2020 at 20:38):

( @sarahzrf I don’t mean Kripke semantics but lol 😝)

Pastel Raschke (Apr 23 2020 at 21:00):

informal mathematical statements can be made in an ambiguous context, so can have an ambiguous meaning. refining the context a statement is interpreted in/refining the meaning of a statement offers choices.

you might require that statements be interpreted in contexts you're comfortable with. you might be searching for a modal formal counterpart of some intuitive idea and so have some desiderata for what would count as an instance of that idea in a formal context.

in some contexts the things you thought you were talking about might furcate and so you have to choose a representative, or examine the diversity (cf commutative monoids -> braiding vs symmetry -> ....).

i think the meaning in dialogue approach can be viewed as reconciling and refining different interpretations of statements and their contents, and through that process negotiating the meaning of a shared language (though the meaning could end up very different from the ostensible goal, like "this means a fight is starting, time to get angry")

but i haven't actually gotten through the book

Henry Story (Apr 23 2020 at 21:18):

yes, that's the gist of it.

Henry Story (Apr 23 2020 at 21:23):

Trafford also develops the duality with co-constructive logic as a logic of refutation, and the interplay between construction and refutation attempts leads to the final proof.

John Baez (Apr 24 2020 at 00:35):

I don't think something like "2 = 0" or "there is a square root of -1" are the kind of things that can be true or false. I think of them more as axioms you can investigate. The first one (together with some others) leads you to $\mathbb{Z}/2$, while the second (together with some others) leads to $\mathbb{C}$. I wouldn't say either of these number systems is "true"... nor would I say it's "false". It's just a system one can investigate... and perhaps put to use.

John Baez (Apr 24 2020 at 00:36):

I try to stick to using "true" as the answer to questions like "from these axioms and these deduction rules, can you deduce this formula?"

(=_=) (Apr 24 2020 at 04:16):

Reid Barton said:

[movie announcer voice] In a world... in which 2 = 0...

That's nothing. As John said, that's working with $\mathbb{Z}/2$.

[movie announcer voice] In a world... in which 1 = 0...

And that's working with $\mathbb{F}_1$. <ducks>

Mohamar Rios (May 11 2020 at 17:46):

I'm actually doing my masters thesis on David Lewis counterfactuals and sphere worlds. I'm investigating a way to talk about neighborhoods of worlds.

Mohamar Rios (May 11 2020 at 17:47):

Pleasantly surprised to see them being talked about here. :smiley:

Henry Story (May 11 2020 at 18:10):

Very nice! There is the very detailed 2011 thesis by Kohei Kishida Generalized Topological Semantics for First-Order Modal Logic which looks at the difference between Kripke and Lewis semantics from a Category Theoretical point of view. I was reading that a 1½ years ago, when I knew a lot less. I need to get back to it. I think it looks mostly at the counterpart relation problem between them, but does not investigate Lewis' counterfactual relation based on adding a distance (similarity) relation to possible worlds. The PhD had an amazing team of reviewers: Nuel D, Belnap , Steve Awodey, Kenneth Manders and Robert Brandom !!!

sarahzrf (May 11 2020 at 18:27):

oh does that do a thing w/ fibers

sarahzrf (May 11 2020 at 18:28):

or does it generalize that

sarahzrf (May 11 2020 at 18:28):

ahh generalizes i guess

sarahzrf (May 11 2020 at 18:30):

here's a fun POV: depending on the details of your definitions, covering spaces are exactly locally constant sheaves

sarahzrf (May 11 2020 at 18:32):

now if you think of sheaves as generalized bundles, of the base space of a bundle as the space of worlds, and of the fiber over a world as the space of individuals in that world—then this means that a locally constant sheaf is exactly one where, on a local scale, there is a coherent counterparthood isomorphism between spaces of individuals

sarahzrf (May 11 2020 at 18:32):

you can even kinda see this in covering space theory!

sarahzrf (May 11 2020 at 18:33):

in a trivial covering space $\pi_2 : D \times B \to B$ for discrete $D$, there is an obvious "counterpart" over each point of the base for any given point of the total space

sarahzrf (May 11 2020 at 18:34):

just move around within the same copy of $B$, leaving the $D$ coordinate unchanged

sarahzrf (May 11 2020 at 18:35):

but if you consider the archetypal covering $\mathbb R \to S^1$, there's no coherent way to assign a counterpart of a given point in R over some other point of the base S¹—you need to also prescribe which path you take between the points of the base, because counterparthood only works at a local scale, so you need all of the intermediate information given by a path

John Baez (May 11 2020 at 18:54):

Yes, it's fun to imagine loops of possible worlds that take you back to the same situation but with the names of two people interchanged, or something like that.

sarahzrf (May 11 2020 at 18:58):

$z \mapsto z^2 : S^1 \to S^1$ ;)

John Baez (May 11 2020 at 18:58):

This is connected to how in physics identical particles are truly indistinguishable, and in the case of "anyons" in two dimensions the topology of braid traced out by a bunch of identical anyons is important for what happens. The space of n-element subsets of the plane has the n-strand braid group as its fundamental group.

John Baez (May 11 2020 at 18:58):

This space of n-element subsets has an infinite-sheeted universal cover, which is the sort of thing you were talking about...

sarahzrf (May 11 2020 at 18:59):

i imagine lifting to that is sort of like "remembering identities"?

John Baez (May 11 2020 at 19:00):

Sorta. That's more correct in the usual 3d physics case where the space of n-element subsets of $\mathbb{R}^3$ has the permutation group $S_n$ as its fundamental group.

John Baez (May 11 2020 at 19:00):

Then the universal cover is "n-tuples of particles with known identities".

John Baez (May 11 2020 at 19:01):

There are n! of these mapping to each n-tuple of points in $\mathbb{R}^3$.

John Baez (May 11 2020 at 19:01):

So the projection of the covering map is "forgetting who is who".

sarahzrf (May 11 2020 at 19:02):

so what does the universal cover of the 2d case look like?

John Baez (May 11 2020 at 19:02):

In the 2d case, where you get a braid group as the fundamental group, it's not just about "who is who" but also "how they got there".

sarahzrf (May 11 2020 at 19:02):

oooooh

John Baez (May 11 2020 at 19:02):

What does it look like?

sarahzrf (May 11 2020 at 19:02):

ha, i didnt mean that literally, but i wouldnt mind...

John Baez (May 11 2020 at 19:03):

Well, a point in the universal cover is an n-tuple of labelled points with a homotopy class of paths from some chosen "standard" n-tuple of labelled points, like

1 2 3 4 5

sitting in a row.

John Baez (May 11 2020 at 19:03):

This homotopy class of paths can be seen as a braid.

sarahzrf (May 11 2020 at 19:05):

...right, points in the universal cover correspond to paths >.<

John Baez (May 11 2020 at 19:06):

So one can draw nice pictures of individual points in the universal cover, as braids.

John Baez (May 11 2020 at 19:06):

like this

sarahzrf (May 11 2020 at 19:07):

yeah, ive encountered the idea of the braid group as this particular $\pi_1$ before :)

John Baez (May 11 2020 at 19:07):

But it's pretty hard to visualize the whole covering space in one go.

sarahzrf (May 11 2020 at 19:07):

id imagine

sarahzrf (May 11 2020 at 19:08):

what about for just two points? :thinking:

sarahzrf (May 11 2020 at 19:08):

i guess that's still gonna be at least 4d :grimacing:

John Baez (May 11 2020 at 19:09):

If you have 2 points, hold one fixed, and let the other roam, the universal cover will be the universal cover of the punctured plane, which is the usual infinite-sheeted "spiral staircase" thing you get for the Riemann surface of $\ln z$.

John Baez (May 11 2020 at 19:10):

Here - it's on Wikipedia:

Riemann surface of logarithm function

sarahzrf (May 11 2020 at 19:11):

yeah, $\exp$ as a covering

John Baez (May 11 2020 at 19:11):

Right.

John Baez (May 11 2020 at 19:11):

So that's not bad, but when you get more points it starts boggling the imagination.

John Baez (May 11 2020 at 19:12):

But it's just more of the same stuff.

Jules Hedges (May 11 2020 at 19:12):

So I don't understand how this magically jumped from counterfactuals to covering spaces, but I suspect it might be secretly exactly the same step that causes lenses to appear in compositional game theory

sarahzrf (May 11 2020 at 19:12):

:rofl:

sarahzrf (May 11 2020 at 19:13):

sorry, i dont mean to laugh at you as much as at the fact that, given how math works, thats probably true

Jules Hedges (May 11 2020 at 19:13):

I thought a bunch about how lenses are "really" describing counterfactuals, and they're the same thing as morphisms between actually constant sheaves

sarahzrf (May 11 2020 at 19:13):

if you scroll up, im the one who made the jump—it was here
sarahzrf said:

here's a fun POV: depending on the details of your definitions, covering spaces are exactly locally constant sheaves

sarahzrf (May 11 2020 at 19:14):

the connecting line is topological semantics where a base space is a space of worlds & fibers are spaces of individuals

Jules Hedges (May 11 2020 at 19:15):

What's an "individual"? An epistemic agent?

sarahzrf (May 11 2020 at 19:15):

"individual" as in the terminology of FOL—element of the domain of discourse

sarahzrf (May 11 2020 at 19:15):

or, less rigidly, "one of the things that the quantifiers range over"

sarahzrf (May 11 2020 at 19:16):

this being semantics for modal fol

Jules Hedges (May 11 2020 at 19:16):

Hm. Maybe it's the same, maybe it's not, not sure

sarahzrf (May 11 2020 at 19:17):

btw @John Baez i just realized: do you care about these coverings for a reason at all similar to why you care about the spin group :o

sarahzrf (May 11 2020 at 19:17):

just, thinking abt the idea of winding something around & that being different as you keep going around, reminds me of fluff ive heard about spinors

sarahzrf (May 11 2020 at 19:20):

@Jules Hedges what do lenses have to do with counterfactuals & sheaves tho :thinking:

Jules Hedges (May 11 2020 at 19:25):

Soo. Start from game theory, game theory is counterfactuals all the way down: a player actually chooses some action because if they chose some other action then their payoff would be lower. All of the information you needed from that is encapsulated in the function $X \to \mathbb R$ from their moves to payoffs, which is the same as a costate $(X, \mathbb R) \to I$ in lenses, aka a continuation. Players actually build this function by counterfactual reasoning about what other players would do given different choices by themselves, and it turns out that this counterfactual reasoning is described by precomposition of the continuation with lenses

sarahzrf (May 11 2020 at 19:26):

$I$ in the codomain there is $(I, I)$?

Jules Hedges (May 11 2020 at 19:26):

Yes

sarahzrf (May 11 2020 at 19:28):

hmm

Jules Hedges (May 11 2020 at 19:28):

For lenses specifically (not for other optics, I have no idea how to generalise it), the object $(X^+, X^-)$ is like the constant sheaf $X^-$ on $X^+$, and the category of lenses is equivalent to the full subcategory of constant sheaves (of sets on Set)

Jules Hedges (May 11 2020 at 19:29):

And I'm pretty sure the same idea goes through fine for morphisms between arbitrary sheaves

sarahzrf (May 11 2020 at 19:31):

wait

sarahzrf (May 11 2020 at 19:31):

do you mean "of sets on sets", rather than "of sets on Set"?

sarahzrf (May 11 2020 at 19:31):

and you're aggregating sheaves on all possible base sets together into one category by a grothendieck construction or something?

Jules Hedges (May 11 2020 at 19:31):

Yes, exactly

sarahzrf (May 11 2020 at 19:32):

so could we rephrase this as, say, this is the subcategory of $\mathbf{Set}^\to$ whose objects are 2nd projections

Jules Hedges (May 11 2020 at 19:33):

No, the morphims are different to $Set^\to$ I think

sarahzrf (May 11 2020 at 19:33):

are you sure?

Jules Hedges (May 11 2020 at 19:33):

No

sarahzrf (May 11 2020 at 19:33):

if they are, maybe you're thinking of sheaves differently from how i am

Jules Hedges (May 11 2020 at 19:33):

It's a function between the bases plus an ordinary sheaf morphism backwards where one of them is a pullback-y thing

Henry Story (May 11 2020 at 19:34):

Jules Hedges said:

Soo. Start from game theory, game theory is counterfactuals all the way down: a player actually chooses some action because if they chose some other action then their payoff would be lower....

That makes a lot of sense. It also explains how David Lewis would have moved from his 1969 thesis Convention supervised by W.V.O. Quine to his later work on counterfactuals, 4 years later. In Convention Lewis gives a game theoretical grounding of Convention. The first few pages of examples make the thinking very clear. One has to be a bit patient to get over his analysis of convention in signaling, to the last part of the book where he ties this in to Convention in a full Language.

Jules Hedges (May 11 2020 at 19:36):

Jules Hedges said:

It's a function between the bases plus an ordinary sheaf morphism backwards where one of them is a pullback-y thing

Specifically: if $S$ is a sheaf on $X$ and $T$ is a sheaf on $Y$ then a morphism $S \to T$ should be a function $X \to Y$ and a sheaf morphism $f^* T \to S$

sarahzrf (May 11 2020 at 19:38):

oic

sarahzrf (May 11 2020 at 19:39):

well that's equivalent to a morphism $T \to f_* S$ right

sarahzrf (May 11 2020 at 19:39):

no wait hold on

sarahzrf (May 11 2020 at 19:40):

oo is that based on something liek this https://ncatlab.org/nlab/show/morphism%20of%20schemes

John Baez (May 11 2020 at 19:41):

sarahzrf said:

btw John Baez i just realized: do you care about these coverings for a reason at all similar to why you care about the spin group :o

Yes, it's the same. There's a long story here, of course.

Jules Hedges (May 11 2020 at 19:41):

So I learned this from David, he said it's based on morphisms of locally ringed spaces except you replace local rings with sets and also replace spaces with sets

sarahzrf (May 11 2020 at 19:42):

setted sets

Jules Hedges (May 11 2020 at 19:42):

Yes, exactly

sarahzrf (May 11 2020 at 19:42):

ssdjkdkls

Jules Hedges (May 11 2020 at 19:43):

Which turns out to be the same again as the category of polynomial endofunctors, another non obvious equivalence, that's teh subject of David's new preprint

Jules Hedges (May 11 2020 at 19:43):

aka. what functional programmers call containers

Jules Hedges (May 11 2020 at 19:43):

Everything is everything else in disguise

sarahzrf (May 11 2020 at 19:43):

hey, you dont have to tell me about functional programming

Henry Story (May 11 2020 at 19:44):

I like functional programming intuitions :-)

John Baez (May 11 2020 at 19:44):

I like to say "settled sets" instead of "setted sets".

Jules Hedges (May 11 2020 at 19:46):

I remember! Me and David and Brendan and Eliana were in the MIT common room talking about this and wandering what to call them, and I asked on twitter and you came up with that

John Baez (May 11 2020 at 19:56):

Yes, I keep saying the same things. :-)

sarahzrf (May 11 2020 at 19:57):

ok i think i get the counterfactual thing

John Baez (May 11 2020 at 19:57):

What's "the counterfactual thing"?

John Baez (May 11 2020 at 19:58):

That is, the specific thing to be gotten....

John Baez (May 11 2020 at 19:58):

... I want to get it too.

sarahzrf (May 11 2020 at 19:59):

is the idea like—naïvely, if you had a simulation of the other player, you could fiddle with that arbitrarily to figure out your move, so you could write your strategy as a function from the other player's strategy to a choice of move—except that would lead to infinite regress, so instead your strategy is something that is required to be able to operate on a bit more general of a class of approximations to some notion of "your opponent's strategy"?

sarahzrf (May 11 2020 at 20:00):

and that's, in fact, an optic?

Jules Hedges (May 11 2020 at 20:02):

yep

sarahzrf (May 11 2020 at 20:02):

you know, i wonder if you could formulate this internally to the topos of trees instead :thinking:

sarahzrf (May 11 2020 at 20:03):

and require that strategies be contractive

sarahzrf (May 11 2020 at 20:03):

or something

Jules Hedges (May 11 2020 at 20:09):

I did wondering about working in the topos of trees to try to get a delayed trace on open games that gives infinite repetition

sarahzrf (May 11 2020 at 20:09):

youve seen the synthetic guarded domain theory paper?

sarahzrf (May 11 2020 at 20:10):

well, i posted it in that other thread, but dunno if that means you looked at it ;)

Jules Hedges (May 11 2020 at 20:17):

I saw a couple of talks about it years ago

sarahzrf (May 11 2020 at 20:18):

cool

Jules Hedges (May 11 2020 at 20:18):

It's quite far down my todo list, probably past the event horizon, I don't expect to get to it basically ever

sarahzrf (May 11 2020 at 20:18):

lol

sarahzrf (May 11 2020 at 20:21):

:thinking:
$S_P \cong \triangleright S_O \to X \qquad S_O \cong \triangleright S_P \to Y$

sarahzrf (May 11 2020 at 20:23):

you think maybe^?

sarahzrf (May 11 2020 at 20:24):

$S_O$ is the type of opponent strategies, $S_P$ is the type of player strategies

sarahzrf (May 11 2020 at 20:24):

$X$ is the type of player moves, $Y$ is the type of opponent moves

sarahzrf (May 11 2020 at 20:25):

those should really be \blacktriangleright but i changed them back because zulip is turning \blacktriangleright into an emoji

Henry Story (May 11 2020 at 21:02):

Counterfactuals: "If Kangaroos had no tails they would topple over" = In the closest possible worlds where kangaroos have no tail they topple over. (That's how Lewis starts his book counterfactuals).

sarahzrf (May 11 2020 at 21:05):

"if two equaled zero then all integers would be either zero or one" = in the minimal quotient of $\mathbb Z$ where $2 = 0$, we have $\forall n. n = 0 \lor n = 1$

sarahzrf (May 11 2020 at 21:05):

;)

Henry Story (May 11 2020 at 21:10):

Tailless kangaroos are a bit easier to imagine. There are video of cases on YouTube too :-)

sarahzrf (May 11 2020 at 21:11):

i dunno, i find $\mathbb Z / 2 \mathbb Z$ pretty easy to think about :)

sarahzrf (May 12 2020 at 02:32):

@Jules Hedges yeah you get some kind of simple delayed feedback type thing with the definition i suggested above

sarahzrf (May 12 2020 at 02:33):

i think

sarahzrf (May 12 2020 at 02:34):

like... you should be able to define a player strategy by a löb recursion thing

sarahzrf (May 12 2020 at 02:36):

you have a |>S_P as your delayed self-reference, and you need to define an S_P, which you can do by accepting a |>S_O and providing an X

sarahzrf (May 12 2020 at 02:36):

you can distribute |> over → and turn |>S_O into |>|>S_P → |>Y

sarahzrf (May 12 2020 at 02:37):

then you can shove your delayed self-reference into another layer of |>, pass it to your opponent strategy, and get out a |>Y, their move

sarahzrf (May 12 2020 at 02:37):

if we decide that we'll use constant sets for moves X and Y, then we can extract |>X → X and |>Y → Y, so then we can see what move they would make

sarahzrf (May 12 2020 at 02:37):

and then we can decide on our X

sarahzrf (May 12 2020 at 02:46):

errr sorry so to be precise this is how you can get a strategy out of any Y → X

Henry Story (May 12 2020 at 08:54):

The key picture from the book Counterfactuals is the one below. The central dot represents the actual world, the spheres around it, group worlds in equivalent classes related to a similarity distance to the actual world (worlds where I wake up 2 minutes later are intuitively closer to worlds where pig s fly). Propositions are spaces of possible worlds. Take ψ: Kangaroos have no tails Φ: Kangaroos topple over. In the illustration that would make the sentence "if kangaroos had not tails they would topple over true" since all the closest ψ worlds are Φ worlds (that is the grayed out space)
Counterfactuals illustration

Mohamar Rios (May 12 2020 at 10:03):

Yeah, you've basically got ordinary logic with these two extra connectives (see note below).

1) The box connective is described above. Reiterating though it basically reads: "if it were the case that \phi, then it would be the case that \psi".
For instance "if the bullet had struck the heart, the patient would have died".

2) The diamond connective is written the same except with a diamond instead of a box. It reads: "if it were the case that \phi, then it might be the case that \psi"
For instance: "If the the bullet had struck the lungs, the patient might've died".

Sphere models give us a way of formalizing which worlds are closer or further than others to our own. Formally this is done by talking about nested sets of worlds. Some remarks about this are that:

• Lewis gives a short list of examples where one can talk about other types of logics by adding extra restrictions to the model. I don't remember these off the top of my head but one example involved being able to talk about an unreachable idealized world to deal with morality.
• When creating a model it's not necessarily obvious how far away (i.e. in which sphere) a given world should be, this is part of why Judea Pearl takes a different approach to counterfactual reasoning using causal networks. Arguably his approach is more popular these days.
• You don't actually get a metric on worlds. All you have is a notion of "how far away is a given world from our own world". Intuitively two worlds that are equally far from our own could also be far from each other. Also, getting from our world to another might be easier than getting back. For this reason you can't give worlds a metric topology (at least not in the usual way, my research involves this) and do other things you might at first expect to be able to do when seeing that picture of spheres.
• There are applications to machine learning interpretability where you think of sample inputs as your worlds. Like for a convolutional network that detects cats. You might take a picture containing a cat as your input representing "our world". Then you might perturb that picture slightly to obtain a slightly altered picture representing a nearby "world". By feeding the network several pictures you can create a map of worlds where a cat is detected. In other words you can figure out which features of the original picture are causing the network to detect a cat. I'm sorry if this explanation is not very good, the application is kind of in reverse and isn't super well known.

Note: Lewis actually develops a lot of different connectives and modalities in his book to do variations of the same thing but ultimately they're all equivalent to these two connectives

Jules Hedges (May 12 2020 at 10:30):

sarahzrf said:

Jules Hedges yeah you get some kind of simple delayed feedback type thing with the definition i suggested above

The definition you wrote looks like game semantics to me

sarahzrf (May 12 2020 at 13:28):

i was just using informal language to describe constructing an expression

sarahzrf (May 12 2020 at 13:31):

$\operatorname{löb}(\operatorname{self} \mapsto e \mapsto f(\operatorname{extract}(K(e)(\operatorname{next}(\operatorname{self})))))$

sarahzrf (May 12 2020 at 13:32):

where
löb constructs fixed points by guarded recursion, (|>A → A) → A
f : Y → X
extract : |>Y → Y
K is the K rule for |>, K : |>(A → B) → |>A → |>B
next destroys information, next : A → |>A

Henry Story (Sep 05 2020 at 08:34):

@sarahzrf I posted a few resources on impossible worlds in Philosophy of Mathematics that are of relevant to the problem of mathematical counterfactuals.