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\) | \(b\) | \(a \land b\) |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | F |
| F | F | F |
>>> 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\) | \(b\) | \(a \lor b\) |
|---|---|---|
| T | T | T |
| T | F | T |
| F | T | T |
| F | F | F |
>>> a = True
>>> b = False
>>> a || b
True
Truth table of Logical Not:
| \(a\) | \(\neg a\) |
|---|---|
| T | F |
| F | T |
>>> a = True
>>> not a
False
Truth table of Logical Imply:
| \(a\) | \(b\) | \(a \implies b\) |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
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?
- \((\forall a) (\exists b)\ b = 2a\)
- \((\exists b) (\forall a)\ b = 2a\)
Assume that we discuss in the domain of integers \(\mathbb{Z}\).
- means for any integer (a), there exists an other integer (b) who is 2 times as large as it. This is a true statement.
- 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