Unipolar Axioms (UAs):

UA1:

UA2:

UA3:

UA4: (a)

(b)

UA5:

Bipolar Axioms (BAs):

BA1:

BA2:

BA3:

BA4: (a)

(b)

BA5:

Inference Rule-Modus Ponens (MP):

UR1:

Bipolar Universal Modus Ponens (BUMP) (* can be bound to any binary bipary bipolar operator)

BR1: IF

THEN

Predicate axioms and rules

UA6:

UA7:

UR2-Generalization

Bipolar Predicate axioms and Rules of inference

BA6:

BA7:

BR2-Generalization: