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 νb, nota, notb} should be consistent becausea being not provable andb being not provable does not implya ν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 nota and notb implies assuming not (a ν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.