Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: =?UTF-8?Q?4-valued_Counter_Example_=28Was:_An_Affine_Logic_Example:?=
 =?UTF-8?Q?_=c5=81ukasiewicz_Logic=29?=
Date: Sun, 22 Dec 2024 17:16:29 +0100
Message-ID: <vk9e0s$17frs$1@solani.org>
References: <vk7evo$1jjc4$1@solani.org>
 <cO-dndcWdYBGGvr6nZ2dnZfqn_idnZ2d@giganews.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 22 Dec 2024 16:16:28 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1294204"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:n++76xBRggj8qCN9ZWSeaz1bFLk=
In-Reply-To: <cO-dndcWdYBGGvr6nZ2dnZfqn_idnZ2d@giganews.com>
X-User-ID: eJwFwQkBwDAIA0BLGU8KcgoF/xJ258qPfYxO8/X9RkdxipHXcp4dymNIbpO4Gy2raKsMrLyURtHCBAW9Uz9FexU0
Bytes: 3585
Lines: 115

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.
> 
>