1. Forum
  2. Usenet
  3. SCI.LOGIC

  • =?UTF-8?Q?An_Affine_Logic_Example:_=c5=81ukasiewicz_Logic?=

    From Mild Shock@21:1/5 to All on Sat Dec 21 23:20:40 2024
    Hi,

    An example of an affine Logic, is this 3-valued
    Logic with the following implication truth table:

    F U T
    F T T T
    U U T T
    T F U T

    It satisfies modus ponens:

    /* Implication Elimination */
    ?- tauto((X & (X->Y) => Y)).
    true.

    It satisfies the types of combinators BCK:

    /* K Combinator */
    ?- tauto((X -> Y -> X)).
    true.

    /* B Combinator */
    ?- tauto(((Y -> Z) -> ((X -> Y) -> (X -> Z)))).
    true.

    /* C Combinator */
    ?- tauto(((X -> (Y -> Z)) -> (Y -> (X -> Z)))).
    true.

    And surprise surprise, it doesn't satisfy contraction,
    the formula that Julio doubted that it is unprovable:

    ?- tauto(((X -> (X -> Y)) -> (X -> Y))).
    false.

    Bye

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)