Disjunctive logic and semantics of disjunctive logic programs

In common sense reasoning with incomplete knowledge bases, conclusions are made by default. However, it is observed that when the negation-by-default operator not is defined as not provable, the disjunctive logic program {a boolean OR b, not a, not b} should be consistent because a being not provable and b being not provable does not imply a boolean OR b being not provable. Such an observation is significant for non-monotonic reasoning, but none of the major current semantics for disjunctive logic programs is able to support it because they are all based on classical first-order logic in which assuming not a and not b implies assuming not (a boolean OR b). A new first-order logic (disjunctive logic) is developed that fully complies with this observation and new semantics for disjunctive logic programs are established. This theory is able to formalize and solve some paradoxical problems, such as the lottery paradox.