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)

    We should always remember that the work of art is invariably the creation of a new world, so that the first thing we should do is to study that new world as closely as possible, approaching it as something brand new, having no obvious connection with the worlds we already know. When this new world has been closely studied, then and only then let us examine its links with other worlds, other branches of knowledge.
    Vladimir Nabokov (1899–1977)

    The American Constitution, one of the few modern political documents drawn up by men who were forced by the sternest circumstances to think out what they really had to face instead of chopping logic in a university classroom.
    George Bernard Shaw (1856–1950)