Yeah, I at least occasionally do step by step derivations directly in TeX. I don’t think Knuth would look at me funny if I told him I was doing this.
transhumanist_atom_understander
Karma: 682
Cool.
I was hoping there was some way to enumerate inequivalent bots. I guess by modal depth within a rank, then by rank.
The way I would put the match with PrudentBot is this. It takes
Which is related to unexploitability. The new bot is unexploitable. But if you can’t prove it defects against DefectBot, then you can’t prove it’s unexploitable. So it’s not provably unexploitable in
You know, it occurs to me that the Barcan formula is by Ruth Barcan Marcus, who is mentioned in the post, in the Dennet quote:
There were nominating speeches and rebuttals, the most memorable of which was by Ruth Marcus, whose Yale colleague John Smith, a philosopher of religion and a theologian, was the pluralists’ candidate. She explicitly trashed his whole career, his character, his books. I had never heard a philosopher speak so ill of a colleague in public, and seldom in private.
So not just a (minor) example of the significance of modal logic from the perspective of mathematics, but from specifically the person Dennet was talking about.
Maybe I didn’t get across the connection to Zeilberger, it’s not that he’s doing or opining about logic, it’s that he’s developing decision procedures, so the disappointing yield from that research program suggests that maybe decision procedures aren’t so important. Like, reaching to something more basic than Zeilberger’s work for an example, there’s Gosper’s algorithm—Gosper’s paper was called “Decision procedure for indefinite hypergeometric summation”. Symbolic computation in the Zeilberger style is developing decision procedures for narrow classes of mathematical questions. The connection to irrationality isn’t about logic, it’s Zeilberger’s thought that since we have decision procedures for questions about hypergeometric sums, we should be able to use them somehow to search for hypergeometric sums to use in irrationality proofs (inspired by how Apéry used handmade hypergeometric sums to prove irrationality of ζ(3)).
They’re decidable fragments.
It seems to me that should make a big difference, but apparently that doesn’t count for as much as I thought, because symbolic computation (also really a collection of decision procedures) hasn’t lived up to the grand promise that Zeilberger sold us. (A modest example: computer algebra systems have been used to do Apéry’s proof of the irrationality of ζ(3), but despite Zeilberger’s efforts I can’t think of any big irrationality proofs that were discovered with symbolic computation.)
The definitions of “modal agent”, “rank”, and “unexploitable” are in the paper.
Likewise, I suspect that the analytic philosophers of 1979 could trounce the continental philosophers at, I dunno, externally-legible tests vaguely related to philosophical reasoning, like the LSAT. If so, the rebels didn’t care.
Maybe an example is the use of logic in computer science.
I keep thinking the deep theory of modal logic developed in philosophy departments should have some impact on math, but it doesn’t seem to have happened yet, as far as I know.
Is there only one FairBot?
I was thinking about how to make an analogue of the betrayal-based FairBot definition from the provability setting.
I think it requires being able to condition on the results of particular matches. We could do that in Python with a Judge object. The Judge runs matches, like this:
class EpsilonGroundedFairBot: def __call__(self, opponent, judge): if random.random() < ε: return C return judge.run(opponent, self)judge.runchecks some internal lookup table for a result for the match, and if it finds it, returns that result. Otherwise it actually runs the bot. In this case, we don’t add to the lookup table.We only add to the lookup table to condition on results of particular matches. Using the conditioning idea to translate the idea of betrayal, I end up with something superficially like
NiceProbeSimulator, but which I’ll callConditioningFairBot:class ConditioningFairBot: def __call__(self, opponent, judge): newJudge = judge.condition(self, opponent, C) return newJudge.run(opponent, self)judge.condition(x, y, r)returns a new Judge, which will always say thatxdoesragainsty, just by checking its lookup table.Seems to me like
ConditioningFairBotshould achieve efficient cooperation with anotherConditioningFairBot. After two recursions, we hit the lookup table.
Can’t believe I just noticed this comment thread… yeah, I got stuck for a while when doing the same thing because I had
Anyway, can go in the other direction too: if PA derives
It’s weird for me to think of betrayal as entirely my opponent’s choice, since it’s a conjunction of two things, their decision to defect, and a proof of my cooperation (which I suppose that I control, not them). Like… yeah it’s up to them to betray me, but it’s up to me whether they have the opportunity.
Thinking of time… if you’re fair and you defect, that’s because yesterday I betrayed you. So yesterday, there was a proof of your cooperation and I defected.
What’s it mean that yesterday there was a proof of your cooperation? Well I’m treating yesterday as what’s possible, so let’s translate “you provably cooperate” to “it’s not possible you defect”. So if there was a proof of your cooperation yesterday, that just means it’s not the case that you defected the day before yesterday.
That actually gives a “dynamic” proof of cooperation when we’re both fair (in the betrayal sense). It’s a proof by contradiction, starting by assuming you defect. Why did you defect? Because yesterday, I betrayed you—I defected, even though you hadn’t defected the day before. So why did I defect? Because the day before that, you betrayed me. So we have a contradiction: did you defect two days ago or not? This is a straight translation of the proof using possible world semantics.
I originally wanted to translate “provably cooperate” as “had always previously cooperated”. This would correspond to transitivity in possible world semantics. I guess you could translate provability in terms of the word “before”, which could either mean “immediately before” (not transitive), or “any time before” (transitive). We have transitivity in provability logic but don’t actually need it for this proof about betrayal. With transitivity, original FairBot is not Tit-For-Tat but an unforgiving bot that, once someone defects against it, defects back forever.
What I call “the new definition of fairness” seems like the provability version of what you call “niceness”.
What a coincidence that we made these posts within two hours of each other.
Inside the mind of a fair player cooperating
Lately I’ve been thinking about proof-based agents: agents that search for proofs in Peano Arithmetic of the consequences of their actions, and decide based on that.
I think when you formulate them right (which would be very different from the last attempt), they have a kind of “free will” that comes from this kind of underspecification.
Specifically: the proof system used to derive stuff like “if I take action A, then the environment will be in state S” cannot derive stuff like “I take action A”.
The model of the agent where I think this works out is it is doing a random proof search. Or a pseudorandom proof search, and “I take action A” means “I take action A regardless of the seed for the random number generator”. That is, the proofs are actually about an ensemble of agents with different RNG seeds.
Since the proof system can’t prove its consistency, it can’t prove that all proof searches will come up with the same result.
This incompleteness about the antecedents of our counterfactuals looks a bit like free will, but it requires considering this ensemble of agents, where we specify they’re doing a proof search but leave out the “microscopic” detail of the RNG seed.
This is in contast to functional decision theory, where we work with a complete specification of the agent, and thus need counterpossible implications, where the antecedent is provably false.
I’m hoping to work out the details and post more about it soon. For now you can believe me or not that this is a coherent theory.
But yeah, I think underspecifying “microscopic” details in a “macroscopic” description is where you get something like free will.
People always say randomness doesn’t help with free will, but it seems to me there’s this weird middle path, where your actions are not determined (in PA), but still not arbitrary (becaue they’re determined in PA+consistency of PA).
An argument of Parfit’s reconsidered with logical decision theory
transhumanist_atom_understander’s Shortform
Does anyone have software they like for doing provability logic? Two use cases:
-
Deciding theorems of GL. I recently made a post which had two derivations in GL. GL is decidable, so I should be able to write them as material implications and run some program to check if they’re theorems. I have no idea what program people would actually use for this though.
-
Computing fixed points. For that post, I would want to input the “equation”
-
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
No problem, I edited and it looks a lot better now.
With that cleared up I do want to get back to the root of this thread, because it’s genuinely weird that the FairBot pseudocode in the paper has a branch where it says “if there’s no proof, return D”. But it’s getting late here so I’ll have to do that another day.
For a hint of the missing pieces between Feynman and Drexler, there’s an extraordinary 1972 lecture by Freeman Dyson. It doesn’t really say anything about nanotechnology, but he has a suggestive section on “enzyme systems tailored to our own design”, followed by the section on “self-reproducing machinery”:
I don’t really see the core ideas of Drexler’s paper:
With molecular biology, “we can begin on the far side of the barrier facing conventional microtechnology.” This is often forgotten, that Drexler thought the path to nanotechnology begins with the ribosome, not just inspired by it, but actual use of it.
Computational design. In fact, Dyson was one of the peer reviewers of Drexler’s paper, and one of his comments was that he thought modification of natural proteins was a more plausible near future tech than engineering-style design, perhaps vindicated by Frances Arnold’s Nobel prize
That the protein folding problem is not actually important for protein engineering. I think the main impact of Drexler’s paper in mainstream science was as a reference for the idea of optimizing a sequence for a target structure. This was eventually the basis of David Baker’s Nobel prize, though I’ve never heard of any direct influence of Drexler on Baker.
So it’s certainly new ideas… but… well, Dyson’s talk shows the kind of ideas that would be floating around in Drexler’s L5 Society milieu. In fact Dyson himself was plausibly an important mode of transmission here, since he knew Feynman and then became friends with Gerard O’Neill. Drexler directly reading Feynman is not the only mode of transmission here.
Though if I had to summarize Drexler’s importance as a predecessor to the rationalist community in a sentence, I would not start with the content of his papers, but rather that he brought the culture of exploratory engineering fostered by Gerard O’Neill to the Bay Area tech scene. One of the most important things he did, I think, was physically cross the country, from the east coast to the west coast. He didn’t just come up with nanotech, he came up with Bay Area futurist orgs that do technical work!