Editing Combinatory logic (section)

=== Logic ===
The [[Curry–Howard isomorphism]] implies a connection between logic and programming: every proof of a theorem of [[intuitionistic logic]] corresponds to a reduction of a typed lambda term, and conversely. Moreover, theorems can be identified with function type signatures. Specifically, a typed combinatory logic corresponds to a [[Hilbert-style deduction system|Hilbert system]] in [[proof theory]].

The '''K''' and '''S''' combinators correspond to the axioms
:'''AK''': ''A'' → (''B'' → ''A''),
:'''AS''': (''A'' → (''B'' → ''C'')) → ((''A'' → ''B'') → (''A'' → ''C'')),
and function application corresponds to the detachment (modus ponens) rule
:'''MP''': from ''A'' and ''A'' → ''B'' infer ''B''.
The calculus consisting of '''AK''', '''AS''', and '''MP''' is complete for the implicational fragment of the intuitionistic logic, which can be seen as follows. Consider the set ''W'' of all deductively closed sets of formulas, ordered by [[inclusion (set theory)|inclusion]]. Then <math>\langle W,\subseteq\rangle</math> is an intuitionistic [[Kripke semantics|Kripke frame]], and we define a model <math>\Vdash</math> in this frame by
:<math>X\Vdash A\iff A\in X.</math>
This definition obeys the conditions on satisfaction of →: on one hand, if <math>X\Vdash A\to B</math>, and <math>Y\in W</math> is such that <math>Y\supseteq X</math> and <math>Y\Vdash A</math>, then <math>Y\Vdash B</math> by modus ponens. On the other hand, if <math>X\not\Vdash A\to B</math>, then <math>X,A\not\vdash B</math> by the [[deduction theorem]], thus the deductive closure of <math>X\cup\{A\}</math> is an element <math>Y\in W</math> such that <math>Y\supseteq X</math>, <math>Y\Vdash A</math>, and <math>Y\not\Vdash B</math>.

Let ''A'' be any formula which is not provable in the calculus. Then ''A'' does not belong to the deductive closure ''X'' of the empty set, thus <math>X\not\Vdash A</math>, and ''A'' is not intuitionistically valid.