This is a special post for quick takes by jessicata. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.
TDT and FDT are ill-posed.
just think about the idea of "logical counterfactual". it is the kind of thing that cannot make logical sense. how can you formalize a thing that doesn't make logical sense? also miri empirically failed to formalize this for over a decade. if someone is advocating that "logical counterfactual" is a real thing, burden of proof is clearly on them at this point
FDT in the FDT paper is defined in terms of logical counterfactuals / subjunctives, so ill-posed-ness of logical counterfactuals spreads to FDT
TDT paper wrongly confuses between Bayesian networks (which represent joint distributions) and Pearlian causal diagrams (which make "further fact" claims about causality, usually disambiguated by physics), in any case it was supposed to be superseded by FDT paper, which as stated, is ill-posed
A "What if this computation had a different answer?" situation can be formalized by introducing a space of possible behavior-states of that computation (that in this case also needs to be able to account for states of being in logical time, for partially completed computations). Most points of that space will be counterfactual with respect to that computation. Something like Scott domains or (Hochster) spectral spaces. Failing to produce a formalized story like that for FDT-like decision making or coordination in PD is a problem, but I don't believe it's "the kind of thing that cannot make logical sense".
"possible behavior-states of that computation"
Is that like program states? Like, a Turing machine has a state in terms of the head state, and the tape. But then you talk about "logical time" and I no longer think this is well-defined.
"most points of that space will be counterfactual with respect to that computation" -- in the sense that for a given (nondeterministic) Turing machine, there is a set of impossible (head,tape) states, yes. nothing philosophically complicated about that.
"Something like Scott domains or (Hochster) spectral spaces." that's lambda calculus model. I'm familiar with Scott domains. I don't know how to apply them here. You could try interpreting the Scott domain state as analogus to partially completed Turing machine state, like lazy evaluation. And then you could say that some lazy evaluation states are impossible. I don't think it helps for FDT.
"Failing to produce a formalized story like that for FDT-like decision making or coordination in PD is a problem, but I don't believe it's 'the kind of thing that cannot make logical sense'" But if you are talking about things everyone believes in, that are not philosophically confusing, like "for a given nondeterministic Turing machine, there is some set of (head,tape) states that it never enters", then you are not solving the general "logical subjunctive" problem that the FDT paper relies on. That question is how to formalize a 'do' operator so I can ask E[U | do(A() = a)] where 'A' is some Turing machine program, fixed source code, and in fact 'A() != a' (and in fact, 'A() != a' is provable in PA). That is the philosophically hard thing, which I am saying is ill-posed.
then you talk about "logical time" and I no longer think this is well-defined
I'm gesturing at what Scott domains are doing that ordinary datatypes from programming usually don't (non-maximal points in specialization order for Scott topology; specialization order then formalizes something about logical time, incomplete states of computation, though logical time could also be about what the computation itself is doing rather than the space it lives in). This kind of structure (rather than ordinary datatypes) seems necessary to talk about some things in FDT-like decision making.
in the sense that for a given (nondeterministic) Turing machine, there is a set of impossible (head,tape) states, yes. nothing philosophically complicated about that.
That's sort of my point, it doesn't seem difficult to formalize counterfactuals, they just need to somehow be the appropriate counterfactuals. And a computation could in particular be enumerating a logical theory, which connects to the idea of logical counterfactuals (alternative partial theories that aren't describing this particular thing).
And then you could say that some lazy evaluation states are impossible. I don't think it helps for FDT.
I'm more thinking that the computation in question is reasoning about the target facts (agents, the world), so its state is building a state of knowledge. The way I imagine it helps with FDT is replacing the probability spaces with something else, and setting up the reasoning-computations in the right way for their counterfactual states to be relevant to how decision making makes use of counterfactuals.
things everyone believes in, that are not philosophically confusing, like "for a given nondeterministic Turing machine, there is some set of (head,tape) states that it never enters"
The philosophically confusing things are about the Turing machine itself having the "ontological authority" in deciding which states it never enters, and nothing outside that Turing machine being able to impose what those are (some kind of compatibilist free will), as well as dependencies between different computations that determine facts about each other, including when they are not literally subterms of each other. This is the way an agent acausally controls some world/computation it's not literally in, or coordinates with another agent that is not a literal copy of it, or doesn't perform a literal simulation of it in full (which wouldn't work anyway for coordination, but it's easy to short-circuit this process with reasoning about computations instead of simulating them directly).
and in fact, 'A() != a' is provable in PA
That depends on what A decides though, if it decides to compute 'a' then 'A() != a' is not provable in PA. And at an early enough logical time this won't be yet decided (I think logical time is always measured with respect to how some reasoning-computation is observing things; so in some system of reasoning about what's going on, as we look at A, we can say that it didn't yet decide what to do, and so we can't yet say that 'A() != a' is provable in PA then). That's the philosophical confusion clue about where such formalizations need to be reframed (to maybe start making sense).
solving the general "logical subjunctive" problem that the FDT paper relies on
That's the problem of setting on the reasoning-computations and their spaces of partial behavior-states appropriately. I don't know how to do that, but my guess is that it can be done.
Scott domains make some difference when we're using a lazy evaluation language like Haskell, however it's also possible to write programs in normal imperative / linear style.
That's sort of my point, it doesn't seem difficult to formalize counterfactuals, they just need to somehow be the appropriate counterfactuals.
So far the counterfactuals you're describing seem closer to physical than logical counterfactuals. Suppose we have a video game such as Factorio. It is possible to imagine a cosmic ray hitting a byte in the game, and then the program state changes, so the future of Factorio is different from what it would otherwise be. I agree this is basically well defined, in a way similar to physical causal counterfactuals. Moreover, it is possible to use a "abstracted physics" in the form of a (possibly stochastic) Turing machine, and do the "Factorio byte changed" counterfactual with no corresponding "cosmic ray" physics. However, this is not what the FDT paper is about ("do" operator on logical statement), and it's not what I mean by logical counterfactual.
I'm more thinking that the computation in question is reasoning about the target facts (agents, the world), so its state is building a state of knowledge.
We could imagine Factorio with computers in Factorio running an agent which uses cdt or something. Again, I don't know how to imagine Factorio with computers running an agent running FDT, because FDT does not seem well-defined.
That depends on what A decides though, if it decides to compute 'a' then 'A() != a' is not provable in PA. And at an early different logical time this won't be yet decided (I think logical time is always measured with respect to how some reasoning-computation is observing things; so in some system of reasoning about what's going on, as we look at A, we can say that it didn't yet decide what to do, and so we can't yet say that 'A() != a' is provable in PA then). That's the philosophical confusion clue about where such formalizations need to be reframed.
This is the bit where I'm not convinced the concepts are meaningful, that what you are talking about makes sense and is well-posed. Like, if A is some fixed string specifying a TM, PA proves A() halts, and 'a' is some fixed possible output of Turing machine, then either 'PA proves A() = a' or 'PA proves A() != a', yes? That's standard proof theory. At least one of these is a logical tautology? Then you say it "depends on what A decides though" and that's precisely where I am skeptical that this notion of "depends" and "decides" is meaningful.
The basic argument for why it's not meaningful: If in fact, 'PA proves A() = a', and b != a, then when you imagine the world where 'A() = b', you have to be imagining some axiom of PA is false, or that some PA-statement has no truth value. But this does not seem sensible. When reasoning about models of PA, we "help ourselves" to all of PA's axioms, to define statements and show them equivalent.
Like, if A is some fixed string specifying a TM, PA proves A() halts, and 'a' is some fixed possible output of Turing machine, then either 'PA proves A() = a' or 'PA proves A() != a', yes?
Yes, but only A decides that. So it should be possible to do the variable-constructions thing (as in sheaves/fibrations in logic-like settings), maybe all the way to the level of foundations of mathematics, and say that A didn't yet decide that. And so there isn't yet a fact of the matter, at that logical time (so "logical time" is pointing to something about locations in the base space, and the logic is making claims that vary with the base space). This is the way A itself should be reasoning about what's going on.
I think I see better what you mean: A() could reason as if it decides whether 'PA proves A() = a', even though we don't know what to put for A yet, i.e. we have not defined FDT.
I don't know what is the variable-constructions thing. Part of why I'm skeptical: I see how logical counterfactuals fail to make sense in 'normal math' (like logic, model theory, PA) and then you said something more advanced about Scott domains, which I happen to know about, and don't think they solve the problem; now you mention 'sheaves/fibrations in logic-like settings', which I know a little about (topos theory, which does something like a constructive logic / type theory), but which I'm not an expert enough in to say "no this doesn't solve the problem", so what am I to do? I am going to keep acting on the idea "logical counterfactuals do not make sense" and I am not going to take "[math thing jessicata does not understand] makes it work" as counter-evidence, unless it is explained clearly and convincingly.
I'm not claiming this makes enough sense for me to tell a formal story, all I can do is gesture at some intuitions about why I think it should be possible to make formal sense of this. So I'm not pointing to specific formal things and instead pointing in a general direction, because I don't know which specific formal things would fit. It's not very helpful, and probably structurally impossible to refute.
I don't know what is the variable-constructions thing
I just mean something like ETCS as opposed to the classical setting of "constant" sets (but again, literal ETCS is unlikely to be the right thing needed here). So all constructions/sets become variable (they vary with the base space). Logical time is then something that happens when we move in the base space.
(also posted on x dot com)
Brief response to "Reward is not the optimization target"