Propositional calculus

Consider first the case of formulas to represent the pure propositions. The standard way to do this is to inductively define a class of propositional formulasformula!propositional, PropFormula. The base case includes the propositional constants, $Constants = \{\top, \perp\}$, and propositional variablesvariable, $Variables = \{P, Q, R, P_1, Q_1, R_1, \ldots\}$. These are propositional formulas. The inductive case is

If F, G are PropFormulas, then so are $(F\; \&\; G)$, $(F \vee G)$, and $(F \Rightarrow G)$. Nothing else is a PropFormula.

We can assign to every formula a mathematical meaning as a pure proposition. Given a formula F, let $P_1, \ldots, P_n$ be the propositional variables occurring in it (say ordered from left to right); let $\bar{P}$ be the vector of them. Define a map from n variable propositional formulas, PropFormulas_n, into $(Prop^n \rightarrow \ Prop)$ inductively by

For each variable P_i, corresponds to the projection function $proj^n_i(\bar{P}) = P_i$. Say that F is validvalid iff ${\lbrack\!\lbrack}F {\rbrack\!\rbrack}$ is a valid pure proposition.