Unipolar Axioms (UAs): UA1: f®(j®f); UA2: (f®(j®c))®((f®j)®(f®c)); UA3: Øf®j)®((Øf®Øj)®f); UA4: (a) fÙj®f; (b) fÙj®j; UA5: f®(j®fÙj); | Bipolar Linear Axioms: BA1: (f −, f+) Þ ((j−, j+) Þ (f−, f+)); BA2: ((f−, f+) Þ ((j−, j+) Þ (c−, c+))) Þ (((f−, f+) Þ (j−, j+)) Þ ((f−, f+) Þ (c−, c+))); BA3: (Ø(f−, f+) Þ (j−, j+)) Þ ((Ø(f−, f+) Þ Ø(j−, j+)) Þ(f−, f+)); BA4: (a) (f−, f+)&(j−, j+) Þ (f−, f+); (b) (f −, f+)&(j −, j+) Þ (j −, j+); BA5: (f−, f+) Þ ((j−, j+) Þ ((f−, f+)&(j−, j+))); |
Inference Rule
―Modus Ponens (MP): UR1: (fÙ(f®j))®j. | Non-Linear Bipolar Universal Modus Ponens (BUMP) (* can be bound to any bipolar operator in Table 1) BR1: IF ((f−, f+)*(y−, y+)), [((f−, f+) Þ (j−, j+))&((y−, y+) Þ (c−, c+))], THEN [(j−, j+)*(c−, c+)]; |
Predicate axioms and rules UA6: "x, f(x)®f(t); UA7: "x, (f®j)®(f®"x, j); UR2-Generalization: f®"x, f(x) | Bipolar predicate axioms and rules of inference BA6: "x, (f −(x), f+(x)) Þ (f −(t), f+(t)); BA7: "x, ((f −, f+)Þ(j−, j+)) Þ ((f−, f+) Þ "x, (j −, j+)); BR2-Generalization: (f −, f+) Þ "x, (f −(x), f+(x)) |