The category of propositional functions

propositional function Frege's analysis of propositions into functions and arguments is central to modern logic. It requires us to consider the notion of a propositional function. Frege starts with concrete propositions such as 0 < 1, then abstracts with respect to a term to obtain a form like 0 < x which denotes a function in x. In Principia notation, given a proposition $\phi a$, $\phi x$ is the ambiguous value, and the propositional function is $\phi \hat{x}$; so 0 < 1 can be factored as $\phi 1$ and abstracted as $0 < \hat{x}$. Also, in Principia a type is defined to be the range of significance of a propositional function; we might write the type as $type(x. \phi x)$. So the function maps this type to Prop. For example, $\frac{1}{3} < \frac{1}{2}$ might be abstracted to $\frac{1}{x} < \frac{1}{2}$; it is not meaningful for x = 0.

In the logic presented here, propositional functions also map types T to Prop. Given a type T we denote the category of propositional functions over T as $T \rightarrow Prop$. Instead of using 0 < x, we denote the abstractions in the manner of Church with lambda notationlambda notation, $\lambda(x.\ 0 < x)$. The details of the function notation will not concern us until section 2.9. It suffices now to say that given a specific proposition such as 0 < 1, we require that the individuals such as 0, 1 be elements of types, here ${{\mathbb{N} }}$. The function maps ${{\mathbb{N} }}$ to Prop, thus an element of the category $({{\mathbb{N} }} \rightarrow Prop)$. Given a function P in $(T \rightarrow Prop)$ and t in the type T, then P(t) denotes the application of P to t just as in ordinary mathematics.