edom.web.id

Logic

Order of a type

The order of a type is: \[ \begin{align*} ord~(\sigma \to \tau) &= 1 + ord~\sigma \\ ord~\sigma &= 0 \text{ for $\sigma$ that is not a function type.} \end{align*} \]

Introduction

A Bool is either False or True: \[ False : Bool \\ True : Bool. \]

The type of a proposition: \[ Prop = Bool. \]

The type of a predicate: \[ Pred~a = a \to Bool. \]

A proposition whose truth depends on context is a predicate: \[ ContextualProposition = Pred~Context. \]

A relation is also a predicate (by currying): \[ \begin{align*} Rel~n~a_0~\ldots~a_m &= a_0 \to \ldots \to a_m \to Bool \\ &\sim (a_0,\ldots,a_m) \to Bool \\ &\sim Pred~(a_0,\ldots,a_m) \end{align*} \] where \(n = m + 1\).

The type of a quantifier: \[ \forall : Pred~a \to Bool \\ \exists : Pred~a \to Bool. \]

Example usages of quantifiers: \[ \forall~(\lambda p. \text{$p : \mathbb{N}$} \implies \text{$p$ is even}) \\ \exists~(\lambda n. n : \mathbb{N} \wedge n \bmod 2 = 0) \\ \forall~(\lambda x. \exists~(\lambda y. x + y = 0)) \\ \forall~(\lambda x. \forall~(\lambda y. \exists~(\lambda z. x+y=z))) \]