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

"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