What is a finite partial function from $\mathfrak c$ to $D=\{0,1\}$

Question

While I reading a paper, there is a notation is called finite partial function. I searched by google, I cannot find its definition. So I post it here as a question:

What is a finite partial function from $\mathfrak c$ to $D=\{0,1\}$?

Thanks!

Answer 1

Posting the comment as an answer:

It is a function with range contained in $D$, and domain a finite subset of $\mathfrak c$. In general, a partial function from $A$ to $B$ is a function $f$ with domain some subset of $A$ and range (contained in) $B$. If the domain of $f$ is $A$, one says that $f$ is a total function.

I believe it was Adrian Mathias who introduced the notation $f\mathrel{\vdots}A\to B$ to indicate that $f$ is a partial function from $A$ to $B$. In computability theory, one sees the notation $f(x)\downarrow$ to indicate that $x\in\mathrm{dom}(f)$, and $f(x)\uparrow$ to indicate otherwise. The idea is that one thinks of $f$ as a program performing a computation with input $x$. The downarrow indicates that the computation converges, and the uparrow, that it diverges.

In set theory, in the context of forcing, it is common to talk of partial functions. Given a poset of partial functions, typically, the generic object $G$ one obtains gives us a total function, obtained by pasting together the partial approximations in $G$.