Wednesday, May 22, 2013

Relative proofs of consistency

In the last post, we defined and explained the importance of the property of consistency for an axiomatic system. The second half of Section II in Nagel and Newman's book describes ways of proving that an axiomatic system is consistent.

But first, note that the question of consistency of Euclidean geometry did not arise. Its axioms were supposed to describe the real world; and something that actually exists cannot be self-contradictory. In other words, existence (or truth) implies internal consistency.

The need for consistency proofs arose much later, with non-Euclidean geometries, which do not obviously model space as we experience it. Non-existence does not imply inconsistency. But any interesting abstract construct had better be internally consistent.

Second, checking the internal consistency of all of the theorems produced so far is typically not a valid proof of consistency, because (interesting) axiomatic systems generate an infinite number of theorems. The proof of consistency must guarantee that not a single theorem, including some that we have not yet produced and that we might never produce, contradicts any other theorem in the system.

One possible way to prove the consistency of an axiomatic system is model-based, where a model is a kind of interpretation.

An interpretation is a way to give meaning to an axiomatic system. More precisely, it is a mapping between the symbols of the system and entities that exist in a domain outside the system.

For example, one interpretation of our formal system FS is the following:
  • the symbol '0' maps to the binary digit zero (the 0 bit)
  • the symbol '1' maps to the binary digit one (the 1 bit)
  • the symbol 'E' maps to the property of being an even integer
  • In this example, we will take the domain of the interpretation to be the set of non-negative integers. 
  • More precisely, in FS, the string Ex (where x is a finite, non-empty sequence of 0's and 1's), is interpreted as the statement: "The non-negative integer whose binary representation is x is even."  If you need a refresher on the binary representation of integers, click here.

model, then, is an interpretation that makes all of the axioms in the system true. Of course, it is assumed that all of the inference rules are truth-preserving with respect to the model; that is, if the axioms are true, then so are all of the theorems derived from them within the system.

Now two interesting questions arise:
  1. Is the interpretation given above a model of FS ?
  2. How would you justify your answer to the previous question?
If you answered 'YES' to the first question, then, according to the model-based approach to consistency, FS is consistent.


Here is a possible argument:

[Premise 1] Under the given interpretation, FS perfectly mirrors a domain that exists outside of the axiomatic system.

[Premise 2] This domain exists (or is true), and is thus consistent; recall that existence (or truth) implies consistency.

[Conclusion] FS is consistent.

Unfortunately, the model-based approach exhibits at least two weaknesses that are illustrated in the two premises above, respectively:

  • Our model has an infinite domain (the set of non-negative integers). So how can we prove that FS really maps onto this domain, as stated in premise 1? In other words, how can we answer question 2 above? We certainly cannot do it by inspection, since we cannot possibly inspect an infinite number of elements. Given the extreme simplicity of FS, it is not surprising that axiomatic systems for full branches of mathematics (such as set theory, algebra, Euclidean and non-Euclidean geometries) typically do not have finite models. Unfortunately, intuitions about infinity are often misleading and do not protect from well-known contradictions or antinomies (i.e., inconsistencies). This is why David Hilbert developed a research program aimed at developing so-called finitary proof techniques.
  • In our example, the model is (a subset of) arithmetic. But in what sense does arithmetic exist? Why is it true, and thus consistent, as stated in premise 2? Shouldn't these questions be settled first? What the model-based approach really does is reduce the consistency of FS to the consistency of (a subset of) arithmetic. Therefore, this proof of consistency of FS is a relative proof. It states that if arithmetic is consistent, then FS is also consistent. Contrast this with the (absolute) statement: FS is consistent. This is what we really wanted to prove.

Nagel and Newman discuss other relative proofs of consistency, namely the proof given by Riemann of his non-Euclidean geometry relative to Euclidean geometry, as well as the proof given by Hilbert of Euclidean geometry relative to algebra.

Clearly, the model-based approach is not the final word on proofs of consistency. Next time, we'll address these issues when we discuss the following section in the book.

No comments:

Post a Comment