It’s interesting to learn why you first used as a decision trigger, because it sounds like you wanted to think of resolving these matches in terms of “well if I do this, then my opponent will...” type reasoning.
I don’t know what to call it.
“Mechanistic”… ?
But it’s interesting because even though that kind of reasoning wasn’t really in Andrew Critch’s write-up, it’s what popped out when I applied possible world semantics.
And that’s just because I had been applying possible world semantics to everything, by writing out tableaux.
The message got through.
Yes, “discursive time” sounds like what I see in the Kripke frames, though I have to qualify that by saying that Kripke frames don’t have to be linear.
You can create a branch with sorry, I meant .
I’ve never seen that come up in these kinds of games though.
It’s definitely appealing to have finite discursive time.
I guess you have the “everything is true from the beginning of time” rule to deal with infinite discourse.
Like, if we have ( could be that FairBot cooperates with itself), then we have , an infinite chain.
I would rather not prove things by saying “this would lead to infinite discourse, so it doesn’t happen”.
Lately I’ve been thinking of the condition as a sort of transformation of the condition.
For provability in PA, it turns out we have an equivalence: PA proves if and only if it proves .
Proving that equivalence requires Löb’s theorem, but once we’ve done it, we can resolve matches without ever encountering infinite frames.
In the zoo of modal logics, that means we have to use GL to prove the equivalence, but then we only need K4 to resolve matches.
(Irresponsibly generalizing from examples here.)
Of course I like resolving matches with finite discourse, because then I can just imagine the discourse step by step.
It sounds like that was your original intention, and it was certainly the significance to me: once I used the condition and saw these finite frames, that’s what showed me that you can have interpretable mechanistic reasoning about this seemingly infinitely reflective problem.
It’s interesting to learn why you first used
But it’s interesting because even though that kind of reasoning wasn’t really in Andrew Critch’s write-up, it’s what popped out when I applied possible world semantics. And that’s just because I had been applying possible world semantics to everything, by writing out tableaux. The message got through.
Yes, “discursive time” sounds like what I see in the Kripke frames, though I have to qualify that by saying that Kripke frames don’t have to be linear. You can create a branch with
It’s definitely appealing to have finite discursive time. I guess you have the “everything is true from the beginning of time” rule to deal with infinite discourse. Like, if we have
In modal logic, ruling out infinite chains corresponds to using GL instead of K4. See the zoo of modal logics and their corresponding requirements on Kripke frames.
I would rather not prove things by saying “this would lead to infinite discourse, so it doesn’t happen”. Lately I’ve been thinking of the
Of course I like resolving matches with finite discourse, because then I can just imagine the discourse step by step. It sounds like that was your original intention, and it was certainly the significance to me: once I used the