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))