Construct a Counterexample to Sorites

individuals=CharacterRange["A","L"];

dvomestneIzjavne={and,or,xor,impl,eq};dvomestneIzjavneM={And,Or,Xor,Implies,Equivalent};
dvomestnecons={" & "," v "," ⊻ "," -> "," ⟷ "};
individualconstants=CharacterRange["A","L"];
variables={x,y,z,u,v,w};
variablesS={"x","y","z","u","v","w"};
enomestni={small,medium,large,triangle,square,pentagon,white,gray};
enomestnioznS={"majhen","srednje velikosti","velik","trikotnik","kvadrat","petkotnik","bel","siv"};
enomestnioznA={"small","medium","large","triangle","square","pentagon","white","gray"};
enomestnioznArS={"majhen lik","lik srednje velikosti","velik lik","trikotnik","kvadrat","petkotnik","bel lik","siv lik"};
enomestnioznArA={"small","medium","large","triangle","square","pentagon","white","gray"};
dvomestni={larger,smaller,leftof,rightof, above,below};
dvomestnioznS={"večji kot","manjši kot","levo od","desno od","nad", "pod"};
dvomestnioznA={"larger than","smaller than","to the left of","to the right of", "above","below"};

ClosedLine[a_]:=Line[Append[a,First[a]]];
satisfies[and[x_,y_],structure_]:=satisfies[x,structure]&&satisfies[y,structure];
satisfies[and[x_,y_,z_],structure_]:=satisfies[x,structure]&&satisfies[y,structure]&&satisfies[z,structure];
satisfies[or[x_,y_],structure_]:=satisfies[x,structure]||satisfies[y,structure];
satisfies[eq[x_,y_],structure_]:=(satisfies[x,structure]&&satisfies[y,structure])||(satisfies[!x,structure]&&satisfies[!y,structure]);
satisfies[xor[x_,y_],structure_]:=(satisfies[x,structure]&&satisfies[!y,structure])||(satisfies[!x,structure]&&satisfies[y,structure]);
satisfies[impl[x_,y_],structure_]:=satisfies[y,structure]||satisfies[!x,structure];
satisfies[not[x_],structure_]:=!satisfies[x,structure];
satisfies[!x_,structure_]:=!satisfies[x,structure];
satisfies[id[x_],structure_]:=satisfies[x,structure];
satisfies[exists[x_,y_],structure_]:=Apply[Or,Table[satisfies[y/.{x:>structure[[i]]},structure],{i,1,Length[structure]}]];

satisfies[forall[x_,y_],structure_]:=Apply[And,Table[satisfies[y/.{x:>structure[[i]]},structure],{i,1,Length[structure]}]];

satisfies[all[x_][y_],structure_]:=Apply[And,Table[satisfies[y/.{x:>structure[[i]]},structure],{i,1,Length[structure]}]];

satisfies[ex[x_][y_],structure_]:=Apply[Or,Table[satisfies[y/.{x:>structure[[i]]},structure],{i,1,Length[structure]}]];

satisfies[large[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[2]]==3/;MemberQ[individuals,x];
satisfies[large[x_],structure_]:=x[[2]]==3;
satisfies[medium[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[2]]==2/;MemberQ[individuals,x];
satisfies[medium[x_],structure_]:=x[[2]]==2;
satisfies[small[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[2]]==1/;MemberQ[individuals,x];
satisfies[small[x_],structure_]:=x[[2]]==1;
satisfies[triangle[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[1]]==1/;MemberQ[individuals,x];
satisfies[triangle[x_],structure_]:=x[[1]]==1;
satisfies[square[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[1]]==2/;MemberQ[individuals,x];
satisfies[square[x_],structure_]:=x[[1]]==2;
satisfies[pentagon[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[1]]==3/;MemberQ[individuals,x];
satisfies[pentagon[x_],structure_]:=x[[1]]==3;
satisfies[white[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[4]]==1/;MemberQ[individuals,x];
satisfies[white[x_],structure_]:=x[[4]]==1;
satisfies[gray[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[4]]==0/;MemberQ[individuals,x];
satisfies[gray[x_],structure_]:=x[[4]]==0;
satisfies[larger[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[2]]>structure[[First[First[Position[individuals,y]]]]][[2]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[larger[x_,y_],structure_]:=x[[2]]>y[[2]];
satisfies[smaller[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[2]]<structure[[First[First[Position[individuals,y]]]]][[2]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[smaller[x_,y_],structure_]:=x[[2]]<y[[2]];
satisfies[leftof[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[3,1]]<structure[[First[First[Position[individuals,y]]]]][[3,1]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[leftof[x_,y_],structure_]:=x[[3,1]]<y[[3,1]];
satisfies[rightof[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[3,1]]>structure[[First[First[Position[individuals,y]]]]][[3,1]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[rightof[x_,y_],structure_]:=x[[3,1]]>y[[3,1]];
satisfies[above[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[3,2]]>structure[[First[First[Position[individuals,y]]]]][[3,2]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[above[x_,y_],structure_]:=x[[3,2]]>y[[3,2]];
satisfies[below[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[3,2]]<structure[[First[First[Position[individuals,y]]]]][[3,2]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[below[x_,y_],structure_]:=x[[3,2]]<y[[3,2]];
satisfies[eq[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]]==structure[[First[First[Position[individuals,y]]]]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[eq[x_,y_],structure_]:=x[[3]]==y[[3]]/;MemberQ[structure,x]&&MemberQ[structure,y];
satisfies[diff[x_,y_],structure_]:=structure[[First[First[Position[individuals,x]]]]]=!=structure[[First[First[Position[individuals,y]]]]]/;MemberQ[individuals,x]&&MemberQ[individuals,y];
satisfies[diff[x_,y_],structure_]:=x[[3]]=!=y[[3]]/;MemberQ[structure,x]&&MemberQ[structure,y];
tobesatisfiedin[structure_][formula_]:=satisfies[formula,structure];
chessboard={{RGBColor[0, 1, 1],{Table[Line[{{i,0},{i,8}}],{i,0,8}],Table[Line[{{0,i},{8,i}}],{i,0,8}]}},{GrayLevel[1],Line[{{-1,-1},{9,-1},{9,9},{-1,9},{-1,-1}}]}};


lik[{tip_,vel_,r_,bar_},{i_}]:={{GrayLevel[If[bar≠1,0.7,bar]],Polygon[Table[r+(1/5+If[vel==3,4,vel]/4){Sin[2 Pi n/(tip+2)],Cos[2 Pi n/(tip+2)]},{n,tip+2}]]},{GrayLevel[0],Text[individualconstants[[i]],r-vel/3{0,0}]}};
lik2[{tip_,vel_,r_,bar_}]:={{GrayLevel[0.],ClosedLine[Table[r+(1/5+If[vel==3,4,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[[Random[Integer,{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={Random[Integer,{1,3}],Random[Integer,{1,3}],nova,Random[Integer]};If[(nov[[2]]==3)&&Intersection[zasedeni,sosede]!={},nov=ReplacePart[nov,Random[Integer,{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=Union[zasedeni,{nova}],{j,1,i}];structure];
prikazsveta[svet_]:=Module[{sv1,sv2},sv1=MapIndexed[lik,svet];sv2=lik2/@svet;Show[Graphics[{chessboard,sv1,sv2}],AspectRatio->Automatic,BaseStyle->{FontSize->14},Axes->False,ImageSize->280]];

names1[fonts1_]=Text[Style[#,fonts1]]&/@CharacterRange["A","U"];names2=CharacterRange["A","U"];names1A[fonts1_]:=Table[Graphics[{RGBColor[0.501961, 0, 0.25098],Text[names1[fonts1][[i]],{0,0}]}],{i,1,20}];

tretji[r_]:=r[[3]];

(*aristotel["a"][{p1_,p2_}]={forall[x,impl[p1[x],p2[x]]],ForAll[x,Implies[p1[x],p2[x]]]};
aristotel["i"][{p1_,p2_}]={exists[x,and[p1[x],p2[x]]],Exists[x,And[p1[x],p2[x]]]};
aristotel["e"][{p1_,p2_}]={forall[x,impl[p1[x],not[p2[x]]]],ForAll[x,Implies[p1[x],Not[p2[x]]]]};
aristotel["o"][{p1_,p2_}]={exists[x,and[p1[x],not[p2[x]]]],Exists[x,And[p1[x],Not[p2[x]]]]};*)

aristotel[tip_][{p1_,p2_}]:=Switch[tip,"a",{forall[x,impl[p1[x],p2[x]]],ForAll[x,Implies[p1[x],p2[x]]]},"i",{exists[x,and[p1[x],p2[x]]],Exists[x,And[p1[x],p2[x]]]},"e",{forall[x,impl[p1[x],not[p2[x]]]],ForAll[x,Implies[p1[x],Not[p2[x]]]]},"o",{exists[x,and[p1[x],not[p2[x]]]],Exists[x,And[p1[x],Not[p2[x]]]]}];

satisfies[InLeftPart[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[3,1]]<4/;MemberQ[individuals,x];
satisfies[InLeftPart[x_],structure_]:=x[[3,1]]<4;

satisfies[InUpperPart[x_],structure_]:=structure[[First[First[Position[individuals,x]]]]][[3,2]]<4/;MemberQ[individuals,x];
satisfies[InUpperPart[x_],structure_]:=x[[3,2]]>4;

satisfies[InMidlePart[x_],structure_]:=Abs[structure[[First[First[Position[individuals,x]]]]][[3,1]]-4]<2&&Abs[structure[[First[First[Position[individuals,x]]]]][[3,2]]-4]<2/;MemberQ[individuals,x];
satisfies[InMidlePart[x_],structure_]:=Abs[x[[3,1]]-4]<2&&Abs[x[[3,2]]-4]<2;

RandomKsublist[set_,k_]:=Module[{sub={},rest=set,new},
Do[new=rest[[RandomInteger[{1,Length[rest]}]]];sub=Append[sub,new];rest=Complement[rest,{new}],{k}];sub];

(*randomSyllogism:={aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InUpperPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InLeftPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][{InUpperPart,InLeftPart}]}*)

randomsyllogism[nsil_]:=Switch[nsil,2,{aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InUpperPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InLeftPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][{InUpperPart,InLeftPart}]},3,{aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InUpperPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{white,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{white,InLeftPart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][{InUpperPart,InLeftPart}]},4,{aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InUpperPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{white,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{white,triangle},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InLeftPart,triangle},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][{InUpperPart,InLeftPart}]},5,{aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InUpperPart,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{white,InMidlePart},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{white,triangle},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{small,triangle},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][RandomKsublist[{InLeftPart,small},2]],aristotel[{"a","i","e","o"}[[RandomInteger[{1,4}]]]][{InUpperPart,InLeftPart}]}];

Manipulate[With[{resitev=Dynamic[Grid[Table[{TraditionalForm[rsilog[[All,2]][[j]]],Style[satisfies[rsilog[[All,1]][[j]],ReplacePart[svet,Table[{i,3}->nn[[i]],{i,1,Length[svet]}]]]]},{j,1,nsil+1}],Spacings->{0,1},Dividers->{False,Join[Table[False,{nsil}],{True}]},Background->{RGBColor[.9, 1, 1]}]]},Pane[Labeled[LocatorPane[Dynamic[nn],Dynamic[prikazsveta[ReplacePart[svet,Table[{i,3}->nn[[i]],{i,1,Length[svet]}]]]],{{1/2,1/2},{7.5,7.5},{1,1}},Appearance->None,ContinuousAction->False,ImageSize->280],If[taken&&set,resitev,""],Bottom],{300,480}]],
{{nsil,2,"set the number of premises"},Range[2,5],Enabled->!set&&!taken},{{set,False,"the number was set"},{True,False}},{{rsilog,randomsyllogism[nsil]},ControlType->None},Button["take argument",rsilog=randomsyllogism[nsil];taken=True,ImageSize->120,Enabled->set],{{taken,False,"syllogism was taken"},{True,False}},{{shape,1},Range[3]},{magnitude,Range[3]},{{color,1},{0,1}},{svet,{},ControlType->None},{{nn,Table[{i-1/2,i-1/2},{i,1,8}]},ControlType->None},

Row[{Button["reset",svet={},ImageSize->80],
Button["add new figure",svet=Append[svet,{shape,magnitude,{RandomInteger[{1,8}],RandomInteger[{1,8}]}-{1/2,1/2},color}],ImageSize->100,Enabled->Dynamic[Length[svet]<8]],Button["remove last figure",svet=Drop[svet,-1],ImageSize->100,Enabled->Dynamic[Length[svet]>0]]}],SaveDefinitions->True]

Aristotelian logic, or the traditional study of deduction, deals with four so-called categorical or subject-predicate propositions, which can be defined by
S a P ⇔ All S is P (universal affirmative or A proposition),
S i P ⇔ Some S is P (particular affirmative or I proposition),
S e P ⇔ No S is P (universal negative or E proposition),
S o P ⇔ Some S is not P (particular negative or O proposition).
S is called the subject (or minor) term and P is called the predicate (or major) term of the proposition. A categorical syllogism is a deductive argument about categorical propositions in which a conclusion is inferred from two premises. The term M that occurs in both premises is called the middle term. An example of a syllogism is M a P, S i M ⊨ S i P. There are 256 possible triples of categorical propositions, but only 24 valid syllogisms, some of which need existential support (Ex(S), Ex(P), or Ex(M), where Ex means "there is" or "there exists"). Without existential support there are 15 valid and 241 invalid syllogisms.

Sorites is an argument consisting of a sequence of categorical syllogisms such that the conclusion of each syllogism except the last one is a premise of the next syllogism. 
The aim of this Demonstration is to construct a counterexample, if possible, to given syllogism or sorites. We use predicates InLeftPart, InUpperPart, InMidlePart for S, P, M. For additional predicates we use white, triangle and small.

Here is an example by Lewis Carroll [4, p.112] of (valid) sorites:

Every one who is sane can do Logic.

No lunatics are fit to serve on a jury.

None of your sons can do Logic.

Therefore none of your sons is fit to serve on a jury.

[1] R. Audi, ed., The Cambridge Dictionary of Philosophy, Cambridge: Cambridge University Press, 1995 pp. 780–782, 753-754.

[2] J. Barwise and J. Etchemendy, Tarski's World, Stanford, CA: CSLI Publications, 1993.
[3] L. Borkowski, Elementy logiki formalnej (Elements of Formal Logic, in Polish), 3rd ed., Warsaw: Wyd, 1976.
[4] L. Carroll, Symbolic Logic and the Game of Logic, New York: Dover, 1958.
[5] I. M. Copi and C. Cohen, Introduction to Logic, 9th ed., New York: Macmillan, 1994 pp. 214–218, 300-302.

Contributed by: Izidor Hafner