Now That’s Indirect
October 8th, 2007 by WaltIn Chang and Keisler’s Model Theory, they give one of the most indirect proofs I’ve ever seen. They prove a theorem assuming the continuum hypothesis, and then they prove a metatheorem that any theorem of that particular form proven using the continuum hypothesis must also have a different proof that does not use the continuum hypothesis. They don’t actually exhibit this proof — they just prove that it exists. (The theorem shows that a theory preserves reduced products if and only if it can be defined entirely in terms of Horn sentences.)
October 9th, 2007 at 5:33 am
Take that, Constructivism!
(I assume that if they could actually construct the proof without CH, they would just present that)
October 9th, 2007 at 9:53 am
A sentence obtained from basic Horn formulas by conjunctions and quantifiers is called a Horn sentence. To put this another way, a Horn sentence consists of a conjunction of sentences, each of them being a disjunction of several (none, one or more) negative literals and maximum one positive literal. Or, a third way:
A Horn sentence is logically equivalent to a conjunction of conditional statements having one of the following forms:
1. (A1/\…/\An) -> B
2. (A1/\…/\An) -> False
3. True -> B
It was Horn who established a sufficient condition for an elementary class to be closed under direct product. Chang and Morel showed that this is not a necessary condition. Appel showed that, if condition is restricted to identity theory (first order predicate calculus with equality but no other relation symbols or operation symbols), then Horn’s condition is necessary and sufficient.
Horn Sentences in Identity Theory
K. I. Appel
The Journal of Symbolic Logic, Vol. 24, No. 4 (Dec., 1959), pp. 306-310
I’m pretty sure that the Chang of Chang and Morel is thew same as that of Chang and Keisler’s Model Theory.
Which reminds me of the drunk who phoned the TV network when Connie Chung was anchoring a broadcast after a minor abrasion to her face from a household accident.
“What,” he asked, “happened to Connie Chin’s chung?”
October 9th, 2007 at 10:20 am
This isn’t a very unusual proof style. Any time you infer A=>B by supposing A and concluding B you’re using the Deduction Metathereom. Actually converting a ‘proof’ that uses hypotheses into a real proof from axioms that doesn’t is a non-trivial task. (It’s equivalent, curiously, to lambda abstraction in computer science, so it’s something that sometimes gets implemented in compilers.).
Another nice example is the metatheorem of non-standard analysis that says that proofs of the right type using infinitesimals can be converted into theorems of ordinary analysis using conventional deltas and epsilons.
October 9th, 2007 at 2:31 pm
sigfpe - you’re only using the deduction theorem there if your proof system is Hilbert-style. If the formal system in play is a “natural-deduction” system, then this is in fact the only standard way to prove a conditional.
Of course, in ordinary mathematics, there’s no formal system at work, so it doesn’t really make sense to reconstruct the argument one way rather than the other, so I’m not sure if it’s quite right to compare this style of proof with the one at work here.
Although, people often call reductio an indirect proof, and in natural deduction systems that’s the only standard way to prove a negative, so maybe there’s something to this. (Perhaps it only counts as indirect if it also uses a double-negation step?)
The example from non-standard analysis feels much more similar to me. One proves that statements of a certain sort are true in the reals iff in the hyperreals, and then proves it for the hyperreals, so it must be true in the reals. Similarly, one proves that statements of a certain sort are true in all universes of sets iff they are true in a universe with CH, and then proves it for a universe with CH, so it must be true in all universes of sets. Viewed in this metatheoretic way, these proofs aren’t even really indirect - they really do give a proof of the result, though perhaps the phrasing of the result is different than one expected.
October 14th, 2007 at 5:28 pm
> you’re only using the deduction theorem there if your proof system is Hilbert-style.
As far as I can tell, that is what most mathematicians use most of the time.