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:
- looking at more data, we realized that subjects needed to be interpreted in a boolean domain
- furthermore, they should be the functions, and their predicates their arguments
- 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
-
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
↩︎