/ truth tables propositions:{@[_d;`$'x;:;2_vs!_2^#x];} modality:{:[&/x;`tautology;&/~x;`contradiction;`contingent]} letters:{?x@&x _lin"ABCDEFGHIJKLMNOPQRSTUVXYZ"} prove:{propositions letters x;modality@. x} prove"P|~P" prove"P&~P" prove"(((~P)|P|Q)&(~P)|(~Q)|Q)=(~(~P>Q)>~(~Q)>~P)"