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)