Soundness, Completeness, Consistency, Satisfiability

Soundness, Completeness, Consistency, Satisfiability: A Logic D is Sound iff for all sets of formulae GAMMA and any formula A:

• if A is derived from GAMMA in D, then A is a logical consequence of GAMMA

A Logic D is Complete iff for all sets of formulae GAMMA and any formula A:

• If A is a logical consequence of GAMMA, then A can be derived from GAMMA in D.

A Logic D is Refutation Complete iff for all sets of formulae GAMMA and any formula A:

• If A is a logical consequence of GAMMA, then the union of GAMMA and (NON A) is inconsistent

Note that if a Logic is Refutation Complete then we can enumerate all the logical consequences of GAMMA and, for any formula A, we can reduce the question if A is or not a logical consequence of GAMMA to the question: the union of GAMMA and NOT A is or not consistent.

We will work with logics that are both Sound and Complete, or at least Sound and Refutation Complete.

A Theory T consists of a logic and of a set of Non-logical axioms. For convenience, we may refer, when not ambiguous, to the logic of T, or the non-logical axioms of T, just as T.

The common situation is that we have in mind a well defined "world" or set of worlds. For example we may know about the natural numbers and the arithmetic operations and relations. Or we may think of the block world. We choose a language to talk about these worlds. We introduce function and predicate symbols as it is appropriate. We then introduce formulae, called Non-Logical Axioms, to characterize the things that are true in the worlds of interest to us. We choose a logic, hopefully sound and (refutation) complete, to derive new facts about the worlds from the non-logical axioms.

A Theorem in a theory T is a formula A that can be derived in the logic of T from the non-logical axioms of T.

A Theory T is Consistent iff there is no formula A such that both A and NOT A are theorems of T; it is Inconsistent otherwise. If a theory T is inconsistent, then, for essentially any logic, any formula is a theorem of T. [Since T is inconsistent, there is a formula A such that both A and NOT A are theorems of T. It is hard to imagine a logic where from A and (NOT A) we cannot infer FALSE, and from FALSE we cannot infer any formula. We will say that a logic that is at least this powerful is Adeguate.

A Theory T is Unsatisfiable if there is no structure where all the non-logical axioms of T are valid. Otherwise it is Satisfiable.
Given a Theory T, a formula A is a Logical Consequence of T if it is a logical consequence of the non logical axioms of T.

Theorem: If the logic we are using is sound then:

1. If a theory T is satisfiable then T is consistent
2. If the logic used is also adequate then if T is consistent then T is satisfiable
3. If a theory T is satisfiable and by adding to T the non-logical axiom (NOT A) we get a theory that is not satisfiable Then A is a logical consequence of T.
4. If a theory T is satisfiable and by adding the formula (NOT A) to T we get a theory that is inconsistent, then A is a logical consequence of T.