4-valued Counter Example (Was: An Affine Logic Example: Łukasiewicz Logic)

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.