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:

    The smallest fact about the connection between character and hormonal balance offers more insight into the soul than a five-story idealistic system [of philosophy] does.
    Robert Musil (1880–1942)

    There is no morality by instinct.... There is no social salvation—in the end—without taking thought; without mastery of logic and application of logic to human experience.
    Katharine Fullerton Gerould (1879–1944)