The New Turing Omnibus Chapter 58 Predicate Calculus

Preamble

As Tom kindly volunteered to shepherd the group this meeting, we first circulated his notes and some copies of the chapter (after a few rounds of Crossy Road on Geckoboard's new Apple TV).

The Chapter

Learning from our struggle to see the big picture last meeting, we began by going through Tom's notes, specifically "The big picture" and "The main pieces" to immediately set the scene.

We then jumped to Tom's example proof, working through resolution using a simpler problem than the one given in the chapter, specifically:

• Axioms:
  • All humans are mortal;
  • Socrates is human.
• Theorem:
  • Socrates is mortal.

Tom led us through the expression of the problem in predicate calculus then its clausal form before showing how we could take a negation of the theorem (in this example, that Socrates is not mortal) and mechanically use resolution to arrive at a proof by contradiction. We initially skimmed the details to ensure we had the gist of the matter before diving into the problem more deeply.

The first topic to cover was predicate calculus itself (or "first-order logic"), reviewing the specific notation used in the chapter and its meaning. We spent some time explaining implication with several practical examples from Tom's notes:

NightTime(x) → Dark(x)

• If it's night time then it must be dark;
• If it's not dark then it must not be night time;
• If it's not night time then we don't know whether it's dark;
• If it's dark then we don't know whether it's night time.

We then worked through the translation of our predicate calculus into clausal form by working through the following transformations:

• X → Y = ~(X ∧ ~Y) = ~X ∨ Y (touching on De Morgan's laws)
• ∃y(LT(x, y)) = LT(x, f(x)) (Skolemization)
• Moving ∀ to the left (renaming variables as needed) and then removing it as it is implied

This lead us to convert our problem into conjunctive normal form and therefore suitable for resolution.

We then stepped through the resolution of our problem by trying to produce clauses that shared the same predicate (using unification where necessary), e.g. ~X and X, so that we could combine them (and hopefully arrive at a contradiction).

With the Socrates example thoroughly completed, we spent the remaining time working through the much more complicated example of the man, the wolf, the goat and the cabbage.

Retrospective

• Feedback was almost universally positive with many people praising Tom's efforts to distill a dense chapter into something digestible for a single meeting;
• The suggestion was floated that we might want to spend longer than one meeting on a chapter but there was some resistance due to our past experience spending many months on the same book (and how this may have put off newcomers);
• Tom noted that it took a lot of his time to prepare for the meeting and this might make the act of shepherding off-putting for others.

Show & Tell

Chris talked about his work on a new language called "Sentient" as a means of expressing first-order logic problems at a high level of abstraction which could then be automatically solved by a SAT solver.

Thanks

Thanks to Leo & Geckoboard for hosting and to Tom for his enormous efforts both in preparing for and running the meeting.