version with subtitles

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

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

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 PonensBurn!! Burn!!

- 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) `Prop2`by first establishingBw:

can_build_bridge_with(woman).

(presumably by attempting to do this) `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