Equivalential Formula

rulesG={{x_,{x_,y_}}:>y,{{x_,y_},z_}:>{x,{y,z}},{x_,{{y_,z_},w_}}:>{x,{y,{z,w}}},{x_,{y_,z_}}:>{x,{z,y}},{x_,{{y_,z_},w_}}:>{x,{z,{y,w}}}};

Convert[p_]:=(p/;AtomQ[p]);
Convert[{p_,q_}]:=StringJoin["E",Convert[p],Convert[q]];

pletters=CharacterRange["p","v"];

formulaexample={{{{x,y},z},w},{{{{{x,y},z},w},v},a},{{{{{{{x,y},z},w},v},a},b},c},{{{{{{{{{x,y},z},w},v},a},b},c},d},e},{{{{{{{{{{{x,y},z},w},v},a},b},c},d},e},f},g}};

RandomKsublist[set_,k_]:=Module[{sub={},rest=set,new},
Do[new=rest[[RandomInteger[{1,Length[rest]}]]];sub=AppendTo[sub,new];rest=Complement[rest,{new}],{k}];sub];
Randompermut[k_]:=RandomKsublist[Range[k],k];
set2[n_]:=Flatten[Table[{i,j},{i,-n+1,n-1},{j,-n+1,n-1}],1];

taut= {{{2,2}},{{2,2,2},{4,2}},{{2,2,2,2},{4,2,2},{4,4}},{{2,2,2,2,2},{4,2,2,2},{4,4,2}},{{2,2,2,2,2,2},{4,2,2,2,2},{4,4,2,2},{4,4,4}}};

set[k_]:=Module[{kom=Random[Integer,{1,Length[taut[[k]]]}],komb},komb=taut[[k,kom]];Flatten[Table[Table[pletters[[i]],{komb[[i]]}],{i,1,Length[komb]}]][[Randompermut[2k+2]]]];

rulesLetter1={x,y,z,w,v,a,b,c,d,e,f,g};

randformulaT[k_]:=Module[{formula=formulaexample[[k]],kk=Random[Integer,{1,k}],set1,rul},Do[formula=formula/.rulesG,{i,1,kk} ];set1=set[k];rul=Table[rulesLetter1[[i]]->set1[[i]],{i,1,2k+2}];formula/.rul]

setpl=Join[Take[pletters,3],Take[pletters,3],Take[pletters,3],Take[pletters,3]][[Randompermut[12]]];

randformula[k_]:=Module[{formula=formulaexample[[k]],kk=Random[Integer,{1,k}],rul},Do[formula=formula/.rulesG,{i,1,k} ];rul=Table[rulesLetter1[[i]]->setpl[[i]],{i,1,2k+2}];formula/.rul];

Manipulate[SeedRandom[ranint];With[{len=Random[Integer,{1,5}]},With[{formula={randformulaT[len],randformula[len]}[[Random[Integer,{1,2}]]]},Column[{If[show,If[Apply[And,Map[EvenQ,Map[Count[Flatten[formula],#]&,pletters]]],"Yes!","No!"],"Is the formula a tautology?"],"","",Style[Convert[formula],20]}]]],{{ranint,RandomInteger[1233455]},ControlType->None},Button["new equivalential formula",(*an=0;*)show=False;ranint=RandomInteger[{1,23423}]],{{show,False,"show answer"},{True,False}},SaveDefinitions->True, ContentSize->{400,300}]

The Demonstration asks whether a formulae of equivelential calculus is a tautology. Is here any simple rule?

In 1929 Leśniewski recognized that the equivalential calculus could be axiomatized. He also observed that a formula of propositional calculus in which the equivalence was  the only propositional function was a tautology if and only if each propositional letter has even number of appearances in it.

Jan Lukasiewicz, The Equivalential Calculus, in Polish Logic (1920 - 1939) (S. McCall, editor), Oxford, Clarendon Press, 1967, pp. 90-91.

Contributed by: Izidor Hafner