"f = (f−, f+), j = (j−, j+), y = (y−, y+), and c = (c−, c+) Î B1, [(f Þ j)&(y Þ c)] Þ [(f*y) Þ (j*c)]; (f Û j) Þ [(f*y Û j*y)]; (fWj) Þ [(f*y)W(j*y)]; Two-fold universal instantiation: Operator instantiation: * as a universal operator can be bound to &, Å, &-, Å−, Ä, Æ, Ä-, Æ-. (f Þ j) is designated (bipolar true (−1, +1)); ((f−, f+)*(y−, y+)) is undesignated. Variable instantiation: "x, (f−, f+)(x) Þ (j−, j+)(x); (f−, f+)(A); \ (j−, j+) (A). |