ARC-1.ipynb

Kernel: Haskell

Inference using all, verbs, and relative clauses:

A worksheet on the semantics and the proof system.

by Lawrence S. Moss

Enter the line below to get started.

To enter any of the gray boxes, click on the box, hold down the shift key and then enter 'return'.

If the Haskell kernel dies during your session, you will need to re-enter this line.

:l AllVerbsRelativeClauses.hs

Syntax of the fragment

category	construction
noun n	dogs, cats, birds, skunks, mammals, animals, chordates, sneetches, boys, girls
verb v	admire, hate, help, love, see
term t	n, v all t
sentence s	all t u

Sentences in this notebook have to be constructed according to the syntax above. But to make things more readable, you can add the words who, are, and also anywhere you like. In other words, those words are dropped by the parser. You also can make the verb singular or plural.

To help you see if an input sentence is ok for this fragment, you can enter it in the box below. If you get a red error, it's seriously out of range.

syntaxCheck "all who admire all skunks love all who see all mammals"
syntaxCheck "all who admire all skunks love all who see all mammals"
syntaxCheck "some who admire all skunks love all who see all mammals"
syntaxCheck "junk who see all skunks love all mammals"

Semantics of the fragment

We next present the main semantic definition for our language.

The language is interpreted in models. A model $\mathcal{M}$ is a set $M$, together with interpretations $[\![p]\!]$ of the basic nouns $p$ (the animal names) as subsets of $M$ and the basic verbs $r$ as sets of pairs of elements of $M$.

Here are two models, called testModel1 and testModel2. Start by either entering the cell below. You also may enter your own models by copying and modifying the box below.

import Models
import Syntax2

testNouns1 =
    [ M Cats     [1,2,3,4],
      M Dogs     [4,5,6],
      M Skunks   [1,2,5,6], 
      M Sneetches  [7],
      M Chordates [1,2,3,4,5,6],
      M Mammals []
    ]
    
testVerbs1 = 
    [ Vb Sees [(1,1),(1,4),(3,4),(2,5), (3,5), (3,6), (3,7)],
      Vb Admires [(6,2), (4,1), (4,2), (4,3), (7,7)],
      Vb Helps  [(1,1), (2,2), (3,3), (4,5), (5,6)],
      Vb Loves [],
      Vb Hates [(6,7)]
    ]    

testModel1 = Model 
    {Models.universe = [1,2,3,4,5,6,7], 
     cnDict = testNouns1, 
     verbDict = testVerbs1 
    }
    
testNouns2 =
    [ M Cats     [3,4],
      M Dogs     [],
      M Skunks   [1,2], 
      M Sneetches  [],
      M Chordates [1,2,3,4],
      M Mammals []
    ]
    
testVerbs2 =
    [ Vb Sees [(1,1),(1,4),(3,4)],
      Vb Admires [(2,2), (1,1), (3,4), (4,3)],
      Vb Helps  [],
      Vb Loves [(1,3),(1,4)],
      Vb Hates [(2,4),(4,2)]
    ]    

testModel2 = Model 
    {Models.universe = [1,2,3,4], 
     cnDict = testNouns2, 
     verbDict = testVerbs2 
    }

You also may define your own models, by inserting a new cell, copying the box above into it, changing the names of the interpretation functions for the nouns, the verbs, and the model.

Here is a function which displays models.

showModel testModel1

In every model $\mathcal{M}$, we have an interpretation $[\![t]\!]$ of each term $t$.

For $t$ atomic, the model itself tells us the interpretation.

And given $[\![t]\!]$, we define ParseError: KaTeX parse error: Unexpected end of input in a macro argument, expected '}' at end of input: [\![\mbox{r$all$tParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲]\!] by

$$[\![\mbox{$r$all$tParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲]\!] = \{ x\in…y\in [![t]!]$,$(x,y)\in [![r]!]ParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲\}.$

Notice that this is an inductive definition.

The next function termEval takes two arguments, a term and then a model.

The term be a legal term in the current fragment.

The function termEval gives the interpretation of this term in the model.

You can enter or change the arguments to termEval. And again, you can also change make your own models and then test them.

termEval "hate all sneetches" testModel1
termEval "see all who hate all sneetches" testModel1
termEval "hate all see all sneetches" testModel2
termEval "dogs" testModel1
termEval "see all mammals" testModel1

We have just seen the interpretation $[\![t]\!]$ of a term $t$ in a given model $M$. And then we can define what it means for a sentence All $t$ $u$ to be true in $M$. Of course, it means that $[\![t]\!] \subseteq [\![u]\!]$.

The next function evaluate takes two arguments, a sentence and a model. The sentence must be a legal sentence in the current fragment. The function evaluate tells whether the input sentence is True or False in the model.

evaluate testModel1 "all who admire all sneetches loves all skunks"
evaluate testModel1 "all who help all sneetches are sneetches"
evaluate testModel2 "all who see all dogs are cats"
evaluate testModel1 "all who see all who love all dogs are cats"

Examples of derivations in the logical system

The rules of the logical system:

$$\frac{}{\mbox{all $x$are$xParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲}\quad Axiom $

$$\frac{\mbox{all $x$are$yParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲ \qquad \mbox{a…y$are$zParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲}{\mbox{all x$are$zParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲}\quad Barbara $

$$\frac{\mbox{all $x$are$yParseError: KaTeX parse error: Expected 'EOF', got '}' at position 1: }̲}{\mbox{all (r$all$y$) ($r$all$xParseError: KaTeX parse error: Expected 'EOF', got '}' at position 2: )}̲}\quad Anti $

Examples of counter-models

The main function that shows off the proof system and the counter-model algorithm is followsInARC.

We are going to illustrate it first, and then afterwards we'll turn to some explanation.

You can click on the examples, and also modify them.

The first argument to followsInARC must be a list of sentences. (Lists in Haskell are enclosed by brackets [ and ], and the items are separated by commas.) These sentences are the assumptions. The second argument is a single sentence. It is the conclusion.

assumptionList = ["All skunks are mammals"]
followsInARC assumptionList "All who see all who love all mammals see all who love all skunks"

assumptionList = ["All dogs love all who see all cats"]
followsInARC assumptionList  "All dogs see all who love all cats"

assumptionList = ["All skunks are mammals"]
followsInARC assumptionList  "all who love all skunks love all mammals"

assumptionList = ["all who love all skunks love all mammals"] 
followsInARC assumptionList  "All skunks are mammals"

-- My favorite example

followsInARC ["All skunks are mammals"] "all who see all who love all mammals see all who love all skunks"

-- You can enter the assumptions one-by-one, as below.
-- Then put them in a list when you call the function.

a1 = "all who see all dogs are sneetches" 
a2 = "all sneetches are chordates"
a3 = "all who admire all who see all dogs are cats"
followsInARC [a1,a2,a3] "all who love all chordates are cats" 

-- You also can list the assumptions one-on-a-line:

followsInARC ["all who see all skunks love all mammals",    
              "all who see all who hate all skunks see all mammals"] 
              "all who see all mammals hate all see all skunks"

-- You can do without assumptions: [] is the empty list.

followsInARC [] "all who see all dogs see all dogs"

followsInARC []
  "all who see all who love all who admire all who hate all who see all skunks are mammals"

followsInARC  ["all boys hate all skunks", 
               "all skunks see all skunks", 
               "all who love all mammals are skunks", 
               "all girls see all who love all skunks", 
               "all who see all boys are mammals", 
               "all who see all boys see all skunks", 
               "all who see all skunks love all skunks"]  
          "all who see all who hate all skunks see all who love all mammals" 

followsInARC  ["all boys hate all skunks"] "all who see all who hate all skunks also see all boys"

Original artwork by Jeffrey Fine

https://www.jeffreyfineart.com