A news.group post I snagged to think about later ... related to the question of [[http://www3.canisius.edu/~moleski/proof/provenegs.htm|"proving negatives."]]

<code>
Xref: sn-us news.groups:543329
Path: sn-us!sn-feed-sjc-01!sn-us!sn-feed-sjc-04!sn-xt-sjc-10!sn-xt-sjc-01!sn-xt-sjc-13!supernews.com!news.glorb.com!postnews.google.com!19g2000hsx.googlegroups.com!not-for-mail
From: aatu.koskensilta@xortec.fi
Newsgroups: news.groups
Subject: Re: Policy Discussion -> Re: Brainstorming Session - "Obvious Groups"
Date: Tue, 02 Oct 2007 06:35:22 -0700
Organization: http://groups.google.com
Lines: 36
Message-ID: <1191332122.544516.59560@19g2000hsx.googlegroups.com>
References: <tskirvin.20070911173402$048f@cairo.ks.uiuc.edu>
   <871wcx3914.fsf@huxley.huxley.fi>
   <46ee5e17$0$47135$892e7fe2@authen.yellow.readfreenews.net>
   <87k5qp1rmy.fsf@huxley.huxley.fi>
   <46ee62ad$0$47143$892e7fe2@authen.yellow.readfreenews.net>
   <87ejgx1qhg.fsf@huxley.huxley.fi>
   <46fbc74b$0$32559$4c368faf@roadrunner.com>
   <1190986310.390055.37540@o80g2000hse.googlegroups.com>
   <46ffafbe$0$7464$4c368faf@roadrunner.com>
   <87r6kgnsah.fsf@huxley.huxley.fi>
   <47015ac2$0$32478$4c368faf@roadrunner.com>
NNTP-Posting-Host: 81.197.123.102
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
X-Trace: posting.google.com 1191332122 30382 127.0.0.1 (2 Oct 2007 13:35:22 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 2 Oct 2007 13:35:22 +0000 (UTC)
In-Reply-To: <47015ac2$0$32478$4c368faf@roadrunner.com>
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.9) Gecko/20050711 Firefox/1.0.5,gzip(gfe),gzip(gfe)
Complaints-To: groups-abuse@google.com
Injection-Info: 19g2000hsx.googlegroups.com; posting-host=81.197.123.102;
   posting-account=ps2QrAMAAAA6_jCuRt2JEIpn5Otqf_w0

dvus wrote:
> Aatu Koskensilta wrote
>
> > Mathematical logicians are paid by other mathematical logicians whose
> > work is equally uninteresting to any sane person. Perhaps you would
> > like to know why, on the assumption that every set is constructible,
> > there is no finitely axiomatisable higher-order theory that is
> > complete but not categorical?
>
> Quantum erasers?

Alas, no.

The proof is rather simple. First recall that there is a definable
well-ordering < of the constructible universe. Observe then that for
finitely axiomatisable higher-order theories T the property of a model
being isomorphic to <-least model of T is expressible by a purely
logical sentence. Let now A be this sentence. Since the <-least model
M of T is, trivially, a model of T, A holds in M. So T can't refute A,
which means A is actually provable since T is complete, and thus all
models of T are isomorphic. This concludes the sketch of the proof
that, assuming V=L, all complete finitely axiomatisable higher-order
theories are categorical.

This is the sort of exciting stuff we logicians like to prattle about.
In set theory we often also talk about the universal weasel, premice,
the zero-handgranade, the axiom of playful universe, ineffable
cardinals, small large cardinals, large large cardinals,
indestructibility, forcing, games between God and Devil, etc.

--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

</code>