Newsportal USENET - An Affine Logic Example: Łukasiewicz Logic

Sujet : An Affine Logic Example: Łukasiewicz Logic
De : janburse (at) *nospam* fastmail.fm (Mild Shock)
Groupes : sci.logic
Date : 21. Dec 2024, 23:20:40

Autres entêtes

Message-ID : <vk7evo$1jjc4$1@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

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

Date	Sujet	#	Auteur
21 Dec 24	An Affine Logic Example: Łukasiewicz Logic	3	Mild Shock
22 Dec 24	Re: An Affine Logic Example: Łukasiewicz Logic	2	Ross Finlayson
22 Dec 24	4-valued Counter Example (Was: An Affine Logic Example: Łukasiewicz Logic)	1	Mild Shock