SharedARC.ipynbOpen in CoCalc
Logic of 'All' + verbs + relative clauses

Inference using all, verbs, and relative clauses:

A worksheet on the semantics and the proof system.

drawing

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"

Looks good!
Looks good!
Sorry, not in the fragment of this notebook
Sorry, invalid input

Semantics of the fragment

We next present the main semantic definition for our language.

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

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,3,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
The universe is the set of numbers in [1,2,3,4,5,6,7]. The nouns are interpreted as follows: Noun | Interpretation ----------+----------------- cats | 1, 2, 3, 4 dogs | 4, 5, 6 skunks | 1, 3, 5, 6 sneetches | 7 chordates | 1, 2, 3, 4, 5, 6 mammals | The transitive verbs are interpreted as follows: Verb | Interpretation -------+------------------------------------------------ see | (1,1), (1,4), (3,4), (2,5), (3,5), (3,6), (3,7) admire | (6,2), (4,1), (4,2), (4,3), (7,7) help | (1,1), (2,2), (3,3), (4,5), (5,6) love | hate | (6,7)

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

For tt atomic, the model itself tells us the interpretation.

And given [[t]][\![t]\!], we define by

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 dogs" testModel1

[6]
[3]
[]
[4,5,6]
[3]

We have just seen the interpretation [[t]][\![t]\!] of a term tt in a given model MM. And then we can define what it means for a sentence All tt uu to be true in MM. Of course, it means that [[t]][[u]][\![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"

drawing

Examples of derivations in the logical system

The rules of the logical system:

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 love all skunks love all mammals"
The given sentence is not provable from the assumptions in ARC. Here is a counter-model: The universe is the set of numbers in [0,1,2,3]. The nouns and verbs are interpreted as follows: Noun | Interpretation --------+--------------- skunks | 0 mammals | 0, 1 Verb | Interpretation -----+-------------------- love | (2,0), (3,0), (3,1) Extra information on the relevant terms: Term | Interpretation -----------------+--------------- skunks | 0 mammals | 0, 1 love all skunks | 2, 3 love all mammals | 3 Here is how the assumptions and purported conclusion fare in this model: Sentence | Truth Value ----------------------------------------------+------------ all skunks are mammals | True all who love all skunks also love all mammals | False The model is built using the sentences below, all of which do follow from the assumptions: all skunks are mammals all who love all mammals also love all skunks all skunks are skunks all mammals are mammals all who love all skunks also love all skunks all who love all mammals also love all mammals
assumptionList = ["All skunks are mammals"]
followsInARC assumptionList  "all who love all mammals love all skunks"
The conclusion follows from the assumptions in ARC. Here is a derivation: 1 all skunks are mammals assumption 2 all who love all mammals also love all skunks anti 1
-- My favorite example

followsInARC ["All skunks are mammals"] "all who see all who love all skunks see all who love all mammals"
The conclusion follows from the assumptions in ARC. Here is a derivation: 1 all skunks are mammals assumption 2 all who love all mammals also love all skunks anti 1 3 all who see all who love all skunks also see all who love all mammals anti 2
-- 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 love 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"

The given sentence is not provable from the assumptions in ARC. Here is a counter-model: The universe is the set of numbers in [0,1,2,3,4,5,6,7]. The nouns and verbs are interpreted as follows: Noun | Interpretation --------+--------------- skunks | 1 mammals | 3 Verb | Interpretation -----+--------------------------- see | (0,1), (4,3), (4,5), (6,3) love | (0,3), (2,3) hate | (5,1), (7,0) Extra information on the relevant terms: Term | Interpretation ----------------------------+--------------- see all skunks | 0 skunks | 1 love all mammals | 0, 2 mammals | 3 see all who hate all skunks | 4 hate all skunks | 5 see all mammals | 4, 6 hate all who see all skunks | 7 Here is how the assumptions and purported conclusion fare in this model: Sentence | Truth Value ---------------------------------------------------------+------------ all who see all skunks also love all mammals | True all who see all who hate all skunks also see all mammals | True all who see all mammals also hate all who see all skunks | False The model is built using the sentences below, all of which do follow from the assumptions: all who see all skunks also love all mammals all who see all who hate all skunks also see all mammals all skunks are skunks all mammals are mammals all who see all skunks also see all skunks all who see all mammals also see all mammals all who love all mammals also love all mammals all who hate all skunks also hate all skunks all who see all who hate all skunks also see all who hate all skunks all who hate all who see all skunks also hate all who 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 mammals hate all skunks", 
               "all skunks see all skunks", 
               "all who love all mammals are skunks", 
               "all boys 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" 
The conclusion follows from the assumptions in ARC. Here is a derivation: 1 all boys see all who love all skunks assumption 2 all boys see all who love all skunks assumption 3 all skunks see all skunks assumption 4 all who see all skunks also love all skunks assumption 5 all skunks love all skunks barbara 3, 4 6 all who see all who love all skunks also see all skunks anti 5 7 all who see all skunks also love all skunks assumption 8 all who see all who love all skunks also love all skunks barbara 6, 7 9 all boys love all skunks barbara 2, 8 10 all who see all who love all skunks also see all boys anti 9 11 all who see all boys are mammals assumption 12 all mammals hate all skunks assumption 13 all who see all boys also hate all skunks barbara 11, 12 14 all who see all who love all skunks also hate all skunks barbara 10, 13 15 all boys hate all skunks barbara 1, 14 16 all who see all who hate all skunks also see all boys anti 15 17 all who see all boys also see all skunks assumption 18 all who love all mammals are skunks assumption 19 all who see all skunks also see all who love all mammals anti 18 20 all who see all boys also see all who love all mammals barbara 17, 19 21 all who see all who hate all skunks also see all who love all mammals barbara 16, 20
drawing