SUO: Re: Practical Consistency Verification
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PCV. Discussion Note 1
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
CM = Chris Menzel
JA = Jon Awbrey
JA, correcting some typos:
When it comes to worries about the consistency of a set of postulates,
let me recommend to you the following strategy, which has the advantage
of having been field-tested by many generations of people who actually
prove non-trivial theorems about difficult objects.
JA: Examples! Examples! Examples!
JA: That's how it was told to me, so please excuse the exclamations.
JA: For example, when I say that there is a non-commutative group of six
elements, I can justify my claim by constructing a non-commutative
group of six elements.
JA: That example, say G, is a "model" of the following postulates:
1. G satisfies the axioms for a group.
2. G is not commutative.
3. G has six elements.
JA: Now, any exercise in formal semantics or model theory is nothing but
a translation from one language to another, and this is no different.
CM: The exercise in question is certainly not a matter of mere translation.
The satisfaction problem (i.e., the problem of finding a model for a
given set of sentences) even for propositional logic is intractable
(assuming P =/= NP). It is obviously intractable for first-order logic,
as even small finite sets of sentences can require infinite models.
CM: Finding models is of course a nice way to convince oneself of the
consistency of a given theory (relative, of course, to the assumed
consistecy of whatever set theory one happens to use to build one's
models) but this is not in general, even for very simple cases,
a procedure that can be implemented.
Chris,
I have changed the title to capture a pun on "Pollution Control Valve".
I think that this illustrates one of those basic misunderstandings that
may be worth trying to clear up. My emphasis is on "practical". I am
thinking about the basic experiences upon which our confidence of making
sense is based, recursively or otherwise, when we practice to talk about
things like graphs, groups, geometries, integers, and so on up the line.
It is true that I view the standard sorts of model theory as the study of translations
from arbitary formal systems, say, lambda calculus, into set-theoretic language, thus
arriving at set-theoretic models of the theory in question. If you reflect on why
anybody imagines that such translations help us understand the source subject,
it seems to be only their greater familiarity with the target language --
it cannot be that talk-about-sets is really more concrete in principle
than what they started with, nor that we have consistency proofs for
the axiomatic set theory of their choice, not even for finite sets.
But I am not really even talking about all that stuff yet.
I am talking about what I did when I was first learning group theory,
cutting out a cardboard triangle, labeling the corners, flipping it
about and rotating it around on my desk until I got some measure of
concrete experience with my first non-abelian group. That sort of
modeling. Those sorts of implements. Everthing else I imagine
I think I know about groups comes down to experiences like that.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o