Pure propositions

pure proposition

The traditional approach to studying logic is to first isolate the propositional calculus and then the first-order predicate calculus, and to study completeness results for these calculi, since completeness results tie together the semantic and proof-theoretic concepts. These topics are covered by defining restricted formal languages. We will take this approach to typed logic starting in section 2.4 on formulas. But many of the concepts can also be presented by a mathematical analysis of propositional functions without resort to linguistic mechanisms and formulas.

There is one outstanding technical problem about the propositional calculus which benefits from this direct analysis, namely a functional approach to completeness of the intuitionistic propositional calculus. The most widely known completeness theorem for this calculus is based on Kripke semanticsKripke semantics ([71]); this account of propositional calculus semantics, while illuminating and technically elegant, and even constructively meaningful, is not faithful to constructive semantics. In particular, it is not based on the type-theoretic semantics we offer in part 3. Providing a completeness result for a constructively faithful semantics is an open area, and it seems to me that Martin-Löf's inductive semantics has created new opportunities here to produce definitive results.

The key to a constructive semantics might be a careful study of a functional approach to propositions that allows us to express the functional uniformity of proofs that is central to completeness.¹⁴ As a start, we can try to understand the basic concept of a pure propositional function without resort to formal languages.

Consider a propositional function of one argument, $P \Rightarrow P$. This can be understood as a function from Prop to Prop.¹⁵ The function $P \Rightarrow(Q \Rightarrow P)$ in variables P, Q is a two-argument function, most naturally from Prop to $(Prop \rightarrow Prop)$ as would be clear from writing the function as

$$\lambda(P.\ \lambda(Q.\ P \Rightarrow (Q \Rightarrow P))).$$

We could also think of this as a mapping from $Prop \times Prop$ to Prop if we took pairs as arguments (writing $\lambda(z.\ 1o\!f(z) \Rightarrow (2o\!f(z) \Rightarrow 1o\!f(z)))$ in $Prop^2 \rightarrow Prop$). For ease of analysis, we will consider propositional functions from the Cartesian power, Propⁿ, into Prop. The constants $\top$ and $\bot$ are regarded as zero-ary functions, and for convenience define Prop⁰ = 1 for 1 the unit typeunit type. Then $f(x) = \top$ and $f(x) = \bot$ are in $Prop^0 \rightarrow Prop$.

The idea is to define the pure propositional functions pure propositional function inductively as a subtype of $Prop^n \rightarrow Prop$ constructed using only constant functions, simple projections like $proj^n_i(P_1, \ldots, P_n) = P_i$ and the operations $\&, \vee, \Rightarrow$ lifted up to the level of functions.

Each connective $\&, \vee, \Rightarrow$ can be lifted to the functions $Prop^n \rightarrow Prop$, namely given f and g, define $(f\: op\: g)(\bar{P}) = f(\bar{P})\: op\: g(\bar{P})$ where $\bar{P} \in Prop^n$. For example, if f(P, Q) = P and $g(P, Q) = (Q \Rightarrow P)$ then $f \Rightarrow g$ is a function h such that $h(P, Q) = (P \Rightarrow(Q\Rightarrow P)).$

We can now define the general abstract propositional functions of n variables call the class ${\cal{P}}_n$ as the inductive subset of $Prop^n \rightarrow Prop$ whose base elements are the constant and projection functions,

	$C_{\top}(\bar{P}) = \mathbf{\top}$	$C_{\bot}(\bar{P}) = \mathbf{\bot}$
	$proj^n_i(\bar{P}) = P_i$	where $\bar{P} = \langle P_1, \ldots, P_n\rangle$ and $1 \leq i \leq n$.

¹⁶

Then given $f, g \in {\cal{P}}_n$ and given any lifted connective op, we have $(f\: op\: g) \in {\cal{P}}_n$. Nothing else belongs to ${\cal{P}}_n$. When we want to mention the underlying type, we write ${\cal{P}}_n$ as ${\cal P}(Prop^n \rightarrow Prop)$. Let ${\cal P} = {\displaystyle \bigcup_{n=0}^{\infty}} {\cal P}_n$; these are the pure propositionspure proposition. Note that ${\cal P} = {\displaystyle \bigcup^{\infty}_{n=0}} {\cal P}(Prop^n \rightarrow Prop)$ is inductively defined. The validvalid element elements of ${\cal P}$ are those functions $f \in {\cal P}$ such that for $f \in {\cal P}_n$ and $\bar{{\cal P}}$ any element of $Prop^n, f(\bar{{\cal P}})$ is true. Call these $True({\cal P})$.

Using these concepts we can express the idea of a uniform functional proof. The simplest approach is probably to use a Hilbert style axiomatic base. If we take Heyting's or Kleene's axioms for the intuitionistic propositional calculus, then we can define $Provable_H({\cal P})$ inductively. The completeness theorem we want is then $True({\cal P}) = Provable_H({\cal P})$.

We can use the same technique to define the pure typed propositional functions. First we need to define pure type functionspure typed function ${\cal T}$ as a subset of Type $^n \rightarrow$ Type for $n=1, 2, \ldots$. We take $n \geq 1$ since there are as yet no constant types to include. An example is $t(A, B) = A \times B$. Next we define the typed propositional functions $p : t(\bar{T}) \rightarrow Prop$.

In general we need to consider functions whose inputs are n-tuples of the type

$$(t_1(\bar{T}) \rightarrow Prop) \times \ldots \times (t_n(\bar{T}) \rightarrow Prop)$$

and whose output is a Prop. We do not pursue this topic further here, but when we examine the proof system for typed propositions we will see that it offers a simple way to provide abstract proofs for pure typed propositions that use only rules for the connectives and quantifiers -- say a pure proofpure proof. There are various results suggesting that if there is any proof of these pure propositions, then there is a pure proof. These are completeness results for this typed version of the predicate calculus. We will not prove them here.