SKI Combinator Calculus - Connection To Intuitionistic Logic

Connection To Intuitionistic Logic

The combinators K and S correspond to two well-known axioms of sentential logic:

AK: A (B A),
AS: (A (B C)) ((A B) (A C)).

Function application corresponds to the rule modus ponens:

MP: from A and A B, infer 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 fragment of classical logic, would require the combinatory analog to the law of excluded middle, e.g., Peirce's law;
  • Complete classical logic, would require the combinatory analog to the sentential axiom F A.

Read more about this topic:  SKI Combinator Calculus

Famous quotes containing the words connection and/or logic:

    Children of the same family, the same blood, with the same first associations and habits, have some means of enjoyment in their power, which no subsequent connections can supply; and it must be by a long and unnatural estrangement, by a divorce which no subsequent connection can justify, if such precious remains of the earliest attachments are ever entirely outlived.
    Jane Austen (1775–1817)

    Our argument ... will result, not upon logic by itself—though without logic we should never have got to this point—but upon the fortunate contingent fact that people who would take this logically possible view, after they had really imagined themselves in the other man’s position, are extremely rare.
    Richard M. Hare (b. 1919)