Interpretation

In the discussion above, the word "meaning" keeps coming up. It is necessary to formalize what is means by "meaning", as used in the above informal definition of logical consequence. An interpretation defines the meaning of symbols, functions, and statements.

An interpretation of a language takes the words used (the syntax) and associates them with the objects that they represent in the wider world. (That such an association is necessary for intelligent action is motivated in Newell and Simon's Turing Award paper [NS76], and that association motivates the use of semantics for search guidance.) Similarly, functions of the language are applied to objects in the world, and are evaluated to objects in the world. Finally, an interpretation determines whether statements written in the language are true or false.

Interpretation of statements

The words of statements are given an interpretation by associating each different part with an object in a set called the domain of the interpretation. Functions are given an interpretation by applying them to elements of the domain and assigning a result from the domain. Statements and connected statements are then interpreted using the interpretations of the component parts and the connectives.

Example

man → mortal → fly → Socrates → Xanthippe → Spouse of → Spouse of → All are → TRUE is a → TRUE is → TRUE could → FALSE

Example
man → mortal → fly → Socrates → Xanthippe → Spouse of → Spouse of → All are → TRUE is a → TRUE is → TRUE could → FALSE

Interpretation of connectives

Connectives are the words that join together nouns and verbs, e.g., and, or, all. There are 16 binary and 4 unary connectives. In English we have an intuition of their meaning (interpretation). In logic their intepretation is formally defined.

Interpretation of statements

Statements are interpreted by first interpreting the words, then the sentences without connectives, and then the full sentence. For example,

All men are mortal or Socrates could fly
All are or could
TRUE or FALSE
TRUE

Models, satisfiability, unsatisfiability

There are some definitions that make it easy to discuss the relationships between formulae and interpretations. Learn these words!

An interpretation is a model of a formula (set of formulae) iff the formula (the conjunction of the formulas in the set) is TRUE in the interpretation. For example, the interpretation above is a model of the formula All men are mortal, and of the set of formulae {All men are mortal, Socrates is a man, Socrates is mortal}.

A formula (set of formulae) is satisfiable iff it has a model. For example, the formula All men are mortal, and the set of formulae {All men are mortal, Socrates is a man, Socrates has a beard}, are satisfiable.

A formula (set of formulae) is valid iff every interpretation is a model. For example, the formula Socrates is either mortal or not mortal is valid (assuming the usual meaning of "either-or"). Valid formulae are also called tautologies, written |=. The example is written |= (Socrates is either mortal or not mortal).

A formula (set of formulae) is counter-satisfiable iff it's negation has a model. For example, the formula All men are mortal, and the set of formulae {All men are mortal, Socrates is a man, Socrates has a beard} are counter-satisfiable.

A formula (set of formulae) is unsatisfiable iff it has no models. For example, the set of formulae {All men are mortal, Socrates is a man, Socrates is not mortal} is unsatisfiable (if you think about it, but it will be proved formally later). Unsatisfiable formulae are also called contradictions.

Logical Consequence

Now that the notion of "meaning" has been formalised as interpretation, it is possible to formalize logical consequence - a conclusion that is TRUE independent of the meaning of the statements used. An alternative way of looking at logical consequence, as opposed to the conclusion being TRUE independent of the meaning, is to think of logical consequence as a conclusion that is TRUE for all possible meanings. If it is TRUE for all possible meanings then you can ignore the meaning, because it doesn't matter which one you choose. This is the idea used here. The formal definition of logical consequence is then:

A formula is a logical consequence of an axiom set if every model of the axiom set is also a model of the formula.

Notice the use of the word "every". That's what captures the ideas of "all possible meanings". The form used for writing the axioms and logical consequence formulae is Axioms |= Logical consequence. If all the axioms are TRUE then the logical consequence is necessarily TRUE, for all possible meanings of the symbols used.

The definition requires access to "every model of the axiom set". Is this possible? Consider again the very first example:

Example

A = { All men are mortal, Socrates is a man } C = Socrates is mortal

Example
A = { All men are mortal, Socrates is a man } C = Socrates is mortal

The deduced formula is apparently a logical consequence of the axioms, i.e., the symbols (man, mortal, Socrates) and the statements given can have any interpretation, and the conclusion will still be TRUE in that context.

The intended interpretation (and model of the axiom set) is :

man                → 
mortal             → 
Socrates           → 
All  are       → TRUE
 is a           → TRUE

and it is TRUE that Socrates is mortal. That makes sense, and that's what is intended. That "checks" one model of the axiom set. Another model of the axiom set is:

man                → 
mortal             → $$$
Socrates           → 
All  are $$$     → TRUE
 is a         → TRUE

Here the formula All men are mortal means every motor car is expensive, and Socrates is a man means a Corvette is a motor car. The conclusion Socrates is mortal means that a Corvette is expensive. Again the conclusion makes sense. That's another model checked. This process of checking models of the axiom set must continue for "every model of the axiom set". In general, there can be an infinite number of models, and so there appears to be a problem here, but this will be discussed and overcome in the context of propositional and 1st order logic, later. However, it is the case that the conclusion Socrates is mortal is a logical consequence of the axioms All men are mortal and Socrates is a man (unless you change what is meant by the connective all). In the argument form:
{All men are mortal, Socrates is a man} |= Socrates is mortal.

Non-logical Consequence

The formal definition of logical consequence can be transformed into one of non-logical consequence:

A formula is not a logical consequence of an axiom set if some model of the axiom set is not a model of the formula.

or equivalently

A formula is not a logical consequence of an axiom set if there is a model of the axiom set and the negation of the formula (they're satisfiable).

Here's an example of non-logical consequence:

Example (of non-logical consequence)

A = { All men are mortal, Socrates is a man } C = Socrates has a beard

Example (of non-logical consequence)
A = { All men are mortal, Socrates is a man } C = Socrates has a beard

Semantically, this conclusion is correct; Socrates did have a beard. There is indeed an interpretation that is a model of the axioms that is also a model of the conclusion.

man             → 
mortal          → 
beard           → 
Socrates        → 
All  are    → TRUE
 is a        → TRUE
 has a       → TRUE

However, there is another model of the axiom set that is not a model of the conclusion:

man             → 
mortal          → 
beard           → 
Socrates        → 
All  are    → TRUE
 is a        → TRUE
 has a       → FALSE

The conclusion is not a logical consequence or the axioms because there is a model of the axioms that is not a model of the conclcusion. Equivalently, the conclusion is not a logical consequence or the axioms because there is a model of the axioms and the negation of the conclusion:

man             → 
mortal          → 
beard           → 
Socrates        → 
All  are    → TRUE
 is a        → TRUE
Not( has a ) → TRUE

Checking for logical consequence

Generically, the process of checking for logical consequence can be thought of as checking rows of a table. There is one row of the table for each possible interpretation of the formulae, and a column for each axiom formula and a column for the conclusion formula. Then, for each row which is a model of all the axioms columns, it is necessary to check that the row is a model of the conclusion column. If this check always succeeds then the conclusion is a logical consequence of the axioms.

Interpretation Axiom 1 Axiom 2 ... Conclusion
1 Model Model all models Model
2 Model Model all models Model
3 Model Not model ... Doesn't matter
4 Model Model all models Model
5 Not model ... ... Doesn't matter
... ... ... ... ...
? Model Model all models Model

Interpretation	Axiom 1	Axiom 2	...	Conclusion
1	Model	Model	all models	Model
2	Model	Model	all models	Model
3	Model	Not model	...	Doesn't matter
4	Model	Model	all models	Model
5	Not model	...	...	Doesn't matter
...	...	...	...	...
?	Model	Model	all models	Model

Note that it is necessary to check the conclusion column only for those rows that are models of all the axiom columns. Other rows are not relevant to this process.

If one or more rows are models of the axioms but are not models of the conclusion, then the conclusion is not a logical consequence of the axioms.

Interpretation Axiom 1 Axiom 2 ... Conclusion
1 Model Model all models Model
2 Model Model all models Model
3 Model Not model ... Doesn't matter
4 Model Model all models Not model
5 Doesn't matter
... Doesn't matter
? Doesn't matter

Interpretation	Axiom 1	Axiom 2	...	Conclusion
1	Model	Model	all models	Model
2	Model	Model	all models	Model
3	Model	Not model	...	Doesn't matter
4	Model	Model	all models	Not model
5	Doesn't matter
...	Doesn't matter
?	Doesn't matter

If the axiom set has no models (i.e., it is unsatisfiable) then vacuously every formula is a logical consequence of the axiom set. (Relevance logics are designed to avoid this paradox.) In practical application of ATP it is sensible to check that axiom sets used are satisfiable, e.g., by building a model of the axioms.

Interpretation Axiom 1 Axiom 2 ... Conclusion
1 Model Not model ... Doesn't matter
2 Not model ... ... Doesn't matter
3 Model Not model ... Doesn't matter
... ... ... ... ...
? Model Not model ... Doesn't matter

Interpretation	Axiom 1	Axiom 2	...	Conclusion
1	Model	Not model	...	Doesn't matter
2	Not model	...	...	Doesn't matter
3	Model	Not model	...	Doesn't matter
...	...	...	...	...
?	Model	Not model	...	Doesn't matter

Logical Consequence via Unsatisfiability

The method for checking for logical consequence given above requires checking that each model of the axioms is a model of the conclusion. An equivalent method is to check that every model of the axioms is not a model of the negation of the conclusion. If the conclusion is a logical consequence, then no interpretation will be a model of both the axioms and the negated conclusion. That is, the set consisting of the axioms and the negated conclusion has no models, i.e., is unsatisfiable. This then provides an alternative method for checking that a conclusion C is a logical consequence of a set Ax:

A formula is a logical consequence of an axiom set iff every model of the axiom set is not a model of the negation of the formula, i.e., if Ax ∪ {~C} has no models, i.e. if Ax ∪ {~C} is unsatisfiable.

Interpretation Axiom 1 Axiom 2 ... ~ Conclusion
1 Model Model all models Not model
2 Model Model all models Not model
3 Model Not model ... Doesn't matter
4 Model Model all models Not model
5 Not model ... ... Doesn't matter
... ... ... ... ...
? Model Model all models Not model

Interpretation	Axiom 1	Axiom 2	...	~ Conclusion
1	Model	Model	all models	Not model
2	Model	Model	all models	Not model
3	Model	Not model	...	Doesn't matter
4	Model	Model	all models	Not model
5	Not model	...	...	Doesn't matter
...	...	...	...	...
?	Model	Model	all models	Not model

If any row is a model of the axioms and the negation of the conclusion, then the conclusion is not a logical consequence of the axioms.

Interpretation Axiom 1 Axiom 2 ... ~ Conclusion
1 Model Model all models Not model
2 Model Model all models Not model
3 Model Not model ... Doesn't matter
4 Model Model all models Model
5 Doesn't matter
... Doesn't matter
? Doesn't matter

Interpretation	Axiom 1	Axiom 2	...	~ Conclusion
1	Model	Model	all models	Not model
2	Model	Model	all models	Not model
3	Model	Not model	...	Doesn't matter
4	Model	Model	all models	Model
5	Doesn't matter
...	Doesn't matter
?	Doesn't matter

Logical Consequence by Inference

An inference rule infers formulae from parent formulae.

An inference rule is sound if it infers only logical consequences of its parents.

The basic procedure is:

Put the axioms in the initial set
While the conjecture has not been found
    Copy formulae from the set
    Generate logical consequences
    Put logical consequences into the set

Note the "Copy", indicating that a fresh copy of a formula may be used multiple times.

An inference system is complete if, by repetitive use, it can infer every logical consequence of its input.

Decidability of Logical Consequence

A reasoning system for a given logic is decidable if it can determine whether or a conclusion is a logical consequence or a non-logical consequence of a set of axioms. Equivalently, a reasoning system for a given logic is decidable if it can determine whether a set of formulae (e.g., axioms and negated conjecture) is satisfiable or unsatisfiable.

A reasoning system for a given logic is semi-decidable if it can determine that a conclusion is a logical consequence of a set of axioms, but may not be able to determine that a conclusion is a non-logical consequence of a set of axioms. Equivalently, a reasoning system for a given logic is semi-decidable if it determine that a set of formulae is unsatisfiable, but may not be able to determine that a set of formulae is satisfiable.

Exam Style Questions

Define the following terms used in classical logic:
- Interpretation
- Model
- Satisfiable
- Unsatisfiable
- Logical consequence
What does it mean for an inference system to be {sound, complete}?
Explain how unsatisfiability can be used to establish logical consequence in classical logic.