Logic

Boolean

There are only 2 values of Boolean type - true (T) and false (F).

>>> True
>>> False

Boolean operations

Logical And is represented as \( \land \) in math.

>>> a = True
>>> b = False
>>> a && b
False

Other boolean operations include Or (\(\lor\)), Not (\(\neg\)), Imply (\(\implies\)) and etc.

Truth table of Logical Or:

>>> a = True
>>> b = False
>>> a || b
True

Truth table of Logical Not:

>>> a = True
>>> not a
False

Truth table of Logical Imply:

Let's define Imply (==>) in Haskell.

(==>) :: Bool -> Bool -> Bool
True ==> False = False
_ ==> _ = True

>>> a = True
>>> b = False
>>> a ==> b
False

First order logic

A predicate (P) is a function that takes some variables as input and produces a Boolean as output. e.g. \(P(x)\).

Example:

>>> isEven a = a `mod` 2 == 0
>>> isEven 3
False

Here, isEven is a predicate that checks whether its input variable a is an even number.

Quantifiers

Forall (\(\forall\)) and Exists (\(\exists\)) are called Quantifiers in Firsr Order Logic.

Forall quantifies variables and make statements about ALL elements in a domain (D). Its general form looks like \((\forall x \in D)\ P(x)\).

>>> forall = flip all
>>> d = [32, 0, 14]
>>> forall d isEven
True

Exists quantifies variables and make statements about SOME elements in a domain (D). Its general form looks like \((\exists x \in D)\ P(x)\).

>>> exists = flip any
>>> d = [1, 32, 7]
>>> exists d isEven
True

Sometimes when the domain is obvious, mathematicians omit it. \((\exists x)\ P(x)\).

Math notations are ambiguous and can be sometimes confusing. For example, can you tell the difference of what the 2 notations mean?

1. \((\forall a) (\exists b)\ b = 2a\)
2. \((\exists b) (\forall a)\ b = 2a\)

Assume that we discuss in the domain of integers \(\mathbb{Z}\).

1. means for any integer (a), there exists an other integer (b) who is 2 times as large as it. This is a true statement.
2. means there exists an integer (b), who is simultaneously 2 times as large as all other integers. This is non-sense.

Haskell can express those properties, but not powerful enough to verify them in the domain of infinite sets. For example, the first notation can be written as below.

>>> ints = 0 : [m | n <- [1..], m <- [n, -n]]
>>> forall ints (\a -> exists ints (\b -> b == 2*a))
-- the expression above never terminates

If the domain is a finite set, we may be able to evaluate the expression.

>>> s = [1, 3, 5]
>>> forall s (\a -> exists ints (\b -> b == 2*a))
True

Naive Set Theory

Set

Set formalizes the idea of "collection of objects". A simple way to denote a set is listing all elements in it. e.g. \( A := \{1, 2, 3\} \)

We can implement set using list in Haskell.

>>> a = [1, 2, 3]

Another way to denote a set is by specifying a pattern. e.g. \( \{0, 2, 4, ...\} \) denotes the set of even natural numbers.

Haskell also has a similar notation.

>>> a = [0, 2 ..]

Yet another way to denote a set is by specifying properties of elements in the set. A general form looks like: \( \{s \in S | s\ satisflies\ P\} \). It specifies a set whose elements (s) belong to a larger set (S) (the symbol \(\in\) means "is an element of..."), and satisfy a property (P).

For example, the set of even integers can be written as \(\{a \in Z|(\exists n \in Z)\ a = 2n\}\).

As a shorthand, it can also be written as \(\{2n|n \in Z\}\).

The 2 notations represent the same set in math, but are evaluated differently if you translate them literally to haskell

>>> evens = [a | a <- ints, exists ints (\n -> a == 2*n)]
>>> take 3 $ evens
-- never terminate

>>> evens = [2*n | n <- ints]
>>> take 3 $ evens
[0,2,-2]

Inclusion of sets

A set S is a subset of T, if every element in S is also an element of T. In math, we write \(S \subseteq T\). It is defined as \[ x \in S \implies x \in T \].

subset :: [a] -> [a] -> Bool
s `subset` t = forall s (\x -> (x `elem` s) ==> (x `elem` t))
-- or simply
s `subset` t = forall s (\x -> x `elem` t)

Equality of 2 sets \(S = T\) is defined as \[ S \subseteq T \land T \subseteq S \]

eq:: [a] -> [a] -> Bool
s `eq` t = s `subset` t && t `subset` s

Note that order of elements or repetition doesn't matter in sets. Thus, \( \{1, 2, 3\} = \{3, 2, 1\} = \{1, 1, 2, 3, 2\} \).

>>> [1,2,3] `eq` [3,2,1]
True
>>> [1,2,3] `eq` [1,1,2,3,2]
True

\(|S|\) denotes the number of elements in S. e.g. \(|\mathbb{Z}| = \infty \)

sizeof :: (Eq a) => [a] -> Int
sizeof = length . uniq
    where uniq [] = []
          uniq (x:xs)
               | x `elem` uniq xs = uniq xs
               | otherwise = x : uniq xs

>>> sizeof [1,2,3]
3
>>> sizeof [1,1,3]
2