# 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)))$