Application Center - Maplesoft

App Preview:

Polynomizing Lukasiewicz's Many-Valued Logics by Maple

You can switch back to the summary page by clicking here.

Learn about Maple
Download Application




``

 

 

 

 

 

Polynomizing Lukasiewicz's Many-Valued Logics by Maple

 

Kahtan H. Alzubaidy

 

 

 

 

Introduction

 Polynomizing of Lukasiewicz's Many-Valued Logics  L[n], n = 2, 3, `and`(() .. is*the*expression*of*propositions, `in`(connectives, L[n]))

 by certain reduced polynomials of several variables over the ring " `ℤ`[n]."
" The reduction of the polynomials involved is done by using Groebner's bases to make checking of tautologies possible."

 This method is applicable when  n is a prime or a power of a prime. We shall restrict ourselves to n = 2, 3, 4 only.

 

Numerical representations

Propositional Lukasiewicz's many valued logics can be introduced by the matrix  "L[n]=< {0,1,...,n-1},&sim;,->, or , and ,&harr;,{n-1}> ; n=2,3,... . "

Suppose that  n is a prime.Then  connectives are expressed by the numeric functions.

negation(ne)      wx = n-1- x

implication(im)   x"->y=min(n-1,n-1-x+y)"

disjunction(di)    x" or y=max(x,y)"

conjunction(co)  x" and y=min(x,y)"

biconditional(bi) x"&harr;y=n-1-|x-y|"

 

"We consider L[2] , L[3] and L[4] only. The connectives are given by the following numerical functions as follows"

For L[2]

 

restart

ne2 := proc (x) options operator, arrow; 1-x end proc

proc (x) options operator, arrow; 1-x end proc

(1)

im2 := proc (x, y) options operator, arrow; min(1, 1-x+y) end proc

proc (x, y) options operator, arrow; min(1, 1-x+y) end proc

(2)

di2 := proc (x, y) options operator, arrow; max(x, y) end proc

proc (x, y) options operator, arrow; max(x, y) end proc

(3)

co2 := proc (x, y) options operator, arrow; min(x, y) end proc

proc (x, y) options operator, arrow; min(x, y) end proc

(4)

bi2 := proc (x, y) options operator, arrow; 1-abs(x-y) end proc

proc (x, y) options operator, arrow; 1-abs(x-y) end proc

(5)

 For  L[3]

 

ne3 := proc (x) options operator, arrow; 2-x end proc

proc (x) options operator, arrow; 2-x end proc

(6)

im3 := proc (x, y) options operator, arrow; min(2, 2-x+y) end proc

proc (x, y) options operator, arrow; min(2, 2-x+y) end proc

(7)

di3 := proc (x, y) options operator, arrow; max(x, y) end proc

proc (x, y) options operator, arrow; max(x, y) end proc

(8)

co3 := proc (x, y) options operator, arrow; min(x, y) end proc

proc (x, y) options operator, arrow; min(x, y) end proc

(9)

bi3 := proc (x, y) options operator, arrow; 2-abs(x-y) end proc

proc (x, y) options operator, arrow; 2-abs(x-y) end proc

(10)

NULL

 Representations by polynomials

  Let n be a prime.

 
"R[n]=`&Zopf;`[n][x[1],x[2],..,x[n]:   (x[i])^(n)=x[i]] is a polynomial ring in x[1],x[2],..,x[n]  over a field  `&Zopf;`[n] subject to the relations  (x[i])^(n)=x[i ] ."

 Any polynomial  p in
"R[n] has the reduced form  p(x[1],x[2],..,x[n])=(&sum;)a(x[1])^(i[1])...(x[n])^(i[n])      ; a in {0,...,n-1} ."

 

Special cases

In R[2]

p(x)=ax+b

p(x,y)=axy+bx+cy+d

 

In R[3]

p(x)=ax^2+bx+c

p(x,y)=ab*x^2*y+x^2*y^2+cx*y^2+d*x^2+f*y^2+exy+gx+hy+k

 

Atomic proposition in
"L[n] is represented by a variable  x in { x[1],x[2],..,x[n]}. The connectives are given as follows "

In L[2]

the unary onnective " &sim;"x= ax+b ;  a,b" in `&Zopf;`[2]"

the binary connectives
"->, or , and ,&harr; are given by by  axy+bx+cy ;  a,b,c in `&Zopf;`[2] In L[3]"

the unary onnective " &sim;"x= ax^2+bx+c ;  a,b",c in `&Zopf;`[3]"

the binary connectives  "->, or , and ,&harr; are given by by   "ab*x^2*y+x^2*y^2+cx*y^2+d*x^2+f*y^2+exy+gx+hy+k ;  "a,b,c,d,e,f,g,h,k in `&Zopf;`[3] ."

 

To find now the connectives

 

NULL

with(SolveTools)

p2 := proc (x, y) options operator, arrow; a*x*y+b*x+c*y+d end proc

proc (x, y) options operator, arrow; a*x*y+b*x+c*y+d end proc

(11)

conn2:=proc(ff)

local DS2,Eq2;

DS2 := [seq(seq([i, j], i = 0 .. 1), j = 0 .. 1)];

Eq2 := [seq(p2(u[])-ff(u[]), `in`(u, DS2))];

modp(Linear(Eq2, [a, b, c, d]),2);

end proc;

proc (ff) local DS2, Eq2; DS2 := [seq(seq([i, j], i = 0 .. 1), j = 0 .. 1)]; Eq2 := [seq(p2(u[])-ff(u[]), `in`(u, DS2))]; modp(SolveTools:-Linear(Eq2, [a, b, c, d]), 2) end proc

(12)

conn2(im2)

{a = 1, b = 1, c = 0, d = 1}

(13)

conn2(di2)

{a = 1, b = 1, c = 1, d = 0}

(14)

conn2(co2)

{a = 1, b = 0, c = 0, d = 0}

(15)

conn2(bi2)

{a = 0, b = 1, c = 1, d = 1}

(16)

Thus the connectives in `in`(L[2], terms*of*polynomials*are*as*follows)

wx = 1+xNULL

 x"->y= xy+x+1"

 x" or y=xy+x+y"

 x" and y=xy"

 x"&harr;y=x+y+1"

In terms of polynomial functions

 

pne2 := proc (x) options operator, arrow; 1+x end proc

proc (x) options operator, arrow; 1+x end proc

(17)

pim2 := proc (x, y) options operator, arrow; x*y+x+1 end proc

proc (x, y) options operator, arrow; x*y+x+1 end proc

(18)

pdi2 := proc (x, y) options operator, arrow; x*y+x+y end proc

proc (x, y) options operator, arrow; x*y+x+y end proc

(19)

pco2 := proc (x, y) options operator, arrow; x*y end proc

proc (x, y) options operator, arrow; x*y end proc

(20)

pbi2 := proc (x, y) options operator, arrow; x+y+1 end proc

proc (x, y) options operator, arrow; x+y+1 end proc

(21)

NULL

p3 := proc (x, y) options operator, arrow; a*x^2*y^2+b*x^2*y+c*x*y^2+d*x^2+e*x*y+f*y^2+g*x+h*y+k end proc

proc (x, y) options operator, arrow; a*x^2*y^2+b*x^2*y+c*x*y^2+d*x^2+e*x*y+f*y^2+g*x+h*y+k end proc

(22)

conn3:=proc(ff)

local DS3,Eq3;

DS3 := [seq(seq([i, j], i = 0 .. 2), j = 0 .. 2)];

Eq3:= [seq(p3(u[])-ff(u[]), `in`(u, DS3))];

`mod`(Linear(Eq3, [a, b, c, d,e,f,g,h,k]), 3);

end proc;

proc (ff) local DS3, Eq3; DS3 := [seq(seq([i, j], i = 0 .. 2), j = 0 .. 2)]; Eq3 := [seq(p3(u[])-ff(u[]), `in`(u, DS3))]; `mod`(SolveTools:-Linear(Eq3, [a, b, c, d, e, f, g, h, k]), 3) end proc

(23)

NULL

conn3(im3)

{a = 2, b = 2, c = 2, d = 0, e = 1, f = 0, g = 2, h = 0, k = 2}

(24)

conn3(di3)

{a = 1, b = 1, c = 1, d = 0, e = 2, f = 0, g = 1, h = 1, k = 0}

(25)

conn3(co3)

{a = 2, b = 2, c = 2, d = 0, e = 1, f = 0, g = 0, h = 0, k = 0}

(26)

conn3(bi3)

{a = 1, b = 1, c = 1, d = 0, e = 2, f = 0, g = 2, h = 2, k = 2}

(27)

NULL

Therefore the connectives in "L[3] in terms of polynomials are given by "

 wx = 2-x

 x"->y=2 x^(2)y^(2)+2 x^(2)y+2 xy^(2)+xy+2 x+2"

 x" or y=x^(2)y^(2)+x^(2)y+xy^(2)+2 xy+x+y"

 x" and y=2 x^(2)y^(2)+2 x^(2)y+2 xy^(2)+xy"

 x"&harr;y=x^(2)y^(2)+x^(2)y+xy^(2)+2 xy+2 x+2 y+2"

 

In terms of polynomial functions

 

pne3 := proc (x) options operator, arrow; 2-x end proc

proc (x) options operator, arrow; 2-x end proc

(28)

pim3 := proc (x, y) options operator, arrow; 2*x^2*y^2+2*x^2*y+2*x*y^2+x*y+2*x+2 end proc

proc (x, y) options operator, arrow; 2*x^2*y^2+2*x^2*y+2*x*y^2+x*y+2*x+2 end proc

(29)

pdi3 := proc (x, y) options operator, arrow; x^2*y^2+x^2*y+x*y^2+2*x*y+x+y end proc

proc (x, y) options operator, arrow; x^2*y^2+x^2*y+x*y^2+2*x*y+x+y end proc

(30)

pco3 := proc (x, y) options operator, arrow; 2*x^2*y^2+2*x^2*y+2*x*y^2+x*y end proc

proc (x, y) options operator, arrow; 2*x^2*y^2+2*x^2*y+2*x*y^2+x*y end proc

(31)

pbi3 := proc (x, y) options operator, arrow; x^2*y^2+x^2*y+x*y^2+2*x*y+2*x+2*y+2 end proc

proc (x, y) options operator, arrow; x^2*y^2+x^2*y+x*y^2+2*x*y+2*x+2*y+2 end proc

(32)

 Checking tautologies

 The following procedure based on Groebner basis can compute compound proposition as a reduced polynomial  in  "R[n]  for n=2,3 ."

 The proposition is a tautolog if the result is  1 for "L[2] and  2  for  L[3]."

 

 In the following procedure  ev (evaluate).

  p = 2, 3 primes

  V is the list of variables x,y,z,...

  q is the proposition as a polynomial in x, y, z, ...

 

with(Groebner)

 

ev:=proc(p,V,q)

local n,W,K,B;

n:=nops(V);

W:=[seq(V[i],i=1..n)];

 

K:=[seq(x^p-x,x in W)];

 

B:=Basis(K,tdeg(seq(V[i],i=1..n)));

modp(NormalForm(q,B,tdeg(seq(V[i],i=1..n))),p);

 

end proc;

proc (p, V, q) local n, W, K, B; n := nops(V); W := [seq(V[i], i = 1 .. n)]; K := [seq(x^p-x, `in`(x, W))]; B := Groebner:-Basis(K, tdeg(seq(V[i], i = 1 .. n))); modp(Groebner:-NormalForm(q, B, tdeg(seq(V[i], i = 1 .. n))), p) end proc

(33)

NULL

 L[2]*axioms

1) x→(y→x)

2) (x→(y→z)→((x→y)→(x→z))

3) (wx→wy)→(y→x)

 

To verify the second axiom for example. The other two axioms are similar.

q := pim2(pim2(x, pim2(y, z)), pim2(pim2(x, y), pim2(x, z)))

(x*(y*z+y+1)+x+1)*((x*y+x+1)*(x*z+x+1)+x*y+x+2)+x*(y*z+y+1)+x+2

(34)

q := modp(simplify(q), 2)

1+x+x*z+x^2*y*z^2+x^2*y*z+x^3*y^2*z^2+x^3*y*z^2+x^2*z+x^2+x^3*y+x^3*y^2

(35)

ev(2, [x, y, z], q)

1

(36)

NULL

L[3]*axioms

1) x→(y→x)

2) (x→y)→((y→z)→(x→z))

3) (wx→wy)→(y→x)

4) ((x→wx )→x)→x

 

To verify the  fourth axiom. The rest are similar.

 

qq := modp(simplify(pim3(pim3(pim3(x, pne3(x)), x), x)), 3)

2+2*x+x^2+2*x^3+x^11+2*x^14+2*x^15+x^16+2*x^17+x^18+x^21+2*x^22+x^6+2*x^9+x^10

(37)

ev(3, [x], qq)

2

(38)

``

alias(t = RootOf(Z^2+Z+1))

t

(39)

  4-valued Logic  L[4]

The truth values of  propositional Lukasiewicz's 4- valued logic  
"L[4]={0,1/(3),2/(3),1} can be represented by the elements of  Galois field  GF(4)."

GF(4)=
"(`&Zopf;`[2][t])/(<t^(2)+t+1>).    GF(4)={0,1,t,t+1}  modulo 2,  modulo(t^(2)+t+1) . We reserve the letter  t for this purpose only."

Minimum and maximum functions on GF(4) are given by the following two proceddures.

 

m:=proc(u,v)

local r;

r:=min(u,v);

r:=eval(subs(t=2,r));

subs(2=t,3=t+1,r);

end proc;

 

proc (u, v) local r; r := min(u, v); r := eval(subs(t = 2, r)); subs(2 = t, 3 = t+1, r) end proc

(40)

M:=proc(u,v)

local r;

r:=max(u,v);

r:=eval(subs(t=2,r));

subs(2=t,3=t+1,r);

end proc;

 

proc (u, v) local r; r := max(u, v); r := eval(subs(t = 2, r)); subs(2 = t, 3 = t+1, r) end proc

(41)

m(0, 1), m(0, t), m(0, t+1), m(1, t), m(1, t+1), m(t, t+1)

0, 0, 0, 1, 1, t

(42)

M(0, 1), M(0, t), M(0, t+1), M(1, t), M(1, t+1), M(t, t+1)

1, t, t+1, t, t+1, t+1

(43)

 The order on GF(4) is therefore given by   0 < 1 < t < t+1 .

 

 The connectives are given by the following functions

 

 

ne4 := proc (u) options operator, arrow; t+1-u end proc

proc (u) options operator, arrow; t+1-u end proc

(44)

im4 := proc (u, v) options operator, arrow; m(t+1, t+1-u+v) end proc

proc (u, v) options operator, arrow; m(t+1, t+1-u+v) end proc

(45)

di4 := proc (u, v) options operator, arrow; M(u, v) end proc

proc (u, v) options operator, arrow; M(u, v) end proc

(46)

co4 := proc (u, v) options operator, arrow; m(u, v) end proc

proc (u, v) options operator, arrow; m(u, v) end proc

(47)

bi4 := proc (u, v) options operator, arrow; co4(im4(u, v), im4(v, u)) end proc

proc (u, v) options operator, arrow; co4(im4(u, v), im4(v, u)) end proc

(48)

NULL

 Consider the following lists

 

CC := [seq(a[i], i = 1 .. 16)]

[a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8], a[9], a[10], a[11], a[12], a[13], a[14], a[15], a[16]]

(49)

L4 := [0, 1, t, t+1]

[0, 1, t, t+1]

(50)

NULL

DS4 := [seq(seq([i, j], `in`(i, L4)), `in`(j, L4))]

[[0, 0], [1, 0], [t, 0], [t+1, 0], [0, 1], [1, 1], [t, 1], [t+1, 1], [0, t], [1, t], [t, t], [t+1, t], [0, t+1], [1, t+1], [t, t+1], [t+1, t+1]]

(51)

NULL

NULL

 

 The reduced polynomial when n = 4

 

p4 := proc (x, y) options operator, arrow; a[1]*x^3*y^3+a[2]*x^3*y^2+a[3]*x^2*y^3+a[4]*x^3*y+a[5]*x^2*y^2+a[6]*x*y^3+a[7]*x^3+a[8]*x^2*y+a[9]*x*y^2+a[10]*y^3+a[11]*x^2+a[12]*x*y+a[13]*y^2+a[14]*x+a[15]*y+a[16] end proc

proc (x, y) options operator, arrow; a[1]*x^3*y^3+a[2]*x^3*y^2+a[3]*x^2*y^3+a[4]*x^3*y+a[5]*x^2*y^2+a[6]*x*y^3+a[7]*x^3+a[8]*x^2*y+a[9]*x*y^2+a[10]*y^3+a[11]*x^2+a[12]*x*y+a[13]*y^2+a[14]*x+a[15]*y+a[16] end proc

(52)

"The coefficients  a[1], ... ,a[16]  in `&Zopf;`[2] ."

 

conn4:=proc(ff)

local DS4,Eq4;

DS4 := [seq(seq([i, j], `in`(i, L4)), `in`(j, L4))];

Eq4:= [seq(p4(u[])-ff(u[]), `in`(u, DS4))];

`mod`(Linear(Eq4, CC), 2);

end proc;

proc (ff) local DS4, Eq4; DS4 := [seq(seq([i, j], `in`(i, L4)), `in`(j, L4))]; Eq4 := [seq(p4(u[])-ff(u[]), `in`(u, DS4))]; `mod`(SolveTools:-Linear(Eq4, CC), 2) end proc

(53)

``

 

 The connectives

 

conn4(im4)

{a[1] = t, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = t, a[6] = t+1, a[7] = 0, a[8] = 1, a[9] = t+1, a[10] = 0, a[11] = 0, a[12] = 1, a[13] = 0, a[14] = 1, a[15] = 0, a[16] = t+1}

(54)

``

conn4(di4)

{a[1] = 0, a[2] = t+1, a[3] = t+1, a[4] = t, a[5] = 1, a[6] = t, a[7] = 0, a[8] = t, a[9] = t, a[10] = 0, a[11] = 0, a[12] = 0, a[13] = 0, a[14] = 1, a[15] = 1, a[16] = 0}

(55)

conn4(co4)

{a[1] = 0, a[2] = t+1, a[3] = t+1, a[4] = t, a[5] = 1, a[6] = t, a[7] = 0, a[8] = t, a[9] = t, a[10] = 0, a[11] = 0, a[12] = 0, a[13] = 0, a[14] = 0, a[15] = 0, a[16] = 0}

(56)

conn4(bi4)

{a[1] = 0, a[2] = 1, a[3] = 1, a[4] = t+1, a[5] = 0, a[6] = t+1, a[7] = 0, a[8] = t, a[9] = t, a[10] = 0, a[11] = 0, a[12] = 0, a[13] = 0, a[14] = 1, a[15] = 1, a[16] = t+1}

(57)

NULL

 

NULL

   Connectives in terms of  polynomials

 

"   &sim;x=t+1-x"

proc (x) options operator, arrow; y = tx^3*y^3+x^3*y^2+tx^2*y^2+(t+1)*xy^3+x^2*y+(t+1)*xy^2+xy+x+t+1 end proc

x or y = (t+1)*x^3*y^2+(t+1)*x^2*y^3+tx^3*y+x^2*y^2+txy^3+tx^2*y+txy^2+x+y

x and y = (t+1)*x^3*y^2+(t+1)*x^2*y^3+tx^3*y+x^2*y^2+txy^3+tx^2*y+txy^2

`&harr;`(x, y) and y = x^3*y^2+x^2*y^3+(t+1)*x^3*y+(t+1)*xy^3+tx^2*y+txy^2+x+y+t+1

 

NULL

"     in terms of polynomial functions"

 

pne4 := proc (x) options operator, arrow; t+1-x end proc

proc (x) options operator, arrow; t+1-x end proc

(58)

pim4 := proc (x, y) options operator, arrow; t*x^3*y^3+x^3*y^2+t*x^2*y^2+(t+1)*x*y^3+x^2*y+(t+1)*x*y^2+x*y+x+t+1 end proc

proc (x, y) options operator, arrow; t*x^3*y^3+x^3*y^2+t*x^2*y^2+(t+1)*x*y^3+x^2*y+(t+1)*x*y^2+x*y+x+t+1 end proc

(59)

pdi4 := proc (x, y) options operator, arrow; (t+1)*x^3*y^2+(t+1)*x^2*y^3+t*x^3*y+x^2*y^2+t*x*y^3+t*x^2*y+t*x*y^2+x+y end proc

proc (x, y) options operator, arrow; (t+1)*x^3*y^2+(t+1)*x^2*y^3+t*x^3*y+x^2*y^2+t*x*y^3+t*x^2*y+t*x*y^2+x+y end proc

(60)

pco4 := proc (x, y) options operator, arrow; (t+1)*x^3*y^2+(t+1)*x^2*y^3+t*x^3*y+x^2*y^2+t*x*y^3+t*x^2*y+t*x*y^2 end proc

proc (x, y) options operator, arrow; (t+1)*x^3*y^2+(t+1)*x^2*y^3+t*x^3*y+x^2*y^2+t*x*y^3+t*x^2*y+t*x*y^2 end proc

(61)

pbi4 := proc (x, y) options operator, arrow; x^3*y^2+x^2*y^3+(t+1)*x^3*y+(t+1)*x*y^3+t*x^2*y+t*x*y^2+x+y+t+1 end proc

proc (x, y) options operator, arrow; x^3*y^2+x^2*y^3+(t+1)*x^3*y+(t+1)*x*y^3+t*x^2*y+t*x*y^2+x+y+t+1 end proc

(62)

 

The following procedure evaluate compound propositions in terms of reduced polynomials  in  "L[4] . "

 p = 2 and V, q as above in ev.

 

ev4:=proc(p,V,q)

local n,W,K,B;

n:=nops(V);

W:=[seq(V[i],i=1..n)];

 

K:=[seq(x^(2*p)-x,x in W)];

 

B:=Basis(K,tdeg(seq(V[i],i=1..n)));

modp(NormalForm(q,B,tdeg(seq(V[i],i=1..n))),p);

 

end proc;

proc (p, V, q) local n, W, K, B; n := nops(V); W := [seq(V[i], i = 1 .. n)]; K := [seq(x^(2*p)-x, `in`(x, W))]; B := Groebner:-Basis(K, tdeg(seq(V[i], i = 1 .. n))); modp(Groebner:-NormalForm(q, B, tdeg(seq(V[i], i = 1 .. n))), p) end proc

(63)

NULL

 

Checking tautologies in L[4]

 The above proceduer ev4  can be used to check tautologies in  "L[4].   If the result is  t+1, then the proposition is a tautology."

 Examples

  1) x →x

 

w := pim4(x, x)

t*x^6+x^5+t*x^4+(t+1)*x^4+x^3+(t+1)*x^3+x^2+x+t+1

(64)

ev4(2, [x], w)

t+1

(65)

 2) x→(y→x)

 

ww := pim4(x, pim4(y, x))

t*x^3*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)^3+x^3*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)^2+t*x^2*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)^2+(t+1)*x*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)^3+x^2*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)+(t+1)*x*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)^2+x*(t*y^3*x^3+y^3*x^2+t*y^2*x^2+(t+1)*y*x^3+y^2*x+(t+1)*y*x^2+y*x+y+t+1)+x+t+1

(66)

ev4(2, [x, y], ww)

t+1

(67)

NULL

 3) xnwx  is not tautology in "L[4]."

 

www := pdi4(x, pne4(x))

(t+1)*x^3*(t+1-x)^2+(t+1)*x^2*(t+1-x)^3+t*x^3*(t+1-x)+x^2*(t+1-x)^2+t*x*(t+1-x)^3+t*x^2*(t+1-x)+t*x*(t+1-x)^2+t+1

(68)

ev4(2, [x], www)

t+1+t*x+(t+1)*x^2

(69)

``

 

 Remark

 We can deduce from → the other connectives  n,o,↔ .

 For example   xny = (x→y)→y

 

g := pim4(pim4(x, y), y)

t*(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)^3*y^3+(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)^3*y^2+t*(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)^2*y^2+(t+1)*(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)*y^3+(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)^2*y+(t+1)*(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)*y^2+(t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+t+1)*y+t*y^3*x^3+x^3*y^2+t*y^2*x^2+(t+1)*x*y^3+y*x^2+(t+1)*x*y^2+y*x+x+2*t+2

(70)

``

ev4(2, [x, y], g)

x+y+y^2*x^2+y*x^2*t+x^3*y*t+(t+1)*x^3*y^2+y^3*x*t+(t+1)*y^3*x^2+y^2*x*t

(71)

sort(%)

(t+1)*x^3*y^2+(t+1)*x^2*y^3+t*x^3*y+x^2*y^2+t*x*y^3+t*x^2*y+t*x*y^2+x+y

(72)

t := 't'

t

(73)

NULL

 References

1) M. Bergmann

    Many-Valued and Fuzzy Logic

    Cambridge 2008.

2) Walter Carnielli

    Polynomial Ring Calculus for Many-Valued Logics

    Proceedings of the 35th International Symposium on Multiple-Valued Logic (ISMVL’05)