# Tag Archives: Logic

# Logic in a box!

Having recently spent some time teaching a short course on logic and critical thinking, here is the core of the course reduced down to a box of 54 cards. These include:

- 15 logic cards (summarising basic syllogistic and propositional logic rules),
- 19 cards illustrating logical fallacies,
- 5 cards for testing your ability to check validity, and
- 15 logic-puzzle cards.

If you’re interested, more details can be downloaded from the game page (see the links in the “Downloads” section). The picture below shows some of the cards:

# L.E.J. Brouwer, fifty years later

Luitzen Egbertus Jan Brouwer (27 February 1881 – 2 December 1966) was a Dutch mathematician who founded intuitionism and made important contributions to topology, such as his fixed-point theorem, which states that every continuous function *f* mapping a compact convex set into itself has a fixed point *a* [i.e. *f*(*a*) = *a*]. A consequence of the theorem is when a crumpled sheet of paper is placed on top of (and within the boundaries of) a copy of itself, at least one point on the top sheet lies over the corresponding point on the bottom sheet.

Brouwer had a huge impact on mathematics and logic in the Netherlands, influencing people such as Arend Heyting (student), Dirk van Dalen (grandstudent), and Henk Barendregt (great-grandstudent).

The Dutch Royal Mathematical Society (*Koninlijk Wiskundig Genootschap*) is organising a special event marking 50 years since Brouwer’s death. The event is on 9 December in the Amsterdam Science Park. It looks to be an interesting event. Details here.

# Sequent Calculus in NetLogo

NetLogo programs sometimes require agents to reason, and one of the simplest forms of reasoning is the sequent calculus. This uses expressions of the form α, β, γ, δ ⊢ ε, ζ, η which are interpreted as α ˄ β ˄ γ ˄ δ ⇒ ε ˅ ζ ˅ η. That is, all the hypotheses α, β, γ, δ are assumed to be true, and from that it should follow that at least one of the conclusions ε, ζ, η is true.

We can resolve the truth of sequents like α, β, γ, δ ⊢ ε, ζ, η using rules which simplify occurrences of ¬ φ (**not** φ), φ ˄ ψ (φ **and** ψ), φ ˅ ψ (φ **or** ψ), and φ ⇒ ψ (φ **implies** ψ) occurring in the hypotheses and/or conclusions, until we are left with a number of sequents like α, β, γ, δ ⊢ ε, ζ, η containing only atomic formulae. Such an expression is true if one of the atomic formulae on the left also occurs on the right (or, in more advanced versions of the logic, if the atomic formulae on the left somehow imply one of the atomic formulae on the right, in the way that *x* = *y* and *y* = *z* imply *x* = *z*).

The simplification rules are as follows. Note that some rules generate two new sequents, and that the rule for **not** flips things from the hypotheses to the conclusions or vice versa:

We can code these up easily in NetLogo, using the list `[ "and" φ ψ ]`

to represent φ ˄ ψ, and so forth. The following function takes 4 lists (atomic and non-atomic hypotheses; atomic and non-atomic conclusions) and applies the simplification rules to the hypotheses (with some printing for debugging):

```
to-report sequent-prove-a [ atomic-hyp non-at-hyp atomic-conc non-at-conc ] ; split hypotheses
nice-print "a" atomic-hyp non-at-hyp atomic-conc non-at-conc ""
ifelse (non-at-hyp = [])
[ report sequent-prove-b atomic-hyp atomic-conc non-at-conc ]
[ let p (first non-at-hyp)
set non-at-hyp (but-first non-at-hyp)
ifelse (is-string? p) ; atomic
[ report sequent-prove-a (fput p atomic-hyp) non-at-hyp atomic-conc non-at-conc ]
[ ifelse (first p = "not") ; not q
[ let q (item 1 p)
report sequent-prove-a atomic-hyp non-at-hyp atomic-conc (fput q non-at-conc) ]
[ ifelse (first p = "and") ; q /\ r
[ let q (item 1 p)
let r (item 2 p)
report sequent-prove-a atomic-hyp (fput q (fput r non-at-hyp)) atomic-conc non-at-conc ]
[ ifelse (first p = "or") ; q \/ r
[ let q (item 1 p)
let r (item 2 p)
report (sequent-prove-a atomic-hyp (fput q non-at-hyp) atomic-conc non-at-conc)
and (sequent-prove-a atomic-hyp (fput r non-at-hyp) atomic-conc non-at-conc) ]
[ ifelse (first p = "implies") ; same as (not q) \/ r
[ let q (item 1 p)
let r (item 2 p)
report (sequent-prove-a atomic-hyp (fput r non-at-hyp) atomic-conc non-at-conc)
and (sequent-prove-a atomic-hyp non-at-hyp atomic-conc (fput q non-at-conc)) ]
[ error "Unexpected logical" ]
]
]
]
]
]
end
```

Once all hypotheses are atomic, the following function applies the simplification rules to the conclusions (for some cases it must call `sequent-prove-a`

again):

```
to-report sequent-prove-b [ atomic-hyp atomic-conc non-at-conc ] ; split conclusions
nice-print "b" atomic-hyp [] atomic-conc non-at-conc ""
ifelse (non-at-conc = [])
[ report sequent-prove-c atomic-hyp atomic-conc ]
[ let p (first non-at-conc)
set non-at-conc (but-first non-at-conc)
ifelse (is-string? p) ; atomic
[ report sequent-prove-b atomic-hyp (fput p atomic-conc) non-at-conc ]
[ ifelse (first p = "not") ; not q
[ let q (item 1 p)
report sequent-prove-a atomic-hyp (list q) atomic-conc non-at-conc ]
[ ifelse (first p = "and") ; q /\ r
[ let q (item 1 p)
let r (item 2 p)
report (sequent-prove-b atomic-hyp atomic-conc (fput q non-at-conc))
and (sequent-prove-b atomic-hyp atomic-conc (fput r non-at-conc)) ]
[ ifelse (first p = "or") ; q \/ r
[ let q (item 1 p)
let r (item 2 p)
report sequent-prove-b atomic-hyp atomic-conc (fput q (fput r non-at-conc)) ]
[ ifelse (first p = "implies") ; same as (not q) \/ r
[ let q (item 1 p)
let r (item 2 p)
report sequent-prove-a atomic-hyp (list q) atomic-conc (fput r non-at-conc) ]
[ error "Unexpected logical" ]
]
]
]
]
]
end
```

Once both hypotheses and conclusions are atomic, checking truth just needs a simple intersection test:

```
to-report sequent-prove-c [ atomic-hyp atomic-conc ]
let proved? false
foreach atomic-conc [
if ((not proved?) and member? ? atomic-hyp) [ set proved? true ]
]
ifelse (proved?)
[ nice-print " c" atomic-hyp [] atomic-conc [] " ** proved **" ]
[ nice-print " c" atomic-hyp [] atomic-conc [] " failed!" ]
report proved?
end
```

Printing requires some code to make sequents look nice:

```
to-report nice-item [ p ]
ifelse (is-string? p)
[ report p ]
[ ifelse (first p = "not")
[ let q (item 1 p)
report (word "~ " (nice-item q)) ]
[ ifelse (first p = "and")
[ let q (item 1 p)
let r (item 2 p)
report (word "(" (nice-item q) " ^ " (nice-item r) ")") ]
[ ifelse (first p = "or")
[ let q (item 1 p)
let r (item 2 p)
report (word "(" (nice-item q) " v " (nice-item r) ")") ]
[ ifelse (first p = "implies")
[ let q (item 1 p)
let r (item 2 p)
report (word "(" (nice-item q) " -> " (nice-item r) ")") ]
[ error "Unexpected logical" ]
]
]
]
]
end
to-report nice-list [ p ]
ifelse (p = [])
[ report "" ]
[ report (reduce [ (word ?1 ", " ?2) ] (map nice-item p)) ]
end
to nice-print [ lab x y z w t]
if (verbose?) [
print (word lab ": " (nice-list (sentence x y)) " |- " (nice-list (sentence z w)) t)
]
end
```

For demonstration purposes, the **go** button computes some basic facts about two turtles, combining this with a user-supplied list of hypotheses, and tries to prove a user-supplied conclusion (in this case `[ "and" [ "implies" "C" "F" ] [ "not" [ "not" "Far" ] ] ]`

, representing (C ⇒ F) ˄ ¬ ¬ Far.

```
globals [
computed-facts
result?
]
to go
if (verbose?) [ print "------------------------------------------------------------------------" ]
clear-all
ask patches [ set pcolor white ]
create-turtles 1 [ set color blue set size 3 set shape "person" setxy random-xcor random-ycor ]
create-turtles 1 [ set color red set size 2 set shape "person" setxy random-xcor random-ycor ]
set result? "?"
ask (turtle 0) [ compute-basic-facts ]
let hypotheses (sentence computed-facts (read-from-string other-hypotheses))
set result? sequent-prove-a [] hypotheses [] (list (read-from-string conclusion))
end
to compute-basic-facts ; calculated by a specific turtle
let fact1 (ifelse-value (xcor < 0) [ "Left" ] [ "Right" ])
let d (distance (turtle 1))
let fact2 (ifelse-value (d < 4) [ "Near" ] [ "Far" ])
set computed-facts (list fact1 fact2)
end
```

The NetLogo interface is shown at the top of this page, and the code is at Modelling Commons. The simple sequent calculus reasoner presented here can be fairly easily extended with quantifiers and other features that might be necessary.

See also my other NetLogo tutorials.