Adding sentential connectives

When we consider the internal structure of sentences, in particular those involving the sentential connectives and, or and not, we see that the truth conditions of these complex sentences are predictable from the atomic sentences they contain and the ways in which these are combined with the connectives.

This ‘semantic’ story is mirrored in the inferences we draw: by and large, if someone believes “Water boils at 212F and Grass is green” then they will also believe “Grass is green.” Although I have here appealed to mysterious beliefs, we can understand this as a convenient way of asserting that under a wide variety of possible testing procedures, people will behave in a manner consistent with the attribution of these beliefs to them. (For example, we could just ask them what they believe.) The interest of these inferences is that they are systematic: whenever we have the word and connecting two sentences, regardless of what those sentences may be, these inferences obtain. This detail was ignored in our previous treatment of language.

TL/DR

The code for this post is downloadable here, if you would like to run it. Please do not just copy and paste from this post!

Here we extend the language of last time with sentential connectives.

Please:

1. Try to understand the ideas.

2. Play with the code.

   I have defined a(n easy to write) helper function:

   iTP :: PropInt PropSit -> [Int] -> Bool
   iTP phi = isTrueProp phi . charFunc
   

3. Ask questions.

   • how might you add another sentential connective, perhaps if..then? It might be best to give it a non discontinuous name, like ‘implies’…

Sentences

Among the infinitely many possible (distinct) sentences, we now observe that there are systematicities in their form and use. Whereas before, we simply treated the sentences “John sings” and “John sings and John dances” as distinct primitives, and were puzzled when they did not behave as we predicted, now we would like to revise our theory to account for their behaviour.¹ One option, which we will not pursue in this case, but will adopt in others, is to change not our analysis but what we count as a relevant situation for the purposes of calculating entailment. We could simply stipulate that we are only interested in those situations which do not make “John sings” false and “John sings and John dances” true. While this would work in the present case, it would not deal with any of the infinitely many other pairs of sentences related via entailment in this way. To deal with them in this approach would require imposing each time a new restriction on relevant situations. If we had no other alternative, we would have to grit our teeth and settle for this uninsightful finite approximation. Luckily, (as you surely remember from your Mathematischen Grundlagen course) we do have alternatives. Before getting into them, I want to emphasize what is right about this rejected solution. This solution diagnoses the problem correctly (given our current semantic definition of entailment). The problem is that the situations we consider are not required to relate the truth of the sentences “John sings” and “John sings and John dances.” Thus, neither entails the other. The solution is to find some way to exclude those situations from consideration that assign “impossible” truth values to these sentences. This is what our rejected solution gets right. What is wrong with our rejected solution is that it simply stipulates this relation. We would like to have a better way of doing this.

The strategy we will pursue will be to refine our syntactic analysis of sentences, so that we can implement some systematic relationships between sentences as syntactic ones. What we are interested in at the moment are the so-called Boolean (sentential) connectives, and, or, and not. We again use the class system of Haskell to allow us to write terms using these words.²

class SentConn b where
  and :: b -> b -> b
  or :: b -> b -> b
  not :: b -> b

A type is an instance of this class just in case we can provide definitions for the functions and, or and not in this type. A really easy (but meaningless) example is given by the unit type.

instance SentConn () where
  () `and` () = ()
  () `or` () = ()
  not () = ()

It becomes interesting for us when we demand that a type support both the SentConn class functions and the Prop class functions. The sentence “Either (\(P_{0}\) and \(P_{1}\)) or not \(P_{2}\)” (in more canonical logical syntax: \((P_{0} \wedge P_{1}) \vee \neg P_{2}\)) can be written in Haskell as the term (p 0 `and` p 1) `or` not (p 2). This term has type (SentConn a,Prop a) => a, which we should read as saying:

any type which can interpret both sentential connectives and propositions can interpret this term

A more meaningful, but not at all ‘semantic’ instance of the class can be given by numbers. There are lots of ways to interpret a term as a number, but a useful one counts the depth of a term. We begin with an informal definition of the depth of a term.

1. The depth of an atomic sentence \(p_{i}\) is one
2. The depth of a negation \(\neg \phi\) is one greater than the depth of \(\phi\)
3. The depth of a conjunction \(\phi \wedge \psi\) (or a disjunction \(\phi \vee \psi\)) is one greater than the deeper of the two conjuncts

The depth of a term measures its complexity, in the sense that the deeper a term, the more logical operations have been applied to an atomic sentence.

To implement this in Haskell, it is convenient not to use integers directly, but to define a new type which is equivalent to integers.

newtype Depth = Depth Int deriving (Eq,Ord)

We declare that it is an instance of the SentConn class by defining how the sentential connectives affect the depths of their arguments.

instance Prop Depth where
  p _ = Depth 1
instance SentConn Depth where
  not (Depth i) = Depth (1 + i)
  Depth i `and` Depth j = Depth (1 + max i j)
  Depth i `or` Depth j = Depth (1 + max i j)

It is useful to define a new type Depth instead of using integers because there are other reasonable things that we might want to do with integers, such as to calculate the size of a term, which is the number of logical operators (sentential connectives) that appear in them.

newtype Size = Size Int deriving (Eq,Ord)
instance Prop Size where
  p _ = Size 0
instance SentConn Size where
  not (Size i) = Size (1 + i)
  Size i `and` Size j = Size (1 + i + j)
  Size i `or` Size j = Size (1 + i + j)

Perhaps we would like to count the number of atomic propositions in a term.

newtype NumAtoms = NumAtoms Int deriving (Eq,Ord)
instance Prop NumAtoms where
  p _ = NumAtoms 1
instance SentConn NumAtoms where
  not (NumAtoms i) = NumAtoms i
  NumAtoms i `and` NumAtoms j = NumAtoms (i + j)
  NumAtoms i `or` NumAtoms j = NumAtoms (i + j)

In a previous post, we introduced abbreviations for a handfull of our sentence terms. Now, we can revise this, having found a way to express syntactic relatedness.

john_sings, john_dances, john_praises_mary, mary_praises_john, mary_sings, mary_dances, john_doesn't_sing, john_sings_and_dances, john_sings_and_john_dances, john_sings_or_john_doesn't_sing, john_sings_or_doesn't_sing :: (Prop b,SentConn b) => b
john_sings = p 0
john_dances = p 1
john_praises_mary = p 2
mary_praises_john = p 3
mary_sings = p 4
mary_dances = p 5
john_doesn't_sing = not (p 0)
john_sings_and_dances = p 7
john_sings_and_john_dances = p 0 `and` p 1
john_sings_or_john_doesn't_sing = p 0 `or` not (p 0)
john_sings_or_doesn't_sing = p 10

Of course, there are many more regularities in the above sentences that we are not yet able to express.

Truth in a Situation

We have previously used the type PropInt as our intended model of propositions. In general, it is often a good strategy to try to reuse the tools you already have, before you develop something completely new. (If you can show that your previous tools will not work at all, you have also learned something important!) We would like to show that our intended model of propositions, the type PropInt, supports sentential structure.

Let us think about how conjunction, disjunction, and negation of sentences work. A conjunction of two sentences is true in a situation, just in case each conjunct sentence is true in that situation. Similarly, a disjunction of two sentences is true in a particular situation, just in case one of the disjuncts is. Finally, the negation of a sentence is true in a situation, just in case the sentence negated is not true in that situation. Recalling that a PropInt s is (morally) a function from situations to truth values, we can interpret our connectives in this type by translating the above intuitions into code.

instance SentConn (PropInt s) where
  phi `and` psi = PropInt (\sit -> (phi `isTrueProp` sit) && (psi `isTrueProp` sit))
  phi `or`  psi = PropInt (\sit -> (phi `isTrueProp` sit) || (psi `isTrueProp` sit))
  not phi = PropInt (\sit -> neg (phi `isTrueProp` sit))
    where
      neg True = False
      neg False = True

To expand on this code, consider the instance implementation for and. It defines the conjunction of two objects phi and psi of type PropInt as a function that takes a situation argument sit, evaluates the first PropInt phi in the situation, obtaining a truth value, evaluates the second PropInt psi in the same situation, obtaining a truth value, and then checks whether both are true (by conjoining them).

This is all we need to do! As we have previously defined the function isTrueProp to map a PropInt and a situation to a truth value, any way of delivering a PropInt to this function is acceptable. By showing how PropInt supports sentential connective structure, we are able to interpret expressions with sentential connectives as being of type PropInt.

We can make predictions about which sentences are true in which ‘situations’.

> iTP john_sings [1]
False
> iTP john_dances [1]
True
> iTP (john_dances `and` john_sings) [1]
False
> iTP (john_dances `or` john_sings) [1]
True

Here a situation can be thought of as being described by a list of the atomic propositions (given by their integer index) which are true in that situation. In the above, the situation described by the list [1] is one where john dances (recall above that we have defined john_dances as a shorthand for the term p 1) and nothing else (i.e. no other atomic proposition) is true.

Validity

Our validity checker (isValidProp) worked by interpreting a term both in the domain of WhichAtoms and in the domain of PropInt. In other words, the validity checker needed to know not only what the semantic interpretation of the term was (in the sense of what function from situations to truth values it denoted), but it also needed to know which atoms were in the term, so that it could construct all of the relevant situations. To this end, we interpreted terms as lists of the atomic propositions they contained (i.e. lists of integers). We defined a new type, called WhichAtoms, which was really just a list of integers.

newtype WhichAtoms = WhichAtoms [Int]

Previously, our terms were just atomic sentences, and so determining which atomic sentences were contained in a term was quite trivial.

instance Prop WhichAtoms where
  p n = WhichAtoms [n]

Now our terms can be much more complex. An informal description of which atoms occur in a term can be given as follows.

1. The atoms that occur in an atomic term is just that term itself
2. The atoms that occur in a negated formula are the same as the atoms that occur in the unnegated formula
3. The atoms that occur in a conjunction (disjunction) are the union of the atoms that occur in the conjuncts (disjuncts)

We can implement this in Haskell nearly verbatim.

instance SentConn WhichAtoms where
  not (WhichAtoms a) = WhichAtoms a
  WhichAtoms a1 `and` WhichAtoms a2 = WhichAtoms (a1 `List.union` a2)
  WhichAtoms a1 `or` WhichAtoms a2 = WhichAtoms (a1 `List.union` a2)

This is, like the Depth, Size, and NumAtoms instances above, not a ‘semantic’ interpretation of our term, in the linguistic sense. Still, we are interpreting our terms compositionally to arrive at meaningful values (just not linguistically meaningful ones).

In order to allow a term containing sentential connectives to be interpreted in two domains at once, we need to explain to Haskell how this is possible.

instance (SentConn a,SentConn b) => SentConn (a,b) where
  (a1,b1) `and` (a2,b2) = (a1 `and` a2, b1 `and` b2)
  (a1,b1) `or` (a2,b2) = (a1 `or` a2, b1 `or` b2)
  not (a,b) = (not a, not b)

This defines the conjunction of two pairs to be the pointwise conjunction of the members of these pairs.

Again, that’s it! Now we can check whether our theory predicts some of the entailments that we couldn’t get last time:

> isValidPropSeq ([john_sings_and_john_dances] :- john_sings)
True
> isValidPropSeq ([john_sings] :- john_sings_and_john_dances)
False
> isValidPropSeq ([john_sings `or` john_dances] :- john_sings)
False
> isValidPropSeq ([john_sings] :- (john_sings `or` john_dances))
True