1. Forum
  2. Usenet
  3. SCI.LOGIC

  • =?UTF-8?Q?4-valued_Counter_Example_=28Was:_An_Affine_Logic_Example:?= =

    From Mild Shock@21:1/5 to Ross Finlayson on Sun Dec 22 17:16:29 2024
    Hi,

    Yes you can also find a 4-valued Counter
    Example, that shows that this here is not
    derivable in Affine Logic:

    ((A -> (A -> B)) -> (A -> B))

    The above stems from the W Combinator.

    W x y = x y y

    The W combinator seems not to be available
    in Affine Combinatory Logic, cannot be
    derived from the combinator basis BCK.

    Bye

    P.S.: How did I verify the 3 valued logic?
    Well that is the Prolog code:

    https://gist.github.com/Jean-Luc-Picard-2021/390e0dddbe56a8b50a4a538b35290b83

    :- op(1000, xfy, &). % conjunction
    :- op(1110, xfy, =>). % conditional

    value('F').
    value('U').
    value('T').

    imp('F', 'F', 'T').
    imp('F', 'U', 'T').
    imp('F', 'T', 'T').
    imp('U', 'F', 'U').
    imp('U', 'U', 'T').
    imp('U', 'T', 'T').
    imp('T', 'F', 'F').
    imp('T', 'U', 'U').
    imp('T', 'T', 'T').

    eval((A->B), X) :- eval(A, H), eval(B, J), imp(H, J, X).
    eval(X, X).

    always([], (F => G)) :- forall(always([], F), always([], G)).
    always([], (F & G)) :- always([], F), always([], G).
    always([], F) :- eval(F, 'T').
    always([X|L], F) :- forall(value(X), always(L, F)).

    tauto(F) :- term_variables(F, L), always(L, F).


    Ross Finlayson schrieb:
    On 12/21/2024 02:20 PM, Mild Shock wrote:
    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


    quasi-modal

    How about instead

    B both
    N neither

    X don't care
    ? don't know

    T true
    F false

    It depends on propositions fulfilling question words,
    all of them.

    That you have "material implication"
    is not necessarily anybody else's problem.

    I.e., nobody needs "the quasi-modal", at all,
    except to make broken logics like those.



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