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 [1]:
case class Function(name: String, degree: Int)

case class Relation(name: String, degree: Int)
Out[1]:
defined class Function
defined class Relation

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

In [2]:
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[2]:
defined trait Expression
defined trait Term
defined trait Formula
defined object Term
defined object Formula
In [3]:
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[3]:
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 [4]:
// An invalid term
import scala.util.Try
val wrong = Try(Recursive(succ, Vector(one, n)))
Out[4]:
import scala.util.Try

wrong: Try[Recursive] = Failure(
  java.lang.IllegalArgumentException: requirement failed
)
In [5]:
// 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[5]:
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 [6]:
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[6]:
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 [7]:
val a = Var("a")
def sameMembers(p: Term, q: Term): Formula = 
    ForAll(a, Equivalent(belongs(a, p), belongs(a, q)))
Out[7]:
a: Var = Var("a")
defined function sameMembers
In [8]:
val x = Var("x")
val y = Var("y")
val extensionality = 
   ForAll(x, 
         ForAll(y,
               Implies(sameMembers(x, y), Equality(x, y))))
Out[8]:
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 [9]:
// 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[9]:
defined function variables
In [10]:
variables(Recursive(sum, Vector(n, m)))
Out[10]:
res9: Set[Var] = Set(Var("n"), Var("m"))
In [11]:
val p = Recursive(succ, Vector(m))
variables(Recursive(sum, Vector(n, p)))
Out[11]:
p: Recursive = Recursive(Function("succ", 1), Vector(Var("m")))
res10_1: Set[Var] = Set(Var("n"), Var("m"))
In [12]:
variables(p)
Out[12]:
res11: Set[Var] = Set(Var("m"))
In [13]:
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[13]:
defined function freeVariables
In [14]:
val fmla1 = Exists(x, belongs(x, y))
val fmla2 = ForAll(y, fmla1)
val fmla3 = belongs(x, y)
Out[14]:
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 [15]:
freeVariables(fmla1)
freeVariables(fmla2)
freeVariables(fmla3)
Out[15]:
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 [16]:
val russell = Not(belongs(x, x))
freeVariables(russell)
Out[16]:
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 [17]:
// 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[17]:
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 [18]:
Set(1, 3, 4) union Set(3, 7, 9)
Out[18]:
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 [19]:
// union of sets
val setOfSets = Set(Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
val bigUnion = setOfSets.flatten
Out[19]:
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 [20]:
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[20]:
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 [21]:
Set[Any](Set(1, 2)).subsetOf(big)
Out[21]:
res20: Boolean = true
In [22]:
val anotherBig = Set[Any](1, Set(1), Set(1, 2), Set[Any](2, Set(1, 3)))
Out[22]:
anotherBig: Set[Any] = Set(1, Set(1), Set(1, 2), Set(2, Set(1, 3)))
In [23]:
anotherBig contains 1
Out[23]:
res22: Boolean = true
In [24]:
Set[Any](1) subsetOf anotherBig
anotherBig contains Set(1)
Out[24]:
res23_0: Boolean = true
res23_1: Boolean = true
In [25]:
import scala.collection.mutable.{Set => mSet}
val ss = mSet[Any](mSet(1), mSet(2))
Out[25]:
import scala.collection.mutable.{Set => mSet}

ss: collection.mutable.Set[Any] = Set(Set(1), Set(2))
In [26]:
ss += mSet(3, 4)
Out[26]:
res25: collection.mutable.Set[Any] = Set(Set(1), Set(2), Set(3, 4))
In [27]:
ss += 1
Out[27]:
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 [28]:
val A = Set(1, 2, 3) 
val B = Set(2,3, 7, 9)
A intersect B
Out[28]:
A: Set[Int] = Set(1, 2, 3)
B: Set[Int] = Set(2, 3, 7, 9)
res27_2: Set[Int] = Set(2, 3)
In [29]:
A.filter(x => B contains x)
Out[29]:
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 [30]:
Set(1, 2, 7).subsets.toSet
Out[30]:
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 [31]:
Set().subsets.toSet
Out[31]:
res30: Set[Set[Nothing]] = Set(Set())
In [32]:
Set().subsets.toSet.size
Out[32]:
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 [33]:
def succ(s: Set[Any]) : Set[Any] = s union Set(s)
succ(Set(1, 2))
Out[33]:
defined function succ
res32_1: Set[Any] = Set(1, 2, Set(1, 2))
In [34]:
def numberSet(n: Int): Set[Any] =
     if (n == 0) Set() else succ(numberSet(n - 1))
numberSet(3)
Out[34]:
defined function numberSet
res33_1: Set[Any] = Set(Set(), Set(Set()), Set(Set(), Set(Set())))
In [35]:
(0 to 10).map (n => numberSet(n).size)
Out[35]:
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 [36]:
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[36]:
defined function isInjective
In [37]:
isInjective((1 to 10).toSet, (1 to 30).toSet, (n: Int) => 2 * n)
Out[37]:
res36: Boolean = true
In [38]:
isInjective((1 to 10).toSet, (1 to 30).toSet, (n: Int) => n/ 2)
Out[38]:
res37: Boolean = false
In [39]:
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[39]:
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 [40]:
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[40]:
defined function range
res39_1: Set[Int] = Set(1, 2)
res39_2: Set[Int] = Set(1, 3, 2)
In [41]:
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[41]:
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 [42]:
def isBijective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
    isSurjective(domain, codomain, f) && isInjective(domain, codomain, f)
Out[42]:
defined function isBijective
In [43]:
isBijective(Set(1, 2, 3), Set(2, 4, 6), Map(1 -> 2, 2-> 4, 3 -> 6))
Out[43]:
res42: Boolean = true
In [44]:
isBijective(
    Set(1, 2, 3), Set(1, 2, 3, 4, 5, 6), Map(1 -> 2, 2-> 4, 3 -> 6)
)
Out[44]:
res43: Boolean = false
In [45]:
isBijective(Set(1, 2, 3), Set(1, 2, 3), Map(1 -> 2, 2-> 1, 3 -> 1))
Out[45]:
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 [46]:
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[46]:
defined function inverseFunction
res45_1: Int => Int = ammonite.$sess.cmd45$Helper$$Lambda$2934/99060392@286ef9a7
In [47]:
Try{
    inverseFunction(Set(1, 2, 3), 
                    Set(1, 2, 3), Map(1 -> 2, 2 ->1, 3 -> 1))
}
Out[47]:
res46: Try[Int => Int] = Failure(
  java.lang.IllegalArgumentException: requirement failed: can only invert bijections
)
In [48]:
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[48]:
defined function inverseMap
In [49]:
inverseMap(Set(1, 2, 3), Set(4, 5, 6), Map(1 -> 4, 2 -> 6, 3 -> 5))
Out[49]:
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 [50]:
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[50]:
defined function cantor
In [51]:
cantor(Set(1, 2, 3), Map(1 -> Set(1), 2 -> Set(1, 2), 3 -> Set(1, 2, 3)))
Out[51]:
res50: Set[Int] = Set()
In [52]:
cantor(Set(1, 2, 3), Map(1 -> Set(1), 2 -> Set(1, 2), 3 -> Set(1, 2)))
Out[52]:
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 [53]:
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[53]:
defined function trichotomy
In [54]:
trichotomy(Set(1, 2, 4), Set(1, 4, 5, 7))
Out[54]:
res53: Map[Int, Int] = Map(4 -> 5, 2 -> 4, 1 -> 1)
In [55]:
trichotomy(Set(true, false), Set(3, 4, 5))
Out[55]:
res54: Map[Boolean, Int] = Map(false -> 4, true -> 3)
In [56]:
trichotomy(Set(1, 2, 4), Set("Hello", "Hi"))
Out[56]:
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 [57]:
def relation[A](s: Set[A], property : (A, A) => Boolean) =
       for {
           x <- s
           y <- s
           if property(x, y)
       } yield (x, y)
Out[57]:
defined function relation
In [58]:
val s = (1 to 10).toSet
val diffDiv3 = relation[Int](s, {(x, y) => (x - y) % 3 == 0})
Out[58]:
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 [59]:
val divides = relation[Int](s, (x, y) => y % x == 0)
Out[59]:
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 [60]:
val sumDiv3 = relation[Int](s, (x, y) => (x + y) % 5 == 0)
Out[60]:
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 [61]:
def isReflexive[A](s: Set[A], r: Set[(A, A)]) = 
      s.forall(x => r.contains((x, x)))
Out[61]:
defined function isReflexive
In [62]:
isReflexive(s, diffDiv3)
isReflexive(s, divides)
isReflexive(s, sumDiv3)
Out[62]:
res61_0: Boolean = true
res61_1: Boolean = true
res61_2: Boolean = false
In [63]:
def isSymmetric[A](s: Set[A], r: Set[(A, A)]) =
        r == r.map{case (x, y) => (y, x)}
Out[63]:
defined function isSymmetric
In [64]:
isSymmetric(s, diffDiv3)
isSymmetric(s, divides)
isSymmetric(s, sumDiv3)
Out[64]:
res63_0: Boolean = true
res63_1: Boolean = false
res63_2: Boolean = true
In [68]:
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[68]:
defined function isTransitive
In [69]:
isTransitive(s, divides)
Out[69]:
res68: Boolean = true
In [70]:
isTransitive(s, diffDiv3)
Out[70]:
res69: Boolean = true
In [71]:
isTransitive(s, sumDiv3)
Out[71]:
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 [74]:
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[74]:
defined function reflexiveClosure
In [75]:
reflexiveClosure(s, sumDiv3)
Out[75]:
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 [76]:
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[76]:
defined function symmetricClosure
In [77]:
symmetricClosure(s, divides)
Out[77]:
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 [78]:
val diff2 = relation[Int](s, (x, y) => y -x == 2)
Out[78]:
diff2: Set[(Int, Int)] = Set(
  (7, 9),
  (8, 10),
  (6, 8),
  (3, 5),
  (4, 6),
  (5, 7),
  (1, 3),
  (2, 4)
)
In [79]:
isTransitive(s, diff2)
Out[79]:
res78: Boolean = false
In [80]:
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[80]:
defined function transiviteClosureStep
In [81]:
transiviteClosureStep(s, diff2)
Out[81]:
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 [82]:
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[82]:
defined function transitiveClosure
In [83]:
transitiveClosure(s, diff2)
Out[83]:
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 [84]:
def isEquivalence[A](s: Set[A], r: Set[(A, A)]) : Boolean =
     isReflexive(s, r) && isSymmetric(s, r) && isTransitive(s, r)
Out[84]:
defined function isEquivalence
In [86]:
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[86]:
defined function equivalenceClosure
In [89]:
val equivDiff2 = equivalenceClosure(s, diff2)
Out[89]:
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 [88]:
def orbit[A](x: A, s: Set[A], r: Set[(A, A)]) =
      s.filter{y => r.contains((x, y))}
Out[88]:
defined function orbit
In [91]:
def orbitMap[A](s: Set[A], r: Set[(A, A)]) = 
     s.map{x => x -> orbit(x, s, r)}
Out[91]:
defined function orbitMap
In [92]:
orbitMap(s, equivDiff2)
Out[92]:
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 [93]:
orbitMap(s, diffDiv3)
Out[93]:
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 [94]:
orbitMap(s, sumDiv3)
Out[94]:
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 [95]:
isEquivalence(s, sumDiv3)
Out[95]:
res94: Boolean = false
In [96]:
orbitMap(s, diff2)
Out[96]:
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 [98]:
orbitMap(Set(1, 2, 3, 4), Set((1, 1),(1, 3), (2, 2), (2, 3), (3, 1)))
Out[98]:
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 [99]:
val next : Int => Int = (n: Int) => n + 1
Out[99]:
next: Int => Int = ammonite.$sess.cmd98$Helper$$Lambda$3651/1830093790@5989799a

There are also prebuilt types and type constructors: pairs, unit and zero (nothing)

In [100]:
(3, 4)
Out[100]:
res99: (Int, Int) = (3, 4)
In [101]:
(3, "Hello World")
Out[101]:
res100: (Int, String) = (3, "Hello World")
In [103]:
() : Unit

The Unit type is a type with just one object (in scala it is also called Unit).

In [104]:
println _
Out[104]:
res103: () => Unit = ammonite.$sess.cmd103$Helper$$Lambda$3668/340148172@1c32095b
In [105]:
val result = println("Hello types")

Hello types
In [106]:
result
In [107]:
Unit
Out[107]:
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 [108]:
sealed trait BinTree

case object Leaf extends BinTree

case class Node(left: BinTree, right: BinTree) extends BinTree
Out[108]:
defined trait BinTree
defined object Leaf
defined class Node
In [110]:
val egTree : BinTree = Node(Node(Leaf, Leaf), Node(Node(Leaf, Leaf), Leaf))
Out[110]:
egTree: BinTree = Node(Node(Leaf, Leaf), Node(Node(Leaf, Leaf), Leaf))

Functions on these can be defined by recursion/induction.

In [111]:
def vertices(t: BinTree) : Int = t match {
    case Leaf => 1
    case Node(t1, t2) => vertices(t1) + vertices(t2) + 1
}
Out[111]:
defined function vertices
In [112]:
vertices(egTree)
Out[112]:
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 [113]:
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[113]:
defined trait LabelledTree
defined class LabelledLeaf
defined class LabelledNode
In [114]:
val egLT = LabelledNode(LabelledLeaf(1), 
                        LabelledNode(LabelledLeaf(2), LabelledLeaf(3)))
Out[114]:
egLT: LabelledNode[Int] = LabelledNode(
  LabelledLeaf(1),
  LabelledNode(LabelledLeaf(2), LabelledLeaf(3))
)
In [115]:
val stringyTree = LabelledNode(LabelledLeaf("Hello"), 
                        LabelledNode(LabelledLeaf("Tree"), 
                                     LabelledLeaf("with labels")))
Out[115]:
stringyTree: LabelledNode[String] = LabelledNode(
  LabelledLeaf("Hello"),
  LabelledNode(LabelledLeaf("Tree"), LabelledLeaf("with labels"))
)
In [116]:
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[116]:
defined function labels
In [117]:
labels(egLT)
Out[117]:
res116: Vector[Int] = Vector(1, 2, 3)
In [118]:
labels(stringyTree)
Out[118]:
res117: Vector[String] = Vector("Hello", "Tree", "with labels")
In [119]:
def cannotDefine : Nothing = ??? // Nothing is a type with no objects
Out[119]:
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 [120]:
// math.sqrt("Hello world") - will not compile
Try(math.sqrt(-1)) // this will compile
Out[120]:
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 [121]:
def half(n: Int) : Int = {
    require(n %2 == 0, "cannot take half of an odd number")
    n /2
}
Out[121]:
defined function half
In [122]:
def double(n: Int) : Int = (2 * n).ensuring{k => k % 2 == 0}
Out[122]:
defined function double
In [123]:
def halfDouble(n: Int) = half(double(n))
(1 to 10).map(halfDouble)
Out[123]:
defined function halfDouble
res122_1: collection.immutable.IndexedSeq[Int] = Vector(
  1,
  2,
  3,
  4,
  5,
  6,
  7,
  8,
  9,
  10
)
In [124]:
Try(half(3))
Out[124]:
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 [125]:
// A bad definition
def recHalf(n: Int) : Int = if (n == 0) 0 else recHalf(n - 2) + 1
Out[125]:
defined function recHalf
In [126]:
recHalf(10)
Out[126]:
res125: Int = 5
In [ ]: