Changes

Here, a notation of the form <math>x \underset{A}{\Downarrow}</math> means that <math>x\!</math> is of the type <math>A,\!</math> while a notation of the form <math>x \overset{A}{\underset{B}{\Downarrow}}</math> means that <math>x\!</math> is of the type <math>A \Rightarrow B.</math>

Here, a notation of the form <math>x \underset{A}{\Downarrow}</math> means that <math>x\!</math> is of the type <math>A,\!</math> while a notation of the form <math>x \overset{A}{\underset{B}{\Downarrow}}</math> means that <math>x\!</math> is of the type <math>A \Rightarrow B.</math>

Note that the explication of <math>\operatorname{P}</math> as a term <math>\operatorname{K}((\operatorname{S}\operatorname{K})\operatorname{S})</math> of type <math>(B \Rightarrow C) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))</math> serves as a clue to the proof of <math>\operatorname{P}'\text{s}</math> type proposition as a theorem of the intuitionistic propositional calculus, that is, using only the following two combinator axioms:

Note that the explication of P as a term K((SK)S) of

 

type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof

of P's type proposition as a theorem of intuitionistic

propositional calculus, based on the combinator axioms,

K : A => (B=>A) and S : (A=>(B=>C)) => ((A=>B)=>(A=>C)).

\operatorname{K} : A \Rightarrow (B \Rightarrow A)

</pre>

\operatorname{S} : (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))

\end{array}</math>

===Step 3 (Optional)===

===Step 3 (Optional)===