Lukasiewicz's Three-Valued Modal Logic

individuals={iA,iB,iC,iD,iE,iF,iG,iH,iI,iJ,iK,iL};
dvomestneIzjavne={and,or,impl,eqq};
dvomestneIzjavneS={" ∧ "," ∨ "," \[Implies] "," ⇔ "};
individualconstants=CharacterRange["A","L"];
enomestni={small,medium,large,triangle,square,pentagon,white,gray};
enomestnioznS={"majhen","srednje velikosti","velik","trikotnik","kvadrat","petkotnik","bel","siv"};
enomestnioznASim={"Small","Medium","Large","Triangle","Square","Pentagon","White","Gray"};
enomestnioznA={"small","medium","large","triangle","square","pentagon","white","gray"};
enomestnioznArS={"majhen lik","lik srednje velikosti","velik lik","trikotnik","kvadrat","petkotnik","bel lik","siv lik"};
enomestnioznSSim={"Majhen","Srednje","Velik","Trikotnik","Kvadrat","Petkotnik","Bel","Siv"};
enomestnioznArA={"small figure","medium figure","large figure","triangle","square","pentagon","white figure","gray figure"};
SetAttributes[And3,{Flat,OneIdentity}];
SetAttributes[Or3,{Flat,OneIdentity}];
And3[p_,q_]:=Min[p,q];
Or3[p_,q_]:=Max[p,q];
Im3[p_,q_]:=If[p≤q,1,1-p+q];
Eq3[p_,q_]:=If[p==q,1,If[(p==0 && q==1)||(p==1&&q==0),0,1/2]];

Not3[p_]:=1-p;
Nuj3[p_]:=If[p==1,1,0];
Mog3[p_]:=If[p==0,0,1];
NiNuj3[p_]:=If[p==1,0,1];
NiMog3[p_]:=If[p==0,1,0];
satisfies[nuj[x_],structure_]:=Nuj3[satisfies[x,structure]]
satisfies[ninuj[x_],structure_]:=NiNuj3[satisfies[x,structure]]
satisfies[nimog[x_],structure_]:=NiMog3[satisfies[x,structure]]
satisfies[mog[x_],structure_]:=Mog3[satisfies[x,structure]]
ClosedLine[a_]:=Line[Append[a,First[a]]];
satisfies[and[x_,y_],structure_]:=And3[satisfies[x,structure],satisfies[y,structure]];
satisfies[and[x_,y_,z_],structure_]:=And3[And3[satisfies[x,structure],satisfies[y,structure]],satisfies[z,structure]];
satisfies[or[x_,y_],structure_]:=Or3[satisfies[x,structure],satisfies[y,structure]];
satisfies[eq[x_,y_],structure_]:=Eq3[satisfies[x,structure],satisfies[y,structure]];
satisfies[eqq[x_,y_],structure_]:=Eq3[satisfies[x,structure],satisfies[y,structure]];

satisfies[impl[x_,y_],structure_]:=Im3[satisfies[x,structure],satisfies[y,structure]];
satisfies[not[x_],structure_]:=Not3[satisfies[x,structure]];
satisfies[!x_,structure_]:=Not3[satisfies[x,structure]];
satisfies[id[x_],structure_]:=satisfies[x,structure];

satisfies[large[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[2]]==3,1,0],
If[x[[2]]==3,1,0,0.5]];
(*satisfies[large[x_],structure_]:=If[x[[2]]==3,1,0,0.5];*)
satisfies[medium[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[2]]==2,1,0],
If[x[[2]]==2,1,0]]
satisfies[small[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[2]]==1,1,0],
If[x[[2]]==1,1,0]];
satisfies[triangle[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[1]]==1,1,If[structure[[First[First[Position[individuals,x]]]]][[1]]==20,0.5,0]],
If[x[[1]]==1 ,1, If[x[[1]]==20,0.5,0]]];
satisfies[square[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[1]]==2,1,If[structure[[First[First[Position[individuals,x]]]]][[1]]==20,0.5,0]],
If[x[[1]]==2 ,1, If[x[[1]]==20,0.5,0]]];
satisfies[pentagon[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[1]]==3,1,If[structure[[First[First[Position[individuals,x]]]]][[1]]==20,0.5,0]],
If[x[[1]]==3,1, If[x[[1]]==20,0.5,0]]];
satisfies[white[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[4]]==1,1,0],
If[x[[4]]==1,1,0]];
satisfies[gray[x_],structure_]:=If[MemberQ[individuals,x],If[structure[[First[First[Position[individuals,x]]]]][[4]]==0,1,0],
If[x[[4]]==0,1,0]];

satisfies[eq[x_,y_],structure_]:=If[MemberQ[individuals,x]&&MemberQ[individuals,y],If[structure[[First[First[Position[individuals,x]]]]]==structure[[First[First[Position[individuals,y]]]]],1,0,0.5]
If[x[[3]]==y[[3]],1,0,0.5]];
satisfies[rightof[x_,y_],structure_]:=If[MemberQ[individuals,x]&&MemberQ[individuals,y],If[structure[[First[First[Position[individuals,x]]]]][[3,1]]>structure[[First[First[Position[individuals,y]]]]][[3,1]],1,0,0.5],
If[x[[3,1]]>y[[3,1]],1,0]];
satisfies[above[x_,y_],structure_]:=If[MemberQ[individuals,x]&&MemberQ[individuals,y],If[structure[[First[First[Position[individuals,x]]]]][[3,2]]>structure[[First[First[Position[individuals,y]]]]][[3,2]],1,0,0.5],
If[x[[3,2]]>y[[3,2]],1,0]];
satisfies[bellow[x_,y_],structure_]:=If[MemberQ[individuals,x]&&MemberQ[individuals,y],If[structure[[First[First[Position[individuals,x]]]]][[3,2]]<structure[[First[First[Position[individuals,y]]]]][[3,2]],1,0,0.5],
If[x[[3,2]]<y[[3,2]],1,0]];
satisfies[eq[x_,y_],structure_]:=If[MemberQ[individuals,x]&&MemberQ[individuals,y],If[structure[[First[First[Position[individuals,x]]]]]==structure[[First[First[Position[individuals,y]]]]],1,0,0.5],
If[x[[3]]==y[[3]],1,0,0.5]];
satisfies[diff[x_,y_],structure_]:=If[MemberQ[individuals,x]&&MemberQ[individuals,y],If[structure[[First[First[Position[individuals,x]]]]]=!=structure[[First[First[Position[individuals,y]]]]],1,0,0.5],
If[x[[3]]=!=y[[3]],1,0,0.5]];
tobesatisfiedin[structure_][formula_]:=satisfies[formula,structure];
chessboard=Union[Table[Line[{{i,0},{i,8}}],{i,0,8}],Table[Line[{{0,i},{8,i}}],{i,0,8}]];

chess[m_,n_]:={Union[Table[Line[{{i,0},{i,m}}],{i,0,n}],Table[Line[{{0,i},{n,i}}],{i,0,m}]],Table[Text[ToString[i],{i+0.5,m-0.5}],{i,1,n-1}],Table[Text[ToString[i],{0.5,m-0.5-i}],{i,1,m-1}]};
lik[{tip_,vel_,r_,bar_},{i_}]:={{GrayLevel[If[bar≠1,0.7,bar]],Polygon[Table[r+{0.5,0.5}+(1/5+vel/4){Sin[2 Pi n/(tip+2)],Cos[2 Pi n/(tip+2)]},{n,tip+2}]]},{GrayLevel[0],Text[individualconstants[[i]],r+{0.5,0.5}-vel/3{0,0}]}};
lik2[{tip_,vel_,r_,bar_}]:={{GrayLevel[0.],ClosedLine[Table[r+{0.5,0.5}+(1/5+vel/4){Sin[2 Pi n/(tip+2)],Cos[2 Pi n/(tip+2)]},{n,tip+2}]]}};
generatTarski[i_]:=Module[{free=Flatten[Table[{m,n},{m,0,7},{n,0,7}],1],structure={},zaodst,zasedeni={}},Do[nova=free[[RandomInteger[{1,Length[free]}]]];sosede={{nova[[1]]+1,nova[[2]]+1},{nova[[1]]+1,nova[[2]]},{nova[[1]]+1,nova[[2]]-1},{nova[[1]],nova[[2]]+1},{nova[[1]],nova[[2]]-1},{nova[[1]]-1,nova[[2]]+1},{nova[[1]]-1,nova[[2]]},{nova[[1]]-1,nova[[2]]-1}};nov={{1,2,3,20,20,20}[[RandomInteger[{1,6}]]],RandomInteger[{1,3}],nova,RandomInteger[]};If[nov[[2]]==3&&zasedeni⋂sosede≠{},nov=ReplacePart[nov,RandomInteger[{1,2}],2]];structure=Append[structure,nov];zaodst=If[nov[[2]]==3,{nov[[3]],{nov[[3]][[1]]+1,nov[[3]][[2]]+1},{nov[[3]][[1]]+1,nov[[3]][[2]]+1},{nov[[3]][[1]]+1,nov[[3]][[2]]},{nov[[3]][[1]]+1,nov[[3]][[2]]-1},{nov[[3]][[1]],nov[[3]][[2]]+1},{nov[[3]][[1]],nov[[3]][[2]]-1},{nov[[3]][[1]]-1,nov[[3]][[2]]+1},{nov[[3]][[1]]-1,nov[[3]][[2]]},{nov[[3]][[1]]-1,nov[[3]][[2]]-1}},{nov[[3]]}];free=Complement[free,zaodst];zasedeni=zasedeni⋃{nova},{j,1,i}];structure];
prikazsveta[svet_]:=Module[{sv1,sv2},sv1=MapIndexed[lik,svet];sv2=Map[lik2,svet];Show[Graphics[{chessboard,sv1,sv2}],AspectRatio->Automatic,TextStyle->{FontSize->14},PlotRange->{{-.5,8.5},{-.5,8.5}}]];

randomatomicNov[k_]:=Module[{ren=Random[Integer,{1,Length[enomestni]}],rin=Random[Integer,{1,k}]},{enomestni[[ren]][individuals[[rin]]],{"lik ",individualconstants[[rin]]," je ",enomestnioznS[[ren]]},{"figure ",individualconstants[[rin]]," is ",enomestnioznA[[ren]]},StringJoin[enomestnioznSSim[[ren]]," (",individualconstants[[rin]],")"],StringJoin[enomestnioznASim[[ren]]," (",individualconstants[[rin]],")"]}];

randomliterNov[k_]:=If[Random[Integer]==0,randomatomicNov[k],Block[{ren=Random[Integer,{1,Length[enomestni]}],rin=Random[Integer,{1,k}]},{not[enomestni[[ren]][individuals[[rin]]]],{"lik ",individualconstants[[rin]]," ni ",enomestnioznS[[ren]]},{"figure ",individualconstants[[rin]]," is not ",enomestnioznA[[ren]]},StringJoin["¬ ",enomestnioznSSim[[ren]]," (",individualconstants[[rin]],")"],StringJoin["¬ ",enomestnioznASim[[ren]]," (",individualconstants[[rin]],")"]}]];
randommolsentNov[k_]:=Block[{dvo=Random[Integer,{1,Length[dvomestneIzjavne]}],li1=randomliterNov[k],li2=randomliterNov[k]},{dvomestneIzjavne[[dvo]][li1[[1]],li2[[1]]],If[dvo==1,{li1[[2]]," in ", li2[[2]]},If[dvo==2,{li1[[2]]," ali ",If[li2[[2]][[3]]==" je ",Insert[li2[[2]][[{3,1,2,4}]]," ",4],li2[[2]]]},If[dvo==3,{"če ",If[li1[[2]][[3]]==" je ",Insert[li1[[2]][[{3,1,2,4}]]," ",4],li1[[2]]],", potem ",If[li2[[2]][[3]]==" je ",Insert[li2[[2]][[{3,1,2,4}]]," ",4],li2[[2]]]},{li1[[2]],", če in  samo če ",If[li2[[2]][[3]]==" je ",Insert[li2[[2]][[{3,1,2,4}]]," ",4],li2[[2]]]}]]],If[dvo==1,{li1[[3]]," and ", li2[[3]]},If[dvo==2,{li1[[3]]," or ",li2[[3]]},If[dvo==3,{"if ",li1[[3]]," then ", li2[[3]]},{li1[[3]],", if and only if ",li2[[3]]}]]],StringJoin[li1[[4]]," ",dvomestneIzjavneS[[dvo]]," ",li2[[4]]],StringJoin[li1[[5]]," ",dvomestneIzjavneS[[dvo]]," ",li2[[5]]]}];

Neg[sen_]:=Module[{},{!sen[[1]],{"ni res, da: ",sen[[2]]},{"it is not true: ",sen[[3]]},StringJoin["¬ (",sen[[4]],")"],StringJoin["¬ (",sen[[5]],")"]}];
Nujno[sen_]:=Module[{},{nuj[sen[[1]]],{"nujno je: ",sen[[2]]},{"necessary that: ",sen[[3]]},StringJoin["□(",sen[[4]],")"],StringJoin["□ (",sen[[5]],")"]}];
Mozno[sen_]:=Module[{},{mog[sen[[1]]],{"možno je: ",sen[[2]]},{"possible that: ",sen[[3]]},StringJoin["◇(",sen[[4]],")"],StringJoin["◇ (",sen[[5]],")"]}];
NiNujno[sen_]:=Module[{},{ninuj[sen[[1]]],{"ni nujno, da: ",sen[[2]]},{"It is not nesessary: ",sen[[3]]},StringJoin["¬□(",sen[[4]],")"],StringJoin["¬ □ (",sen[[5]],")"]}];
NiMozno[sen_]:=Module[{},{nimog[sen[[1]]],{"ni možno, da: ",sen[[2]]},{"it is not possible that: ",sen[[3]]},StringJoin["¬◇(",sen[[4]],")"],StringJoin["¬ ◇ (",sen[[5]],")"]}];
dvo4[p_,q_]:={{And3[p,q],{p, " in ",q},{"res je, da ",p, " in res je, da  ",q},{p," and ",q},{"both ",p," and ",q},{p," ∧ ",q}},{Or3[p,q], {p, " ali ", q}, {"res je, da ",p, " ali je res, da ", q},{p," or ",q," (or both)"},{"either ",p," or ",q," or both"},{p," ∨ ",q}},
{Im3[p,q],{"če ",p,", potem ",q},{"če ",p,", potem ",q},{"if ",p," then ",q},{"if ",p," then ",q},{p," ⇒ ",q}},{Eq3[p,q],{p," natanko tedaj, kadar ",q},{p,", če in samo če je res, da ",q},{ p," if and only if ",q},{ p," if and only if ",q},{p," ⇔ ",q}}
};
tabl={Join[{"1","1"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->1,q->1}],Join[{"1","0"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->1,q->0}],Join[{"1","1/2"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->1,q->1/2}],Join[{"0","1"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->0,q->1}],Join[{"0","0"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->0,q->0}],Join[{"0","1/2"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->0,q->1/2}],Join[{"1/2","1"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->1/2,q->1}],Join[{"1/2","0"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->1/2,q->0}],Join[{"1/2","1/2"},Table[dvo4[p,q][[i,1]],{i,1,4}]/.{p->1/2,q->1/2}]}(*/.{1->"T",0->"F",1/2->"U",0.5->"U"}*);
trtable=Join[{Join[{"p","q"},Map[StringJoin,Table[dvo4["p","q"][[i,6]],{i,1,4}]]]},tabl];
tabenomestne={{"p","¬ p","□ p","◇ p"},{1,0,1,1},{0,1,0,0},{1/2,1/2,0,1}};
world1={{3,1,{1,1},0},{3,2,{1,3},0},{3,3,{1,5},0},{2,1,{3,1},0},{2,2,{3,3},0},{2,3,{3,5},0},{1,1,{5,1},0},{1,2,{5,3},0},{1,3,{5,5},0},{20,1,{7,1},0},{20,2,{7,3},0},{20,3,{7,5},0}};
pret[x_]:=Switch[x,1,"T",0,"F",0.5,"U"];
pret2[x_]:=Switch[x,1,"1",0,"0",0.5,"1/2"];pret3[x_]:=Switch[x,"T","1","F","0","U","1/2"];

Manipulate[
If[try,ranint=RandomInteger[{1,1000}];try=False];
With[{ran=SeedRandom[ranint],svet=generatTarski[k],stavki=Join[Table[{Mozno,Nujno,NiMozno,NiNujno}[[RandomInteger[{1,4}]]][randomliterNov[k]],{k1}],Table[{Mozno,Nujno,NiMozno,NiNujno}[[RandomInteger[{1,4}]]][randommolsentNov[k]],{k2}]]},With[{seznam=stavki[[All,1]]},With[{gr1=Column[Table[Style[StringJoin[ToString[i],". ",Apply[StringJoin,stavki[[All,If[lan==="Slovenian",4,5]]],{1}][[i]]
],12],{i,1,Length[seznam]}]],tv=Map[tobesatisfiedin[svet],seznam]},If[help2,Pane[Row[{Text@Grid[trtable,Frame->All,Background->{{RGBColor[0.980392, 0.309804, 0.0196078],RGBColor[0.980392, 0.309804, 0.0196078],RGBColor[0.501961, 1, 1],RGBColor[0.501961, 1, 1],RGBColor[0.501961, 1, 1],RGBColor[0.501961, 1, 1]}}],"  ",Text@Grid[tabenomestne,Frame->All,Background->{{RGBColor[0.980392, 0.309804, 0.0196078],RGBColor[0.501961, 1, 1],RGBColor[0.501961, 1, 1],RGBColor[0.501961, 1, 1],RGBColor[0.501961, 1, 1]}}]}],ImageSize->{600,300},Alignment->{{Left,Left,Left},{Top,Center,Center}}],If[help,GraphicsRow[{prikazsveta[world1],Column[{Text[Style["",14]],Text[Style["  Large figures",14]],Text[Style["",14]],Text[Style["  Medium figures",14]],Text[Style["",14]],Text[Style["  Small figures",14]]}],Column[{Style["Symbols for operators",14],Style["Not (¬)",14],Style["And (∧)",14],Style["Or (∨)",14],Style["Implies (\[Implies])",14],Style["Equivalent (⇔)",14],Style["Possible (⋄)",14],Style["Necessary (\[Square])",14]}]},ImageSize->{500,300},Spacings->{0,0},Alignment->{{Left,Left,Left},{Center,Center,Center}}],
GraphicsRow[{
prikazsveta[svet],gr1,If[rezult,Style[Column[Map[pret2,tv]],12],""]},ImageSize->{660,300}]]]]]],{{rezult,True,"show results"},{False,True},Enabled->Dynamic[!(help || help2)],ControlPlacement->Top},{{lan,"English","language of predicates"},{"Slovenian","English"},Enabled->Dynamic[!(help || help2)],ControlPlacement->Top},{{k,4,"number of elements"},1,10,1,Appearance->"Labeled",Enabled->Dynamic[!(help || help2)],ControlPlacement->Top},{{k1,5,"number of literals"},1,5,1,Appearance->"Labeled",Enabled->Dynamic[!(help || help2)],ControlPlacement->Top},
{{k2,5,"number of molecular statements"},1,5,1,Appearance->"Labeled",Enabled->Dynamic[!(help || help2)],ControlPlacement->Top},
{{help,False,"used symbols"},{False,True},Enabled->!help2},
{{help2,False,"show truth tables"},{False,True},Enabled->!help},
{{try,False,"try again"},{False,True},Enabled->!(help||help2)},
{{ranint,2729},ControlType->None},
AutorunSequencing->{1,2,3,4,5,6,7},ControlPlacement->Left,
SaveDefinitions->True,ContentSize->{500,300}]

This Demonstration presents a test for Łukasiewicz's three-valued modal logic. The values are: True, False, and Possible, with associated numerical values 1, 0, 1/2, respectively. The value of compound propositions is evaluated according Łukasiewicz truth tables. The definition of possibility was discovered by Tarski in 1921: ⋄p⇔(¬p⇒p).

A simple two-dimensional area is occupied by triangles, squares, and pentagons of three sizes and two colors. A disk shape figure means that the shape of  the element is not known. In this case a proposition of type Shape(x) has value "possible". The notion of necessity can be introduced by the definition □ p ⇔ ¬ ⋄ ¬ p.

J.  Łukasiewicz, Philosophical Remarks on Many-valued Systems of Propositional Logic, in Polish Logic 1920-1939, Oxford: Clarendon Press, 1967, pp. 40–65.

Contributed by: Izidor Hafner