## 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.