The proper treatment of subjects

By decomposing atomic sentences into subject and predicates we were able to provide a theoretical account of more empirical data; entailment judgements like the following became explicable.

  • “John laughed and cried” ⊢ “John cried”
  • “John either laughed or cried”, “John didn’t laugh” ⊢ “John cried”
  • “John either laughed or cried” ⊢ “Either John laughed or John cried”
  • “John both laughed and cried” \(\vdash\) “John laughed and John cried”
  • “John didn’t laugh” ⊢ “It is not the case that John laughed”

But not all subjects behave the same way.

  • “Everyone either laughed or cried” \(\not\vdash\) “Either everyone laughed or everyone cried”
  • “Noone both laughed and cried” \(\not\vdash\) “Noone laughed and noone cried”
  • “Everyone didn’t laugh” \(\not\vdash\) “It is not the case that everyone laughed”

Moreover, subjects can be operated upon with the boolean connectives.

  • “John or Mary laughed” \(\vdash\) “John laughed or Mary laughed”
  • “Someone but not everyone laughed” \(\vdash\) “Someone laughed but it is not the case that everyone laughed”

Recalling our semantic treatment of the logical operators as the meet and join operations of a boolean algebra, this suggests that subjects should denote in boolean algebras (currently they denote in the set of individuals, which is not even a lattice).

Furthermore, if two functions are combined meet or join, they act pointwise on their arguments:

  • (f `meet` g) x == f x `meet` g x
  • (f `join` g) x == f x `join` g x

The same is true of complements:

  • (cmp f) x == cmp (f x)

While the third, fourth and fifth examples above behave in the predicted way (where the functions are the predicates, and the argument the noun phrases), the next three examples do not. Moreover, the following two examples behave as though the functions were the subjects, and the predicates were the arguments! Summarizing: with respect to predicates,

  • proper names behave both as though they were arguments and functions
  • quantified noun phrases behave only as though they were functions

Treating subjects in general as functions which take predicates as arguments allows us to account (in principle, we still need to give actual denotations) for the most data, but there is still the awkward residue of the argumental behaviour of proper names to consider. We saw last time, however, that a certain kind of function behaves just as though it were an argument; a boolean homomorphism commutes with the operations meet, join, and cmp. Recall:

bhom (cmp a) == cmp (bhom a)
bhom (a `meet` b) == bhom a `meet` bhom b
bhom (a `join` b) == bhom a `join` bhom b

Any function which commutes with the boolean operations (as described above) is a boolean homomorphism. So the ‘argumental’ behaviour of proper names can be seen not as contradicting that subjects be treated uniformly as functions, but as being evidence for the fact that proper names are a special kind of function; boolean homomorphisms.

To summarize:

  1. looking at more data, we realized that subjects needed to be interpreted in a boolean domain
  2. furthermore, they should be the functions, and their predicates their arguments
  3. finally, proper names should be boolean homomorphisms

These conclusions were reached solely by considering the kinds of inferences which are acceptable. (Given our treatment of the boolean connectives and, or, and not as boolean operators.)

TL/DR

  • we have introduced generalized quantifiers
  • proper names are boolean homomorphisms

The code for this post is available here

A revised metalanguage

We will revise our semantic metalanguage to allow for this.

Our previous treatment of subjects and predicates had predicates as functions:

class SubjPred exp where
  type Entity exp
  type Truth exp
  pred :: Int -> exp (Entity exp) -> exp (Truth exp)
  subj :: Int -> exp (Entity exp)

The idea was that exp was a type function, associating a different domain exp a with each type a. The term pred i was a function from things of type exp e to things of type exp t (where here e and t are the types of entities and truth values for this type). Now we have to change this, because predicates are now arguments of subjects, instead of the other way around. As we will now begin the process of expanding our language in earnest, it will be useful to give a precise language of types. We define new types, one for predicates (P), one for truth (T), and a way of building new types from old types (a :-> b).

data P -- the type of predicates

data T -- the type of truth values

data (:->) a b -- a :-> b is the type of functions from a to b

Our predicate terms are now expressions of type P.

class Pred exp where
  pred :: Int -> exp P

Our proper names are given their own class, and are of type P :-> T, so that they can be interpreted as functions taking predicates as their arguments.

class Name exp where
  name :: Int -> exp (P :-> T)

We now introduce generalized quantifier (subject) terms, which include the quantifiers everyone, someone, and noone. These are expressions of type P :-> T, which we will interpret as functions from expressions of type P to those of type T.

class GQ exp where
  everyone :: exp (P :-> T)
  someone :: exp (P :-> T)
  noone :: exp (P :-> T)

In order to interpret an expression of type a :-> b as a function from expressions of type a to those of type b, we introduce the Apply class, which contains metalanguage operators $> and <$. Terms of the form m $> n and n <$ m in our metalanguage will be interpreted as the interpretation of m taking the interpretation of n as its argument.

class Apply exp where
  ($>) :: exp (a :-> b) -> exp a -> exp b
  (<$) :: exp a -> exp (a :-> b) -> exp b
  (<$) = flip ($>)

With our metalanguage extended in this way, we can write terms standing for the sentences we have been considering. First, we give names to individuals and predicates:

john, mary :: Name exp => exp (P :-> T)
john = name 0
mary = name 1

laugh, cry :: Pred exp => exp P
laugh = pred 0
cry = pred 1

All sentences will be expressions of type T. Atomic sentences will be composed (via the Apply class) of predicates (the Pred class) and subjects (the GQ class).

johnLaughed, johnCried :: (Pred exp, Name exp, Apply exp) => exp T
johnLaughed = john $> laugh
johnCried = john $> cry

Sentences with complex predicates will require that expressions of type P be interpreted in a boolean domain (class Boolean).

johnLaughedAndCried, johnLaughedOrCried, johnDidntLaugh, everyoneLaughedOrCried, everyoneLaughedOrEveryoneCried, nooneLaughedAndCried, nooneLaughedAndNooneCried, everyoneDidntLaugh, itIsNotTheCaseThatEveryoneLaughed, johnOrMaryLaughed, johnLaughedOrMaryLaughed, someoneButNotEveryoneLaughed, someoneLaughedButItIsNotTheCaseThatEveryoneLaughed :: (Boolean (exp P), Pred exp, Name exp, Apply exp) => exp T

johnLaughedAndCried = john $> (laugh `meet` cry)

johnLaughedOrCried = john $> (laugh `join` cry)

johnDidntLaugh = john $> cmp laugh

johnOrMaryLaughed = (john `join` mary) $> laugh

everyoneLaughedOrCried, everyoneLaughedOrEveryoneCried, nooneLaughedAndCried, nooneLaughedAndNooneCried, everyoneDidntLaugh, itIsNotTheCaseThatEveryoneLaughed, someoneButNotEveryoneLaughed, someoneLaughedButItIsNotTheCaseThatEveryoneLaughed :: (Boolean (exp P), Pred exp, GQ exp, Apply exp) => exp T


everyoneLaughedOrCried = everyone $> (laugh `join` cry)

nooneLaughedAndCried = noone $> (laugh `meet` cry)

everyoneDidntLaugh = everyone $> cmp laugh

someoneButNotEveryoneLaughed = (someone `meet` cmp everyone) $> laugh

Complex sentences will require that expressions of type T be interpreted in a boolean domain.

itIsNotTheCaseThatJohnLaughed, everyoneLaughedOrEveryoneCried, nooneLaughedAndNooneCried, itIsNotTheCaseThatEveryoneLaughed, johnLaughedOrMaryLaughed, someoneLaughedButItIsNotTheCaseThatEveryoneLaughed :: (Boolean (exp T), Pred exp, Name exp, Apply exp) => exp T

itIsNotTheCaseThatJohnLaughed = cmp (john $> laugh)

johnLaughedOrMaryLaughed = (john $> laugh) `join` (mary $> laugh)


everyoneLaughedOrEveryoneCried, nooneLaughedAndNooneCried, itIsNotTheCaseThatEveryoneLaughed, someoneLaughedButItIsNotTheCaseThatEveryoneLaughed :: (Boolean (exp T), Pred exp, GQ exp, Apply exp) => exp T

everyoneLaughedOrEveryoneCried = (everyone $> laugh) `join` (everyone $> cry)

nooneLaughedAndNooneCried = (noone $> laugh) `meet` (noone $> cry)

itIsNotTheCaseThatEveryoneLaughed = cmp (everyone $> laugh)

someoneLaughedButItIsNotTheCaseThatEveryoneLaughed = (someone $> laugh) `meet` cmp (everyone $> laugh)

The entailments we discussed at the beginning of the post can be written as follows:

{-| CLAIM:

    the following are valid entailments, which our semantic theory should predict to hold.
-}
[johnLaughedAndCried] :-  johnCried
[johnLaughedOrCried, johnDidntLaugh] :- johnCried
[johnLaughedOrCried] :- johnLaughedOrJohnCried
[johnLaughedAndCried] :- johnLaughedAndJohnCried
[johnDidntLaugh] :- itIsNotTheCaseThatJohnLaughed
[johnOrMaryLaughed] :- johnLaughedOrMaryLaughed
[someoneButNotEveryoneLaughed] :- someoneLaughedButItIsNotTheCaseThatEveryoneLaughed

{-| CLAIM:

    the following are *NOT* valid entailments, and our semantic theory should predict that they do not hold
-}
[everyoneLaughedOrCried] :- everyoneLaughedOrEveryoneCried
[nooneLaughedAndCried] :- nooneLaughedAndNooneCried
[everyoneDidntLaugh] :- itIsNotTheCaseThatEveryoneLaughed

Now that we can talk about our claims in our semantic metalanguage, we would like to actually make predictions about them.

Truth in a model

In our previous account of subjects and predicates, subjects denoted individuals, and predicates sets thereof (or equivalently functions from individuals to truth values). This seemed right. At any rate, our decision to modify our semantic metalanguage doesn’t seem to have been based on any conceptual difficulties with this way of thinking about subjects and predicates. We would like to continue to take predicates as denoting sets of individuals. And similarly, the semantic content of proper names should continue to be determined by individuals.

data Model e t = Model {individuals :: Int -> e, predicates :: Int -> e -> t}

Expressions are associated with ‘type expressions’ of the form P :-> T, but we need to relate these type expressions to haskell values. We define a function from type expressions to the type of haskell values they should be understood as.

type family TypeInterp (e :: *) (t :: *) (ty :: *) :: *
type instance TypeInterp e t T = t
type instance TypeInterp e t P = e -> t
type instance TypeInterp e t (a :-> b) = TypeInterp e t a -> TypeInterp e t b

The interpretation of expressions in a model is a function from models to the value of expressions.

newtype Interp e t ty = Interp {unInterp :: Model e t -> TypeInterp e t ty}

The interpretation of predicates is exactly as before; a predicate denotes a function from a model to a set of individuals.

instance Pred (Interp e t) where
  pred i = Interp (\model -> predicates model i)

A name cannot anymore just refer to an individual. It must now be of semantic type P :-> T which is of haskell type (e -> Bool) -> Bool. Thus it must take a set of individuals as its argument, and return a truth value. Previously, we combined predicates and names by looking to see whether the predicate was true of the name. We gave control of this check to the predicate, by treating it as a function. Now we must give control of this check to the name, but the end result should be the same: the name will take the predicate, and check whether the predicate is true of the individual the name is a name of.

instance Name (Interp e t) where
  name i = Interp (\model p -> p (individuals model i))

Instead of allowing names and predicates to combine on their own, we have given control of this to the Apply class, which interprets an expression of type a :-> b as a function from expressions of type a to those of type b. Something of type Interp e (a :-> b) is actually a wrapper for a Haskell function of type Model e -> TypeInterp e a -> TypeInterp e b, and an expression of type Interp e a has type Model e -> TypeInterp e a. The Apply class needs to put these two things together to come up with an expression of type Interp e b, which is of Haskell type Model e -> TypeInterp e a. In other words, we need to put functor and argument together, before they have been given a model.

instance Apply (Interp e t) where
  Interp f $> Interp x = Interp (\model -> f model (x model))

To interpret the boolean connectives in a type ty, we need to show that Interp e t ty is a boolean algebra.

instance Lattice (TypeInterp e t a) => Lattice (Interp e t a) where
  Interp f `meet` Interp g = Interp (f `meet` g)
  Interp f `join` Interp g = Interp (f `join` g)

instance Boolean (TypeInterp e t a) => Boolean (Interp e t a) where
  top = Interp top
  bot = Interp bot
  cmp (Interp f) = Interp (cmp f)

Unlike names and predicates, the interpretation of which varies from situation to situation, but like the boolean operations, which have an interpretation that does not change across models, the generalized quantifiers everyone, someone, and noone are logical constants. the expression everyone $> laugh should be true iff laugh is true of all the individuals of the model. Similarly someone $> laugh should be true iff laugh is true of at least one individual in the model. And noone $> laugh should be true iff laugh is true of no individual in the model.

instance (Bounded e,Enum e,b~Bool) => GQ (Interp e b) where
  everyone = Interp (\_ p -> all p [minBound..maxBound])
  someone = Interp (\_ p -> any p [minBound..maxBound])
  noone = Interp (\_ p -> all (not . p) [minBound..maxBound])

The fact that the meanings of everyone, someone, and noone are independent of the situation of use is implemented in these definitions by ‘throwing away’ the model argument (the underscore after the Haskell lambda-slash means that there is an argument there, but we do not want it - we don’t even give it a name). However, in contrast to the interpretations of predicates and names, to interpret generalized quantifiers in this way we need to constrain the individuals to be finite and enumerable. Essentially, when we say everyone $> laugh, we are making a claim about everyone, and so in order to see whether this claim is true or not, we need to check whether each individual does indeed laugh or not.

Validity

The language we have just introduced is a restricted version of classical first-order logic, a subcase of what is called monadic first-order logic. This is the special case of first-order logic where there are only one-place relations (and not, more generally, binary or higher-order relations). This is one of the fragments of first-order logic for which entailment between sentences can actually be computed! The entailment problem is becoming more and more difficult as we increase the sophistication of our semantic meta-language: the richer the things we can talk about are, the more kinds of relevant situations there are which we must take into account. With propositional logic (the system in Adding sentential connectives), the relevant situations are completely determined by the identity of the atomic propositions in the logical sentence, and we can obtain them by computing the powerset of this set (each set of atomic propositions representing the situation which makes exactly those true). Decomposing atomic sentences into individuals and predicates does not fundamentally change the problem; now we must ask about each individual, which sets it belongs to. The relevant situations are completely determined by pairing the predicates with the set of individuals they are predicated of in the logical sentence. A relevant situation can obtained from this information by interpreting each predicate as a subset of the individuals it was predicated of. In the limiting case where we have but one predicate, the problem degenerates to exactly the problem of sentential logic; we have essentially replaced propositional variables by different individuals being predicated of different predicates.

Adding the quantifier everyone allows us to talk about whether a set contains everything, adding someone allows us to state that a set is non-empty, and adding noone allows us to state that a set is empty. The boolean operations allow us to talk about intersections, unions and complements, and thus enable us to say that some sets share a common element (someone $> (laugh `meet` cry)), or that one set is a subset of another (everyone $> (cmp laugh `join` cry)). Thus for the first time our semantic metalanguage is powerful enough to express relations among sets.1

{-# LANGUAGE DataKinds, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, GADTs, KindSignatures #-}
import qualified Data.Set as Set
import qualified Data.IntMap as Map

data WhichAtoms = WhichAtoms {whichNames :: Set.set Int, whichPredicates :: Set.set Int}
data K a b = K a

instance Pred (K WhichAtoms) where
  pred i = K (WhichAtoms Set.empty (Set.singleton i))
instance Name (K WhichAtoms) where
  name i = K (WhichAtoms (Set.singleton i) Set.empty)

instance GQ (K WhichAtoms) where
  everyone = K (WhichAtoms Set.empty Set.empty)
  noone = K (WhichAtoms Set.empty Set.empty)
  someone = K (WhichAtoms Set.empty Set.empty)

instance Apply (K WhichAtoms) where
  K (WhichAtoms n1 p1) $> K (WhichAtoms n2 p2)
    = K (WhichAtoms (n1 `Set.union` n2) (p1 `Set.union` p2))

instance Lattice (K WhichAtoms) where
  K (WhichAtoms n1 p1) `join` K (WhichAtoms n2 p2)
    = K (WhichAtoms (n1 `Set.union` n2) (p1 `Set.union` p2))
  K (WhichAtoms n1 p1) `meet` K (WhichAtoms n2 p2)
    = K (WhichAtoms (n1 `Set.union` n2) (p1 `Set.union` p2))

instance Boolean (K WhichAtoms) where
  top = WhichAtoms Set.empty Set.empty
  bot = WhichAtoms Set.empty Set.empty
  cmp = id


data Nat = Z | S Nat deriving (Eq,Ord)
instance Enum Nat where
  toEnum n | n > 0 = toEnumHelper n
           | otherwise = Z
    where
      toEnumHelper 0 = Z
      toEnumHelper n = S (toEnumHelper (n - 1))
  fromEnum Z = 0
  fromEnum (S n) 1 + fromEnum n
data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
class SNAT (n :: Nat) where
  snat :: SNat n
instance SNAT Z where
  snat = SZ
instance SNAT n => SNAT (S n) where
  snat = SS snat

class LE (m :: Nat) (n :: Nat) where
instance LE Z n where
instance LE m n => LE (S m) (S n) where

data Fin (n :: Nat) where
  FinZ :: Fin m
  FinS :: LE (S Z) m => Fin m -> Fin (S m)
instance Ord (Fin m) where
  FinZ <= _ = True
  FinS m <= FinS n = m <= n
  _ <= _ = False
instance Eq (Fin m) where
  FinZ == FinZ = True
  FinS m == FinS n = m == n
  _ == _ = False
instance Enum (Fin (S Z)) where
  toEnum 0 = FinZ
  toEnum _ = FinS FinZ
  fromEnum FinZ = 0
  fromEnum _ = 1
instance (Enum (Fin (S m))) => Enum (Fin (S (S m))) where
  toEnum 0 = FinZ
  toEnum m = FinS $ toEnum (m - 1)
  fromEnum FinZ = 0
  fromEnum (FinS m) = succ $ fromEnum m


data Exists (p :: k -> *) where
  Exists :: p i -> Exists p
type WNat = Exists SNat



constructModels :: K WhichAtoms -> [Model (Either Int Int) Bool]
constructModels (K (WhichAtoms n p)) = fmap mkModel $ sequenceA $ Map.fromList $ fmap (\a -> (a,pSet)) Set.toList p
  where
    pSet = Set.powerSet (n `Set.disjointUnion` p)
    mkModel preds = Model Left (flip Set.member . flip Map.lookup preds)

isValidSequent (ant :- conc) = all (unInterp sequentProp) $ constructModels sequentAtoms
  where
    (sequentProp,sequentAtoms) = cmp (infMeet ant) `join` conc

  1. Just to be clear, the translation from our semantic meta-language to ‘set-talk’ works as follows. everyone p : p == top noone p : p == bot someone p : p \= bot ↩︎