1.3.1: Basics

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

A function is a map which sends each element of a given set to a specific element in some (other) given set. For instance, the operation of adding \(1\) defines a function: each number \(n\) is mapped to a unique number \(n+1\).

More generally, functions may take pairs, triples, etc., as inputs and returns some kind of output. Many functions are familiar to us from basic arithmetic. For instance, addition and multiplication are functions. They take in two numbers and return a third.

In this mathematical, abstract sense, a function is a black box: what matters is only what output is paired with what input, not the method for calculating the output.

Definition \(\PageIndex{1}\): Function

A function \(f \colon A \to B\) is a mapping of each element of \(A\) to an element of \(B\).

We call \(A\) the domain of \(f\) and \(B\) the codomain of \(f\). The elements of \(A\) are called inputs or arguments of \(f\), and the element of \(B\) that is paired with an argument \(x\) by \(f\) is called the value of \(f\) for argument \(x\), written \(f(x)\).

The range \(\ran{f}\) of \(f\) is the subset of the codomain consisting of the values of \(f\) for some argument; \(\ran{f} = \Setabs{f(x)}{x \in A}\).

The diagram in Figure \(\PageIndex{1}\) may help to think about functions. The ellipse on the left represents the function’s domain; the ellipse on the right represents the function’s codomain; and an arrow points from an argument in the domain to the corresponding value in the codomain.

Figure \(\PageIndex{1}\): A function is a mapping of each element of one set to an element of another. An arrow points from an argument in the domain to the corresponding value in the codomain.

Example \(\PageIndex{1}\)

Multiplication takes pairs of natural numbers as inputs and maps them to natural numbers as outputs, so goes from \(\Nat \times \Nat\) (the domain) to \(\Nat\) (the codomain). As it turns out, the range is also \(\Nat\), since every \(n \in \Nat\) is \(n \times 1\).

Example \(\PageIndex{2}\)

Multiplication is a function because it pairs each input—each pair of natural numbers—with a single output: \(\times \colon \Nat^2 \to \Nat\). By contrast, the square root operation applied to the domain \(\Nat\) is not functional, since each positive integer \(n\) has two square roots: \(\sqrt{n}\) and \(-\sqrt{n}\). We can make it functional by only returning the positive square root: \(\sqrt{\phantom{X}} \colon \Nat \to \Real\).

Example \(\PageIndex{3}\)

The relation that pairs each student in a class with their final grade is a function—no student can get two different final grades in the same class. The relation that pairs each student in a class with their parents is not a function: students can have zero, or two, or more parents.

We can define functions by specifying in some precise way what the value of the function is for every possible argment. Different ways of doing this are by giving a formula, describing a method for computing the value, or listing the values for each argument. However functions are defined, we must make sure that for each argment we specify one, and only one, value.

Example \(\PageIndex{4}\)

Let \(f \colon \Nat \to \Nat\) be defined such that \(f(x) = x+1\). This is a definition that specifies \(f\) as a function which takes in natural numbers and outputs natural numbers. It tells us that, given a natural number \(x\), \(f\) will output its successor \(x+1\). In this case, the codomain \(\Nat\) is not the range of \(f\), since the natural number \(0\) is not the successor of any natural number. The range of \(f\) is the set of all positive integers, \(\Int^{+}\).

Example \(\PageIndex{5}\)

Let \(g \colon \Nat \to \Nat\) be defined such that \(g(x) = x+2-1\). This tells us that \(g\) is a function which takes in natural numbers and outputs natural numbers. Given a natural number \(n\), \(g\) will output the predecessor of the successor of the successor of \(x\), i.e., \(x+1\).

We just considered two functions, \(f\) and \(g\), with different definitions. However, these are the same function. After all, for any natural number \(n\), we have that \(f(n) = n+1 = n+2-1 = g(n)\). Otherwise put: our definitions for \(f\) and \(g\) specify the same mapping by means of different equations. Implicitly, then, we are relying upon a principle of extensionality for functions, \[\text{if }\forall x\, f(x) = g(x)\text{, then }f = g\nonumber\] provided that \(f\) and \(g\) share the same domain and codomain.

Example \(\PageIndex{6}\)

We can also define functions by cases. For instance, we could define \(h \colon \Nat \to \Nat\) by \[h(x) = \begin{cases} \frac{x}{2} & \text{if $x$ is even} \\ \frac{x+1}{2} & \text{if $x$ is odd.} \end{cases}\nonumber\] Since every natural number is either even or odd, the output of this function will always be a natural number. Just remember that if you define a function by cases, every possible input must fall into exactly one case. In some cases, this will require a proof that the cases are exhaustive and exclusive.