## She's a Witch!

**Flip** is a logical framework written in
Python. One Flip application is a proof checker for entering and
editing proofs in natural deduction style. Here is a Pythonic example.

F L i P Home
Download
User's guide
Reference
Logics
Code
Tests
Notes
PyPI
GitHub

"There are ways of telling whether she's a witch."

"What do you do with witches?" "Burn them!"

Ax.(Witch(x) -> Burn(x)) (1) Given

"Why do witches burn?" "'Cause they're made of wood!"

Ax.(Wood(x) -> Witch(x)) (2) Given

"How do we tell if she's made of wood?"
"Does wood sink in water?" "It floats!"

Ax.(Floats(x) -> Wood(x)) (3) Given

"What also floats in water?" "A duck!"

Floats(duck) (4) Given

"Exactly! So, logically ..."

"If she weights the same as a duck, she's made of wood!"

Ax.Ay.((Floats(x) & (weight(x) = weight(y))) -> Floats(y)) (5) Given

"We shall use my largest scales. ... Remove the supports!"

weight(duck) = weight(girl) (6) Given

Ay.((Floats(duck) & (weight(duck) = weight(y))) -> Floats(y)) (7) A-Elimination (5)
(Floats(duck) & (weight(duck) = weight(girl))) -> Floats(girl) (8) A-Elimination (7)
Floats(duck) & (weight(duck) = weight(girl)) (9) And-Introduction (4) (6)
Floats(girl) (10) Implication-Elimination (Modus Ponens) (8) (9)
Floats(girl) -> Wood(girl) (11) A-Elimination (3)
Wood(girl) (12) Implication-Elimination (Modus Ponens) (11) (10)

"A witch! A witch!"

Wood(girl) -> Witch(girl) (13) A-Elimination (2)
Witch(girl) (14) Implication-Elimination (Modus Ponens) (13) (12)

"Burn her! Burn!"

Witch(girl) -> Burn(girl) (15) A-Elimination (1)
Burn(girl) (16) Implication-Elimination (Modus Ponens) (15) (14)

This is the output from the checker. Here is
the proof script
(more here).

F L i P Home
Download
User's guide
Reference
Logics
Code
Tests
Notes
PyPI
GitHub
Summary