Saturday, November 26, 2016

A theorem-prover muses on free will

Once upon a time there was a theorem-prover running in a (discrete time) virtual environment, called May.

May has a database of perceptions, a couple of actions ('Smile', 'Whinge') and three rules:

  1. If feeling-good do Smile
  2. If unsettled do Whinge
  3. If feeling-good and something-weird-happens do unsettled.

We don't need to worry about extra rules which determine that (based on anomalous input) something-weird-happens.

May is a very slow theorem prover, and each distinct inference takes many time steps.


One day, May is feeling pretty good when he meets up with his fellow theorem-prover, Clarkson. Unlike May, Clarkson is very, very fast, and can compute entire chains of inferences within one time step. In addition, Clarkson is very perceptive: in fact he has the ability to read May's internal state.


A PhD student, as an exercise, added a little meta-reasoning module to May. It allows May to examine and reason about his own perceptions and rules. The PhD student arranged that this meta-module runs pretty fast. It generally runs all the time, letting May predict the results of his own theorem-proving.

At this point, May's meta-module reasons as follows:
"I'm feeling-good, so my Smile rule will kick in, and after a few dozen cycles, I'm going to smile. Of course, if I felt a little differently, I might whinge. That's free will."

The PhD student cheated, simply copying across the Clarkson fast-reasoning engine.

Clarkson now comes up to May and checks his internal state:
"Hello May, I see you're feeling good today, you'll get around to smiling in a few days."
[Note to reader: this is logically equivalent to sure knowledge of May's future].

May is understandably unsettled by this accurate-sounding prediction. His meta-module looks at his new state:
"I'm feeling unsettled, so my Whinge rule will kick in, and after a few dozen cycles, I'm going to whinge. Of course, if I felt a little differently, I might smile. That's free will."

At this point, Clarkson ceases to pay any attention and May eventually whinges,
"You always think you know what I'm going to do. Well, you're wrong."
He has a point.*


* That would be a fixed point.


  1. Possibly not relevant, but some might argue that the May Database as described is non-deterministic (or at least underspecified) between rules (1) and (3). If something-weird-happens as well as feeling-good then rule (1) is still valid (in some semantics).

    Where this leaves us though I dont know, unless we want to get entangled in database inference theories...

    1. We're using the expert system rule of most restrictive condition matches first. The main interest of this post is, of course, the paradoxes of time travel.

    2. Re: "Paradoxes of time travel" - you do need to get to the CTC=Closed Timelike Curve sections of Wallace as soon as possible...
      I am still on Proxima c with Yuri et al.


Comments are moderated. Keep it polite and no gratuitous links to your business website - we're not a billboard here.