Editing SKI combinator calculus (section)

==Connection to intuitionistic logic==
The combinators '''K''' and '''S''' correspond to two well-known axioms of [[sentential logic]]:

:{{math|'''AK''': ''A'' &rarr; (''B'' &rarr; ''A'')}},
:{{math|'''AS''': (''A'' &rarr; (''B'' &rarr; ''C'')) &rarr; ((''A'' &rarr; ''B'') &rarr; (''A'' &rarr; ''C''))}}.

Function application corresponds to the rule [[modus ponens]]:

:{{math|'''MP'''}}: from {{mvar|A}} and {{math|''A'' &rarr; ''B''}}, infer {{mvar|B}}.

The axioms '''AK''' and '''AS''', and the rule '''MP''' are complete for the implicational fragment of [[intuitionistic logic]]. In order for combinatory logic to have as a model:
*The [[implicational propositional calculus|implicational fragment]] of [[classical logic]], would require the combinatory analog to the [[law of excluded middle]], ''i.e.'', [[Peirce's law]];
*[[sentential logic|Complete classical logic]], would require the combinatory analog to the sentential axiom {{math|'''F''' &rarr; ''A''}}.

This connection between the types of combinators and the corresponding logical axioms is an instance of the [[Curry–Howard isomorphism]].