Logical Analysis of Monty Python's Witch Scene from the Holy Grail.

The Skit

In which Bedevere (soon to be Sir Bedevere) uses logical inference to help the people figure out if a certain woman is indeed a witch, and therefore that they should burn her.
version with subtitles

Basic rules of inference.

We will be using the following fundamental rules of inference:

Modus Ponens (MP)

Established ca. 370BC by Artistotle et al., clearly well known by the middle ages.

X.
X->Y.
------
Y.

Modus Bogus (MB)

This rule seems to have been developed prior to the middle ages, possibly by Bedevere himself, but clearly in common usage by the time of the witch-hunt depicted in the video. References to this rule of inference are notably lacking from the literature.

Y.
X->Y.
------
X.

The Analysis

We have the following premisses

W:	same_weight(woman,duck).	(according to the scale)
F:	same_weight(X,Y) and floats(Y) -> floats(X).	(false premiss, possibly acceptable in middle ages)
Df:	floats(duck).	(premiss - OK most ducks float)
Wf:	is_wood(X)->floats(X).	(premiss - OK most woods float)
Wob:	is_wood(X)->burns(X).	(premiss - OK most woods burn)
Wib:	is_witch(X)->burns(X).	(premiss - questionable...)

We can derive the following theorem

T1:is_wood(X)->is_witch(X).

Proof:
A1: is_wood(X).
P1: burns(X).  (A1 and Wob by Modus Ponens)
witch(X).  (P1 and Wib by Modus Bogus)

We can now prove the following propositions:

Prop1: floats(woman).
Proof:
F and Df and W using Modus Ponens

Prop2: is_wood(woman).
Proof:
Prop1 and Wf using Modus Bogus

Prop3: is_witch(woman).
Proof:
Prop2 and T1 using Modus Ponens

Burn!! Burn!!

Alternate Derivations

An alternate derivation of Prop2 was proposed by the people, but rejected by Bedevere (creaky-facemask-guy, soon to be Sir Bedevere):
Wb:
is_wood(X)->can_build_bridge_with(X).
(premiss - OK most wood can be used for bridges)
From which the people thought they could derive Prop2 by first establishing
Bw:
can_build_bridge_with(woman).
(presumably by attempting to do this)
And then proving Prop2 using Bw and Wb using MB. However, this was rejected, although it is unclear why since the same logic was using to prove Prop2 using Wf and MB. However, it is possible that Bedevere rejected this because was not familiar with the medieval experimental technique of building a bridge out of her.
The people also proposed an alternate derivation of Prop1 by simply establishing this fact using the medieval experimental technique of throwing her into the pond. This was also rejected by Bedevere, presumably due to the availability of his largest scales, a far more precise measurement tool than throwing her into the pond.
Finally, a more concise derivation that everyone in the skit seem to have missed, was provided by Robby Goetschalckx:
```
T1: True.
T2: False -> True
```
These both hold, verify by checking truth tables. Very short truth tables.
Modus bogus then gives us:
```
T3: False
```
Then, since we have False -> P for any proposition P, we get:
```
T4: False -> (is_witch(woman))
```
T3, T4 and modus ponens give:
```
is_witch(woman)
```

Here is some Prolog code to implement the premisses. However, the lack of Modus Bogus in Prolog (why?) means we can't make any valid inferences in this case:

%%would really like to put this here:
%:- include('modusbogus.pl').

same_weight(woman,duck).
is_wood(bridge).
floats(duck).

floats(X):-same_weight(X,Y),floats(Y).

floats(X):-is_wood(X).

burns(X):-is_wood(X).

burns(X):-is_witch(X).

A detailed counter proof by Yannis Haralambous demonstrating the reasoning in the film is fallacious, and reviewing the proof shown above.

Last modified: Fri Jan 25 14:11:24 EST 2013