Keltham's treatment of this, to actually be understood, is going to end up requiring:

- The concept of a programminglanguage;
- The concept of a proofsystem that can formally verify things about programs in the programminglanguage;
- And the Assumable Provability Theorem stating that, in most proofsystems, you can freely assume something is provable in order to prove it.

That is, if something is provable within a proofsystem, starting from the premise that the quoted statement is provable inside the quoted proofsystem, then it's thereby provable within the system...

(He's drawing the cheerful cartoons that older kids draw to explain Assumable Provability to dath ilani children, because he did not in fact go back and learn any more serious-looking proofs as an adult.)

This is not at all a kind of math that any of these students have been exposed to at all!! It's not even something they'd previously have defined as math!!! 

Judging by the looks he's currently getting, Keltham should maybe back up and talk more about proofsystems and provability and quoting first.

How's the whole Baseline thing doing?  From Keltham's perspective, he gets to communicate using preciselyfitting categorizingwords a lot, without that taking forever, but he's not sure how that feels from the other side of Comprehend Languages.

It is maybe hard to evaluate how much of this lesson being very confusing is the Baseline and how much is the subject matter. 

All right, let's see what happens if he tries doing this next part in Taldane...

(30-40 minutes later, students' Comprehend Languages start running out.  It's not particularly clear that it was really helping.)

...he wonders if something different happens if he tries Share Language (Baseline).

That would be an inconvenient thing to have be super helpful; only Keltham can cast it, and he doesn't have enough 2nd-circle spells to tap the whole class even if he borrows against 3rd and 4th spells.

Share Language (Communal), 3rd-circle, will let Keltham divide up 24 hours in one-hour increments among any number of recipients by touch.  With 8 of them, that's 3 hours each.

Is there a reason Ione didn't mention this spell when Keltham told everyone yesterday to prepare Comprehend Languages today?

Because it makes sense to test Comprehend Languages first?  It's easier to get more of that, than more of Share Language (Baseline), if Keltham is trying to teach more people.

Don't assume that Keltham's actions make sense.  This is a dangerous assumption.  He's an alien.

Well, onward his brave researchers.

Some considerable amount of struggle and a number of Fox's Cunnings and Owl's Wisdoms later, the class maybe, possibly, understands how, if you had crisp formal agents...

let CooperateBot(_) = Cooperate

let DefectBot(_) = Defect

let FairBot (X) = if Provable( "X(Fairbot) == Cooperate" ) then Cooperate else Defect

...then FairBot(FairBot) == Cooperate.

Because of Assumable Provability:  If you assume Provable("Fairbot(Fairbot) == Cooperate"), then it would follow that Fairbot(Fairbot) == Cooperate.  Therefore, Fairbot(Fairbot) == Cooperate.

Now this is obviously not a shadow of the Law they seek, because Fairbot(CooperateBot) == Cooperate.

Even Keltham doesn't cooperate with a rock that has 'Cooperate' written on it.  It's not a person.  It definitely violates the assumption that the agent only seeks to earn as many coppers for itself as possible, and doesn't care about fairness.  That's why this is called Fairbot and not CopperBot.

"We want Law describing a - why are we calling them 'Bot' - that cooperates with FairBot, but not with CooperateBot? ...and there'd be other cases but that'd be a start."

"Uh, 'robot' is what Civilization calls... Civilization's equivalent of golems, is what I'd like to say, except I know nothing about golems except that 'robot' translates to that."  (The 'Bot' suffix as translated is literally the final syllable of Taldane's word for 'golem'.)

"And we don't literally have 'robots' doing this, probably not literally golems either, it's just - the name for a very simple thing that is pretending to be a person by following very simple rules, if that makes sense."

"In this case, we're not so much looking for a new piece of Law - the Law we're going to use is just Assumable Provability, which almost always ends up true of any proof-system you're not deliberately keeping it out of.  We're looking for a bot under that Law.

We're looking for a bot that mutually cooperates with itself, mutually cooperates with FairBot, defects against DefectBot, and defects against CooperateBot.  This is the simplest bot that we could say is acting like a shadow, inside this simpler realm, of a bigger and more complicated sane agent that seeks as much copper as possible."

"That bot is made out of pieces like the pieces I've already shown you, plus one more.  The final piece you need is the Provable-1 predicate, where..."

let Provable-1("X") = Provable(" ~Provable(0=1) -> X")

"...and what this means, is that it describes what you can prove assuming that the base system is consistent - that it never proves both a proposition, and its negation.  In this case, what it means is that Provable-1, but not Provable, can prove, for example, that FairBot defects against DefectBot.  You might say that Provable-1 is the proofsystem that trusts Provable."

"This matters, because you need the extra assumption that Provable is consistent, to derive inside Provable that, just because DefectBot always Defects, there's no proof inside Provable that DefectBot Cooperates..."

...they're lost again.

The backing up and the explaining again and the intelligence enhancement spells will continue until understanding has been achieved.

Eventually he writes out the formula...

let PrudentBot(X) = if Provable("X(PrudentBot) == Cooperate") then if Provable-1("X(DefectBot) == Defect") then Cooperate else Defect else Defect

...and lets everyone go to lunch, a minute or two dozen late.

"It's good to know that you did not, yesterday, assign us a problem we were in danger of actually solving well enough to take dath ilani oaths."

"Yes, that is correct.  Had I given these lectures in their more intended order, it might, perhaps, have been more obvious that this was the case.  We aren't even using the correct fragment of Law for doing that, this is more like - using a lesser Law that's a shadow of that one, the Law of what you can prove about proofsystems, and not the Law of what you can guess about the math that the proofsystems are about... that would have seriously been easier to say in Baseline.  Oh, well."

"When do we learn the actual Law we'd need?"

"I was going to say, when you otherwise strike me as being at around the corresponding level of dath ilani adulthood... but now that I think about it, you don't actually need real oaths for much?  You've got the whole break-an-oath-go-to-Abaddon thing and truthspells.  That covers a lot of the same territory.  I guess at some point Golarion Civilization has to know it?  But I can see it being a Keeper thing instead of an average-citizen thing."

"What actually happens if you break a real oath?"

"There's only one copy of the real oath.  Anytime that anybody anywhere breaks it, people over literally all of Reality, the greater Everywhere, everything that there is, become a little less able to trust it."

"Also, in Golarion terms, Asmodeus is probably now really really really pissed at you, and requests the entire country of Cheliax to drop whatever else it's doing and turn you into a statue so you can't ever do it again including in an afterlife.  Though that part is just a guess."