# First-order languages and Set Theory¶

## First-Order languages¶

A first-order language is determined by a vocabulary consisting of variables, constants, functions and relations. First, we encode functions and relations.

In :
case class Function(name: String, degree: Int)

case class Relation(name: String, degree: Int)

Out:
defined class Function
defined class Relation

We form two kinds of expressions, terms and formulas using these. Both of these are defined recursively.

In :
sealed trait Expression

sealed trait Term extends Expression

sealed trait Formula extends Expression

object Term{
case class Var(name: String) extends Term

case class Const(name: String) extends Term

case class Recursive(function: Function, arguments: Vector[Term]) extends Term{
require(function.degree == arguments.length)
}
}

object Formula{
case class Equality(lhs: Term, rhs: Term) extends Formula

case class Atomic(relation: Relation, arguments: Vector[Term]) extends Formula{
require(relation.degree == arguments.length)
}

case class Or(p: Formula, q: Formula) extends Formula

case class And(p: Formula, q: Formula) extends Formula

case class Implies(p: Formula, q: Formula) extends Formula

case class Equivalent(p: Formula, q: Formula) extends Formula

case class Not(p: Formula) extends Formula

case class ForAll(x: Term.Var, p: Formula) extends Formula

case class Exists(x: Term.Var, p: Formula) extends Formula

}

Out:
defined trait Expression
defined trait Term
defined trait Formula
defined object Term
defined object Formula
In :
val sum = Function("+", 2)
val succ = Function("succ", 1)
// Some valid terms
import Term._
val n = Var("n")
val m = Var("m")
val one = Const("1")
Recursive(sum, Vector(n, m))
Recursive(succ, Vector(n))
val two = Recursive(succ, Vector(one))

Out:
sum: Function = Function("+", 2)
succ: Function = Function("succ", 1)
import Term._

n: Var = Var("n")
m: Var = Var("m")
one: Const = Const("1")
res2_6: Recursive = Recursive(Function("+", 2), Vector(Var("n"), Var("m")))
res2_7: Recursive = Recursive(Function("succ", 1), Vector(Var("n")))
two: Recursive = Recursive(Function("succ", 1), Vector(Const("1")))
In :
// An invalid term
import scala.util.Try
val wrong = Try(Recursive(succ, Vector(one, n)))

Out:
import scala.util.Try

wrong: Try[Recursive] = Failure(
java.lang.IllegalArgumentException: requirement failed
)
In :
// Some formulas
import Formula._
val f1 = Equality(one, two)
val f2 = Equality(n, one)
val leq = Relation("<=", 2)
val f3 = Atomic(leq, Vector(one, two))
val f4 = ForAll(n, f2)
val f5 = Exists(n, f2)
val f6 = ForAll(m, f1)

Out:
import Formula._

f1: Equality = Equality(
Const("1"),
Recursive(Function("succ", 1), Vector(Const("1")))
)
f2: Equality = Equality(Var("n"), Const("1"))
leq: Relation = Relation("<=", 2)
f3: Atomic = Atomic(
Relation("<=", 2),
Vector(Const("1"), Recursive(Function("succ", 1), Vector(Const("1"))))
)
f4: ForAll = ForAll(Var("n"), Equality(Var("n"), Const("1")))
f5: Exists = Exists(Var("n"), Equality(Var("n"), Const("1")))
f6: ForAll = ForAll(
Var("m"),
Equality(Const("1"), Recursive(Function("succ", 1), Vector(Const("1"))))
)

The formulas in mathematical notation are

• $1 = 2$
• $n = 1$
• $1 \leq 2$
• $\forall n\ n = 1$
• $\exists n\ n = 1$
• $\exists m\ 1 = 2$

## The language of Sets¶

The language of sets has:

• a single constant $\phi$
• a single relation $\in$ of degree $2$.

We introduce these as well as a convenience method.

In :
import Term._, Formula._

val phi = Const("empty-set")
val in = Relation("in", 2)

def belongs(x: Term, y: Term) = Formula.Atomic(in, Vector(x, y))

Out:
import Term._, Formula._

phi: Const = Const("empty-set")
in: Relation = Relation("in", 2)
defined function belongs

As an example, we define extensionality, i.e. if two sets have the same members, they are equal. $$\forall x\forall y((\forall a\ (a\in x\iff a \in y)) \implies (x = y))$$

In :
val a = Var("a")
def sameMembers(p: Term, q: Term): Formula =
ForAll(a, Equivalent(belongs(a, p), belongs(a, q)))

Out:
a: Var = Var("a")
defined function sameMembers
In :
val x = Var("x")
val y = Var("y")
val extensionality =
ForAll(x,
ForAll(y,
Implies(sameMembers(x, y), Equality(x, y))))

Out:
x: Var = Var("x")
y: Var = Var("y")
extensionality: ForAll = ForAll(
Var("x"),
ForAll(
Var("y"),
Implies(
ForAll(
Var("a"),
Equivalent(
Atomic(Relation("in", 2), Vector(Var("a"), Var("x"))),
Atomic(Relation("in", 2), Vector(Var("a"), Var("y")))
)
),
Equality(Var("x"), Var("y"))
)
)
)

## Variables and free variables¶

• The value of a term can depend on some variables.
• The truth value of a formula can depend on some variables.
• These are called free variables.

### Examples¶

In the language of natural numbers

• $1 = 2$; no free variables
• $n = 1$; free variable n
• $1 \leq 2$; no free variables
• $\forall n\ n = 1$; no free variables
• $\exists n\ n +5 < m$; free variable m
• $\exists m\ 1 = 2$; no free variables
In :
// Variable in a term
def variables(t: Term): Set[Var] = t match {
case Const(name) => Set()
case Recursive(function, arguments) =>
for{
arg : Term <- arguments.toSet
x <- variables(arg)
} yield x
case Var(name) => Set(Var(name))
}

Out:
defined function variables
In :
variables(Recursive(sum, Vector(n, m)))

Out:
res9: Set[Var] = Set(Var("n"), Var("m"))
In :
val p = Recursive(succ, Vector(m))
variables(Recursive(sum, Vector(n, p)))

Out:
p: Recursive = Recursive(Function("succ", 1), Vector(Var("m")))
res10_1: Set[Var] = Set(Var("n"), Var("m"))
In :
variables(p)

Out:
res11: Set[Var] = Set(Var("m"))
In :
def freeVariables(fmla: Formula) : Set[Var] = fmla match {
case Equality(lhs, rhs) =>
variables(lhs) union variables(rhs)
case And(p, q) =>
freeVariables(p) union freeVariables(q)
case Implies(p, q) =>
freeVariables(p) union freeVariables(q)
case Equivalent(p, q) =>
freeVariables(p) union freeVariables(q)
case Not(p) =>
freeVariables(p)
case ForAll(x, p) =>
freeVariables(p) - x
case Atomic(relation, arguments) =>
for {
arg: Term <- arguments.toSet
x <- variables(arg)
} yield x
case Exists(x, p) =>
freeVariables(p) - x
case Or(p, q) =>
freeVariables(p) union freeVariables(q)
}

Out:
defined function freeVariables
In :
val fmla1 = Exists(x, belongs(x, y))
val fmla2 = ForAll(y, fmla1)
val fmla3 = belongs(x, y)

Out:
fmla1: Exists = Exists(
Var("x"),
Atomic(Relation("in", 2), Vector(Var("x"), Var("y")))
)
fmla2: ForAll = ForAll(
Var("y"),
Exists(Var("x"), Atomic(Relation("in", 2), Vector(Var("x"), Var("y"))))
)
fmla3: Atomic = Atomic(Relation("in", 2), Vector(Var("x"), Var("y")))
In :
freeVariables(fmla1)
freeVariables(fmla2)
freeVariables(fmla3)

Out:
res14_0: Set[Var] = Set(Var("y"))
res14_1: Set[Var] = Set()
res14_2: Set[Var] = Set(Var("x"), Var("y"))

## Set Theory¶

We have so far:

• the empty set $\phi$.
• the relation $\in$ for sets.
• an axiom saying when two sets are equal.

We also know that we cannot specify sets by arbitrary properties, i.e., like $$\{p : \text{p is a prime}\}$$.

We shall, however, see that we can define sets such as $$\{p \in\mathbb{N} : \text{p is a prime}\}$$ provided we have previously defined (constructed) $\mathbb{N}$.

### Properties¶

Let $x$ be a variable. A property of $x$ is a formula $p = p(x)$ so that $p$ has no free variables other than $x$ ($x$ may also not be a free variable).

We cannot define sets with unrestricted comprehension, i.e., of the form $$S = \{x : p(x) \}$$ as we get a paradox with the set $$S = \{x : x \notin x\}$$

In :
val russell = Not(belongs(x, x))
freeVariables(russell)

Out:
russell: Not = Not(Atomic(Relation("in", 2), Vector(Var("x"), Var("x"))))
res15_1: Set[Var] = Set(Var("x"))

### Axiom schema of specification¶

Given a set $U$ and a property $p= p(x)$ of the variable $x$, there exists a set $S$ given by $$S = \{x \in U: p(x)\}$$

More formally, fix a formula $p$ with no free variables other than $x$. We have the axiom: $$\forall U\exists S(x\in S \iff (x \in U \land p(x))$$

In :
// we can implement specification for nice properties
val U = (1 to 20).toSet
val S = U.filter(x => x % 3 == 0) // p(x) = x % 3 == 0
show(S)

Set(6, 9, 12, 3, 18, 15)

Out:
U: Set[Int] = Set(
5,
10,
14,
20,
1,
6,
9,
13,
2,
17,
12,
7,
3,
18,
16,
11,
8,
19,
4,
15
)
S: Set[Int] = Set(6, 9, 12, 3, 18, 15)

## Union of a pair of sets¶

$A \cup B$ is the set whose elements are elements of $A$ and elements of $B$

In :
Set(1, 3, 4) union Set(3, 7, 9)

Out:
res17: Set[Int] = Set(1, 9, 7, 3, 4)

The existence of union is given by the axiom of unordered pairs

$$\forall A \forall B\exists C(\forall x\ (x\in C \iff (x\in A \lor x\in B )))$$

### Arbitrary union¶

Given a set of sets $U$, we can take the union of all of these, i.e. there exists $$\bigcup_{A \in U}A$$ such that $x \in \bigcup_{A \in U}A$ if and only if $$\exists A\ (A \in U \land x \in A)$$.

In :
// union of sets
val setOfSets = Set(Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
val bigUnion = setOfSets.flatten

Out:
setOfSets: Set[Set[Int]] = Set(Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
bigUnion: Set[Int] = Set(1, 2, 7, 3, 23, 8)

There is an axiom that says $\bigcup_{A \in U}A$ exists (axiom of unions)

In :
val big = Set[Any](Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
big contains (Set(1, 2))
(Set[Any](1, 2)).subsetOf(big)
big contains 1

Out:
big: Set[Any] = Set(Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
res19_1: Boolean = true
res19_2: Boolean = false
res19_3: Boolean = false
In :
Set[Any](Set(1, 2)).subsetOf(big)

Out:
res20: Boolean = true
In :
val anotherBig = Set[Any](1, Set(1), Set(1, 2), Set[Any](2, Set(1, 3)))

Out:
anotherBig: Set[Any] = Set(1, Set(1), Set(1, 2), Set(2, Set(1, 3)))
In :
anotherBig contains 1

Out:
res22: Boolean = true
In :
Set[Any](1) subsetOf anotherBig
anotherBig contains Set(1)

Out:
res23_0: Boolean = true
res23_1: Boolean = true
In :
import scala.collection.mutable.{Set => mSet}
val ss = mSet[Any](mSet(1), mSet(2))

Out:
import scala.collection.mutable.{Set => mSet}

ss: collection.mutable.Set[Any] = Set(Set(1), Set(2))
In :
ss += mSet(3, 4)

Out:
res25: collection.mutable.Set[Any] = Set(Set(1), Set(2), Set(3, 4))
In :
ss += 1

Out:
res26: collection.mutable.Set[Any] = Set(Set(1), Set(2), 1, Set(3, 4))

## Intersections¶

These do not need a new axiom:

$$A \cap B = \{x \in A : x \in B\}$$

i.e., we are using the property $p = p(x) = x \in B$ with free variable $x$.

Remark: By axiom of extenstion $A \cap B = B \cap A$.

In :
val A = Set(1, 2, 3)
val B = Set(2,3, 7, 9)
A intersect B

Out:
A: Set[Int] = Set(1, 2, 3)
B: Set[Int] = Set(2, 3, 7, 9)
res27_2: Set[Int] = Set(2, 3)
In :
A.filter(x => B contains x)

Out:
res28: Set[Int] = Set(2, 3)

### Power Set¶

The power set of a set $S$ is the set of subsets of $S$, i.e. $$2^S = \{x : x \subset S\}$$

This exists because of the axiom of power sets (which just says it exists).

In :
Set(1, 2, 7).subsets.toSet

Out:
res29: Set[Set[Int]] = Set(
Set(),
Set(2),
Set(1, 2),
Set(2, 7),
Set(1, 2, 7),
Set(7),
Set(1, 7),
Set(1)
)
In :
Set().subsets.toSet

Out:
res30: Set[Set[Nothing]] = Set(Set())
In :
Set().subsets.toSet.size

Out:
res31: Int = 1

Formally, we define $A \subset B$ by $x\in A \implies x \in B$.

The axiom giving existence of power sets says $$\forall S\exists P (x\in P \iff x\subset S)$$

or in full form $$\forall S\exists P (x\in P \iff (\forall y\ y\in x\iff y\in S))$$

## Numbers as Sets¶

Everything in mathematics can be represented as sets. As an example, we consider natural numbers. We associate to each number $n$ a set of size n.

• $0$ is $\phi$.
• $1$ is $\{\phi\}$.
• $2$ is $\{\phi, \{\phi\}\}$.

In general, we define the successor of a set $s$ as $$succ(s) = s \cup \{s\}$$ and define the set associated to $n$ by

• associate $\varphi$ to $0$.
• if $s$ is associated to $n$, associate $succ(s)$ to $n + 1$.

Remark: $\{s\} = \{y \in 2^s: y = s \}$

In :
def succ(s: Set[Any]) : Set[Any] = s union Set(s)
succ(Set(1, 2))

Out:
defined function succ
res32_1: Set[Any] = Set(1, 2, Set(1, 2))
In :
def numberSet(n: Int): Set[Any] =
if (n == 0) Set() else succ(numberSet(n - 1))
numberSet(3)

Out:
defined function numberSet
res33_1: Set[Any] = Set(Set(), Set(Set()), Set(Set(), Set(Set())))
In :
(0 to 10).map (n => numberSet(n).size)

Out:
res34: collection.immutable.IndexedSeq[Int] = Vector(
0,
1,
2,
3,
4,
5,
6,
7,
8,
9,
10
)
• Talking of size is circular. Instead Cantor defined when two sets have the same size. Formally, we say same cardinality.

• We say two sets have the same cardinality if there is a one-to-one correspondence between their elements.

• By this definition, natural numbers and even natural numbers have the same cardinality.

## Functions : semi-formal¶

A function $f: X \to Y$ is given by

• A set $X$, called the domain.
• A set $Y$, called the co-domain.
• For each $x\in X$, we associate $f(x)\in Y$.

Example: We can take $X = Y = \mathbb{N}$ and define $f(n) = 2n$.

### Injective (one-to-one)¶

A function $f: X \to Y$ is said to be injective if for $a, b\in X$, if $a\neq b$ then $f(a)\neq f(b)$, i.e. $$\forall a,b\in X, a\neq b\implies f(a)\neq f(b)$$

Equivalently, $$\forall a, b\in X, (a = b) \lor (f(a) \neq f(b))$$

In :
def isInjective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
domain.forall{a =>
domain.forall{b =>
(a == b) || (f(a) != f(b))}}

Out:
defined function isInjective
In :
isInjective((1 to 10).toSet, (1 to 30).toSet, (n: Int) => 2 * n)

Out:
res36: Boolean = true
In :
isInjective((1 to 10).toSet, (1 to 30).toSet, (n: Int) => n/ 2)

Out:
res37: Boolean = false
In :
isInjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 2, 3 -> 1))
isInjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 3, 3 -> 2))

Out:
res38_0: Boolean = false
res38_1: Boolean = true

### Range and surjectivity¶

The range of $f: X \to Y$ is defined as $$f(X) = \{f(x): x \in X\}$$

We say $f: X \to Y$ is surjective if $f(X) = Y$.

In :
def range[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
domain.map(f)
range(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 2, 3 -> 1))
range(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 3, 3 -> 2))

Out:
defined function range
res39_1: Set[Int] = Set(1, 2)
res39_2: Set[Int] = Set(1, 3, 2)
In :
def isSurjective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
range(domain, codomain, f) == codomain

isSurjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 2, 3 -> 1))
isSurjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 3, 3 -> 2))
isSurjective(Set(1, 2, 3), Set(1, 2), Map(1 ->1, 2 -> 2, 3 -> 1))

Out:
defined function isSurjective
res40_1: Boolean = false
res40_2: Boolean = true
res40_3: Boolean = true

### Bijections and Cardinality¶

• A function $f: X \to Y$ is said to be bijective if it is both injective and surjective.
• Two sets $X$ and $Y$ have the same cardinality if there exists a bijective function $f: X \to Y$.
In :
def isBijective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
isSurjective(domain, codomain, f) && isInjective(domain, codomain, f)

Out:
defined function isBijective
In :
isBijective(Set(1, 2, 3), Set(2, 4, 6), Map(1 -> 2, 2-> 4, 3 -> 6))

Out:
res42: Boolean = true
In :
isBijective(
Set(1, 2, 3), Set(1, 2, 3, 4, 5, 6), Map(1 -> 2, 2-> 4, 3 -> 6)
)

Out:
res43: Boolean = false
In :
isBijective(Set(1, 2, 3), Set(1, 2, 3), Map(1 -> 2, 2-> 1, 3 -> 1))

Out:
res44: Boolean = false

### Inverses for bijections¶

If $f: X \to Y$ is a bijection, then it has an inverse $f^{-1}: Y\to X$ so that $$\forall x\in X, f^{-1}(f(x)) = x$$ and $$\forall y\in Y, f(f^{-1}(y)) = y$$ and conversely. Further, $f^{-1}: Y \to X$ is a bijection.

In :
def inverseFunction[A, B](domain: Set[A], codomain: Set[B], f: A => B) ={
require(isBijective(domain, codomain, f),
"can only invert bijections")
(y: B) => domain.find(x => f(x) == y).get
}.ensuring{
g =>
domain.forall(x => g(f(x)) == x) &&
codomain.forall(y => f(g(y)) == y)
}

inverseFunction(Set(1, 2, 3), Set(1, 2, 3), Map(1 -> 2, 2 ->3, 3 -> 1))

Out:
defined function inverseFunction
res45_1: Int => Int = ammonite.$sess.cmd45$Helper$$Lambda2934/99060392@286ef9a7 In : Try{ inverseFunction(Set(1, 2, 3), Set(1, 2, 3), Map(1 -> 2, 2 ->1, 3 -> 1)) }  Out: res46: Try[Int => Int] = Failure( java.lang.IllegalArgumentException: requirement failed: can only invert bijections ) In : def inverseMap[A, B](domain: Set[A], codomain: Set[B], f: A => B) ={ require(isBijective(domain, codomain, f), "can only invert bijections") (codomain.map{ (y: B) => y -> domain.find(x => f(x) == y).get}).toMap }.ensuring{ g => isBijective(codomain, domain, g) && domain.forall(x => g(f(x)) == x) && codomain.forall(y => f(g(y)) == y) }  Out: defined function inverseMap In : inverseMap(Set(1, 2, 3), Set(4, 5, 6), Map(1 -> 4, 2 -> 6, 3 -> 5))  Out: res48: Map[Int, Int] = Map(4 -> 1, 5 -> 3, 6 -> 2) ## Cantor's theorem¶ Theorem: For any set S, any function f: S \to 2^S is not a surjection. In particular S and 2^S do not have the same cardinality. In other words, if f: S\to 2^S, there exists y\in 2^S such that y\notin f(S). Proof: We define y\in 2^S, i.e., y\subset S, which is not in the range by$$y = \{x \in S: x \notin f(x)\}$$This is not in f(S) as for all x_0\in X, then observe that$$x_0\in y \iff x_0 \notin f(x_0)$$so y\neq f(x_0). In : def cantor[A](s: Set[A], f: A => Set[A]): Set[A] = s.filter{x => !f(x).contains(x) }.ensuring(t => !range(s, s.subsets.toSet, f).contains(t))  Out: defined function cantor In : cantor(Set(1, 2, 3), Map(1 -> Set(1), 2 -> Set(1, 2), 3 -> Set(1, 2, 3)))  Out: res50: Set[Int] = Set() In : cantor(Set(1, 2, 3), Map(1 -> Set(1), 2 -> Set(1, 2), 3 -> Set(1, 2)))  Out: res51: Set[Int] = Set(3) ### Hilbert's hotel¶ This is a hotel with infinitely many rooms, with number 1, 2, 3, 4, ... • Suppose all the rooms are occupied and a guest turns up, he can still be accomodated: shift everyone. • Suppose guests with employee codes 1, 2, 3, 4, ... turn up, all can be accomodated. • Suppose guests with employee codes all infinite sequences of 0's and 1's turn up, they cannot be accomodated. ### Comparing sets¶ We have defined what it means for sets A and B to have the same size. We denote this |A| = |B| (for now |A| has no meaning). Question: When should we say |A| \leq |B|? • If B \subset A we expect |B| \leq |A|. • If |B| = |C| and |C| \leq |A| then |B| \leq |A|. Definition: We say |A| \leq |B| if there is an injective function from f: A \to B. Question: If |A| \leq |B| and |B| \leq |A|, does it follow that |A| = |B|? Answer: Yes. This is the Cantor-Bernstein-Shroeder theorem. Question (Trichotomy): Given sets A and B, is at least one of |A| \leq |B| and |B| \leq |A| true? Answer: Yes. Follows from the following. Proposition: There are subsets C \subset A and D \subset B and a bijection from C to D such that either C = A or D = B. That is, there is either a bijection from a subset of A to all of B or from A to a subset of B. In : def trichotomy[X, Y](A : Set[X], B: Set[Y]) : Map[X, Y] = { if (A.isEmpty || B.isEmpty) Map[X,Y]() else { val x = A.head val y = B.head trichotomy[X, Y](A - x, B - y) + (x -> y) } }.ensuring{(f : Map[X, Y]) => (f.keySet == A || f.values.toSet == B) && f.keySet.subsetOf(A) && f.values.toSet.subsetOf(B) && isBijective(f.keySet, f.values.toSet, f) }  Out: defined function trichotomy In : trichotomy(Set(1, 2, 4), Set(1, 4, 5, 7))  Out: res53: Map[Int, Int] = Map(4 -> 5, 2 -> 4, 1 -> 1) In : trichotomy(Set(true, false), Set(3, 4, 5))  Out: res54: Map[Boolean, Int] = Map(false -> 4, true -> 3) In : trichotomy(Set(1, 2, 4), Set("Hello", "Hi"))  Out: res55: Map[Int, String] = Map(2 -> "Hi", 1 -> "Hello") In the finite case, this terminates by induction. In general, we have to use transfinite induction. Definition: A set A is said to be countable if |A| \leq |\mathbb{N}|. Otherwise we say it is uncountable. Propn: If A is countable either A is finite or |A| = \mathbb{N} ## Relations¶ A relation R on a set A is a subset of A \times A. We think of (a, b)\in R as A is related to R. Examples: • Two sets are related if they have the same cardinality. • Two sets A and B are related if |A| \leq |B|. • Two numbers are related if their difference is divisible by 3. • Two numbers n and m are related if n exactly divides m. In : def relation[A](s: Set[A], property : (A, A) => Boolean) = for { x <- s y <- s if property(x, y) } yield (x, y)  Out: defined function relation In : val s = (1 to 10).toSet val diffDiv3 = relation[Int](s, {(x, y) => (x - y) % 3 == 0})  Out: s: Set[Int] = Set(5, 10, 1, 6, 9, 2, 7, 3, 8, 4) diffDiv3: Set[(Int, Int)] = Set( (7, 1), (2, 5), (3, 9), (5, 2), (7, 4), (4, 10), (7, 7), (4, 7), (6, 6), (4, 1), (6, 9), (4, 4), (10, 10), (10, 1), (3, 6), (2, 8), (1, 1), (6, 3), (1, 10), (10, 7), (1, 4), (8, 2), (8, 8), (7, 10), (2, 2), (5, 5), (10, 4), (9, 6), (5, 8), (3, 3), (1, 7), (9, 9), (8, 5), (9, 3) ) In : val divides = relation[Int](s, (x, y) => y % x == 0)  Out: divides: Set[(Int, Int)] = Set( (1, 8), (1, 5), (3, 9), (7, 7), (2, 10), (6, 6), (4, 4), (5, 10), (10, 10), (1, 6), (3, 6), (2, 8), (1, 1), (1, 10), (1, 9), (1, 4), (2, 6), (8, 8), (1, 3), (2, 2), (5, 5), (4, 8), (2, 4), (3, 3), (1, 7), (1, 2), (9, 9) ) In : val sumDiv3 = relation[Int](s, (x, y) => (x + y) % 5 == 0)  Out: sumDiv3: Set[(Int, Int)] = Set( (10, 5), (6, 4), (7, 8), (9, 1), (4, 1), (6, 9), (5, 10), (10, 10), (2, 8), (7, 3), (4, 6), (1, 9), (1, 4), (8, 2), (3, 2), (5, 5), (3, 7), (9, 6), (2, 3), (8, 7) ) ### Properties of a relation R on S¶ • Reflexive : For all a\in S, (a, a)\in R • Symmetric : For all a, b\in S, if (a, b)\in R then (b, a)\in R. • Transitive : For all a, b, c\in S, if (a, b)\in R and (b, c)\in R then (a, c)\in R. In : def isReflexive[A](s: Set[A], r: Set[(A, A)]) = s.forall(x => r.contains((x, x)))  Out: defined function isReflexive In : isReflexive(s, diffDiv3) isReflexive(s, divides) isReflexive(s, sumDiv3)  Out: res61_0: Boolean = true res61_1: Boolean = true res61_2: Boolean = false In : def isSymmetric[A](s: Set[A], r: Set[(A, A)]) = r == r.map{case (x, y) => (y, x)}  Out: defined function isSymmetric In : isSymmetric(s, diffDiv3) isSymmetric(s, divides) isSymmetric(s, sumDiv3)  Out: res63_0: Boolean = true res63_1: Boolean = false res63_2: Boolean = true In : def isTransitive[A](s: Set[A], r: Set[(A, A)]) : Boolean = s.forall{a => s.forall{b => s.forall{c => !r.contains((a, b)) || !r.contains((b, c)) || r.contains((a, c)) }}}  Out: defined function isTransitive In : isTransitive(s, divides)  Out: res68: Boolean = true In : isTransitive(s, diffDiv3)  Out: res69: Boolean = true In : isTransitive(s, sumDiv3)  Out: res70: Boolean = false ### Reflexive, Symmetric, Transitive closures¶ If a relation R does not have one or more of these properties, we find the smallest relation on S that contains R and has the property. In : def reflexiveClosure[A](s: Set[A], r: Set[(A, A)]) = {r union s.map{a => (a, a)}}.ensuring{r1 => isReflexive(s, r1) && r.subsetOf(r1)}  Out: defined function reflexiveClosure In : reflexiveClosure(s, sumDiv3)  Out: res74: Set[(Int, Int)] = Set( (10, 5), (6, 4), (7, 7), (6, 6), (7, 8), (9, 1), (4, 1), (6, 9), (4, 4), (5, 10), (10, 10), (2, 8), (1, 1), (7, 3), (4, 6), (1, 9), (1, 4), (8, 2), (8, 8), (3, 2), (2, 2), (5, 5), (3, 7), (9, 6), (3, 3), (2, 3), (9, 9), (8, 7) ) In : def symmetricClosure[A](s: Set[A], r: Set[(A, A)]) = {r union r.map{case (a, b) => (b, a)}}.ensuring{ r1 => isSymmetric(s, r1) && r.subsetOf(r1) }  Out: defined function symmetricClosure In : symmetricClosure(s, divides)  Out: res76: Set[(Int, Int)] = Set( (7, 1), (1, 8), (1, 5), (10, 5), (3, 9), (5, 1), (7, 7), (2, 10), (6, 6), (3, 1), (9, 1), (6, 1), (4, 1), (6, 2), (8, 1), (4, 4), (5, 10), (10, 10), (1, 6), (10, 1), (3, 6), (2, 8), (1, 1), (6, 3), (1, 10), (1, 9), (1, 4), (2, 6), (10, 2), (8, 2), (8, 8), (1, 3), (2, 2), (5, 5), (4, 8), (4, 2), (2, 4), (8, 4), ... In : val diff2 = relation[Int](s, (x, y) => y -x == 2)  Out: diff2: Set[(Int, Int)] = Set( (7, 9), (8, 10), (6, 8), (3, 5), (4, 6), (5, 7), (1, 3), (2, 4) ) In : isTransitive(s, diff2)  Out: res78: Boolean = false In : def transiviteClosureStep[A](s: Set[A], r: Set[(A, A)]) = r union { for { a <- s b <- s c <- s if r.contains((a, b)) && r.contains((b, c)) } yield (a, c) }  Out: defined function transiviteClosureStep In : transiviteClosureStep(s, diff2)  Out: res80: Set[(Int, Int)] = Set( (1, 5), (7, 9), (8, 10), (6, 10), (5, 9), (6, 8), (3, 5), (4, 6), (2, 6), (5, 7), (1, 3), (4, 8), (2, 4), (3, 7) ) In : def transitiveClosure[A](s: Set[A], r : Set[(A, A)]) : Set[(A, A)] = { val nextStep = transiviteClosureStep(s, r) if (r == nextStep) r else transitiveClosure(s, nextStep) }.ensuring{r1 => isTransitive(s, r1) && r.subsetOf(r1) }  Out: defined function transitiveClosure In : transitiveClosure(s, diff2)  Out: res82: Set[(Int, Int)] = Set( (1, 5), (7, 9), (8, 10), (3, 9), (6, 10), (4, 10), (2, 10), (5, 9), (2, 8), (6, 8), (3, 5), (4, 6), (1, 9), (2, 6), (5, 7), (1, 3), (4, 8), (2, 4), (3, 7), (1, 7) ) ### Equivalence relation¶ An equivalence relation is a relation that is reflexive, symmetric and transitive. In : def isEquivalence[A](s: Set[A], r: Set[(A, A)]) : Boolean = isReflexive(s, r) && isSymmetric(s, r) && isTransitive(s, r)  Out: defined function isEquivalence In : def equivalenceClosure[A](s: Set[A], r: Set[(A, A)]) = transitiveClosure(s, symmetricClosure(s, reflexiveClosure(s, r))). ensuring{ r1 => isEquivalence(s, r1) && r.subsetOf(r1) }  Out: defined function equivalenceClosure In : val equivDiff2 = equivalenceClosure(s, diff2)  Out: equivDiff2: Set[(Int, Int)] = Set( (7, 1), (7, 5), (1, 5), (7, 9), (8, 10), (3, 9), (6, 10), (5, 1), (4, 10), (6, 4), (7, 7), (2, 10), (6, 6), (3, 1), (9, 1), (5, 9), (6, 2), (4, 4), (10, 10), (2, 8), (6, 8), (1, 1), (3, 5), (7, 3), (4, 6), (1, 9), (2, 6), (10, 2), (8, 2), (8, 8), (5, 7), (9, 7), (10, 6), (1, 3), (2, 2), (5, 5), (4, 8), (4, 2), ... We say the orbit of x in an equivalence relation R is$$\{y \in S: (x, y)\in R\}$$In : def orbit[A](x: A, s: Set[A], r: Set[(A, A)]) = s.filter{y => r.contains((x, y))}  Out: defined function orbit In : def orbitMap[A](s: Set[A], r: Set[(A, A)]) = s.map{x => x -> orbit(x, s, r)}  Out: defined function orbitMap In : orbitMap(s, equivDiff2)  Out: res91: Set[(Int, Set[Int])] = Set( (2, Set(10, 6, 2, 8, 4)), (7, Set(5, 1, 9, 7, 3)), (1, Set(5, 1, 9, 7, 3)), (10, Set(10, 6, 2, 8, 4)), (8, Set(10, 6, 2, 8, 4)), (4, Set(10, 6, 2, 8, 4)), (3, Set(5, 1, 9, 7, 3)), (6, Set(10, 6, 2, 8, 4)), (9, Set(5, 1, 9, 7, 3)), (5, Set(5, 1, 9, 7, 3)) ) In : orbitMap(s, diffDiv3)  Out: res92: Set[(Int, Set[Int])] = Set( (8, Set(5, 2, 8)), (10, Set(10, 1, 7, 4)), (2, Set(5, 2, 8)), (3, Set(6, 9, 3)), (4, Set(10, 1, 7, 4)), (1, Set(10, 1, 7, 4)), (5, Set(5, 2, 8)), (6, Set(6, 9, 3)), (7, Set(10, 1, 7, 4)), (9, Set(6, 9, 3)) ) Thus, for an equivalence relation R on S, the orbits form a partition of S, i.e., we get a collection of disjoint sets whose union is S. These are called equivalence classes. Furthermore, two elements x and y are related if and only if they both belong to some equivalence class. In [ ]:   In : orbitMap(s, sumDiv3)  Out: res93: Set[(Int, Set[Int])] = Set( (4, Set(1, 6)), (7, Set(3, 8)), (3, Set(2, 7)), (2, Set(3, 8)), (8, Set(2, 7)), (1, Set(9, 4)), (9, Set(1, 6)), (6, Set(9, 4)), (10, Set(5, 10)), (5, Set(5, 10)) ) In : isEquivalence(s, sumDiv3)  Out: res94: Boolean = false In : orbitMap(s, diff2)  Out: res95: Set[(Int, Set[Int])] = Set( (1, Set(3)), (5, Set(7)), (8, Set(10)), (7, Set(9)), (9, Set()), (10, Set()), (6, Set(8)), (3, Set(5)), (4, Set(6)), (2, Set(4)) ) In : orbitMap(Set(1, 2, 3, 4), Set((1, 1),(1, 3), (2, 2), (2, 3), (3, 1)))  Out: res97: Set[(Int, Set[Int])] = Set( (1, Set(1, 3)), (2, Set(2, 3)), (3, Set(1)), (4, Set()) ) ## Partial order¶ • A reflexive relation R on S is anti-symmetric if (a, b)\in R \land (b, a)\in R \implies a = b. • A partial-order is a relation that is reflexive, transitive and anti-symmetric. # Type theory¶ • In formal languages(e.g. FOL)/natural languages/programming languages, expressions/words and phrases/objects have types (parts of speech). • Rules for forming expressions are in terms of types only. • In First-order languages and Natural languages, the collection of types is fixed. A type theory means: • minimal view: there are rules forming new types. • maximal view: types are rich enough to form foundations replacing Set Theory and FOL as well as \lambda-calculus. In scala and most other languages, we have various types we can form. The most important is that given types A and B, we can form the function type A \to B. In : val next : Int => Int = (n: Int) => n + 1  Out: next: Int => Int = ammonite.sess.cmd98Helper$$Lambda$3651/1830093790@5989799a There are also prebuilt types and type constructors: pairs, unit and zero (nothing) In : (3, 4)  Out: res99: (Int, Int) = (3, 4) In : (3, "Hello World")  Out: res100: (Int, String) = (3, "Hello World") In : () : Unit  The Unit type is a type with just one object (in scala it is also called Unit). In : println _  Out: res103: () => Unit = ammonite.$sess.cmd103$Helper$$Lambda$3668/340148172@1c32095b
In :
val result = println("Hello types")

Hello types

In :
result

In :
Unit

Out:
res106: Unit.type = object scala.Unit

We also have inductive types, which are types whose objects are generated by given introduction rules. In scala these are given by a sealed trait and case class (or case object) statements.

In :
sealed trait BinTree

case object Leaf extends BinTree

case class Node(left: BinTree, right: BinTree) extends BinTree

Out:
defined trait BinTree
defined object Leaf
defined class Node
In :
val egTree : BinTree = Node(Node(Leaf, Leaf), Node(Node(Leaf, Leaf), Leaf))

Out:
egTree: BinTree = Node(Node(Leaf, Leaf), Node(Node(Leaf, Leaf), Leaf))

Functions on these can be defined by recursion/induction.

In :
def vertices(t: BinTree) : Int = t match {
case Leaf => 1
case Node(t1, t2) => vertices(t1) + vertices(t2) + 1
}

Out:
defined function vertices
In :
vertices(egTree)

Out:
res111: Int = 9

Types, including inductive types, can depend on other types. For example, we can define Labelled trees labelled with leaves having labels in $A$. We call these type families.

In :
sealed trait LabelledTree[A]

case class LabelledLeaf[A](label: A) extends LabelledTree[A]

case class LabelledNode[A](
left: LabelledTree[A], right: LabelledTree[A]
) extends LabelledTree[A]

Out:
defined trait LabelledTree
defined class LabelledLeaf
defined class LabelledNode
In :
val egLT = LabelledNode(LabelledLeaf(1),
LabelledNode(LabelledLeaf(2), LabelledLeaf(3)))

Out:
egLT: LabelledNode[Int] = LabelledNode(
LabelledLeaf(1),
LabelledNode(LabelledLeaf(2), LabelledLeaf(3))
)
In :
val stringyTree = LabelledNode(LabelledLeaf("Hello"),
LabelledNode(LabelledLeaf("Tree"),
LabelledLeaf("with labels")))

Out:
stringyTree: LabelledNode[String] = LabelledNode(
LabelledLeaf("Hello"),
LabelledNode(LabelledLeaf("Tree"), LabelledLeaf("with labels"))
)
In :
def labels[A](t: LabelledTree[A]) : Vector[A] = t match {
case LabelledLeaf(l : A) => Vector(l)
case LabelledNode(t1, t2) => labels(t1) ++ labels(t2)
}

Out:
defined function labels
In :
labels(egLT)

Out:
res116: Vector[Int] = Vector(1, 2, 3)
In :
labels(stringyTree)

Out:
res117: Vector[String] = Vector("Hello", "Tree", "with labels")
In :
def cannotDefine : Nothing = ??? // Nothing is a type with no objects

Out:
defined function cannotDefine

A type system at this level allows us to check some properties, but not all at the level of syntax (i.e. at compile time).

In :
// math.sqrt("Hello world") - will not compile
Try(math.sqrt(-1)) // this will compile

Out:
res119: Try[Double] = Success(NaN)

For example, if we want to take half of only even integers, we can do this using require and ensuring but not at type level (in a simple way).

In :
def half(n: Int) : Int = {
require(n %2 == 0, "cannot take half of an odd number")
n /2
}

Out:
defined function half
In :
def double(n: Int) : Int = (2 * n).ensuring{k => k % 2 == 0}

Out:
defined function double
In :
def halfDouble(n: Int) = half(double(n))
(1 to 10).map(halfDouble)

Out:
defined function halfDouble
res122_1: collection.immutable.IndexedSeq[Int] = Vector(
1,
2,
3,
4,
5,
6,
7,
8,
9,
10
)
In :
Try(half(3))

Out:
res123: Try[Int] = Failure(
java.lang.IllegalArgumentException: requirement failed: cannot take half of an odd number
)

In dependent type theory, we will have types that represent, for example, that a number is even. Specifically

• types will be first-class.
• types, including inductive types, can depend on terms (objects).
In :
// A bad definition
def recHalf(n: Int) : Int = if (n == 0) 0 else recHalf(n - 2) + 1

Out:
defined function recHalf
In :
recHalf(10)

Out:
res125: Int = 5
In [ ]: