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 to, connection and/or logic:

    One must always maintain one’s connection to the past and yet ceaselessly pull away from it. To remain in touch with the past requires a love of memory. To remain in touch with the past requires a constant imaginative effort.
    Gaston Bachelard (1884–1962)

    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)

    What avail all your scholarly accomplishments and learning, compared with wisdom and manhood? To omit his other behavior, see what a work this comparatively unread and unlettered man wrote within six weeks. Where is our professor of belles-lettres, or of logic and rhetoric, who can write so well?
    Henry David Thoreau (1817–1862)