From lusk Mon Jun 20 15:54:21 1994
Received: from head.cs.wisc.edu (head.cs.wisc.edu [128.105.9.41]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id PAA07073 for ; Mon, 20 Jun 1994 15:53:19 -0500
Date: Mon, 20 Jun 94 15:53:16 -0500
From: kunen@cs.wisc.edu (Ken Kunen)
Message-Id: <9406202053.AA12534@head.cs.wisc.edu>
Received: by head.cs.wisc.edu; Mon, 20 Jun 94 15:53:16 -0500
To: qed@mcs.anl.gov
Subject: AC and Description
Regarding the discussion of Roger Jones and John Harrison on
whether you can derive AC if you allow constructs of the form
(there exists a unique x such that Px) => P(the x such that Px) (1)
and
(there exists an x such that Px) => P(some x such that Px) (2)
:
I believe this is an issue in general logic, not specific to HOL,
and revolves about the implementation of schemata such as Comprehension.
Consider (2) first: It is a general fact of logic that adding a Skolem
function is conservative. It doesn't matter whether there are additional
free variables. Thus, say T is some axiomatic theory and P(y,z,x) is
some predicate in the language of T. You may add a new function symbol,
f, and add a new axiom to the theory:
forall y z [(exists x P(y,z,x)) --> P(y,z f(y,z))] (*)
Then, if phi is some sentence in the original language of T and phi
is provable from T + (*), then phi is provable from T alone.
In particular, phi could be AC (say, "every set can be well-ordered"),
if T is some sort of set theory or type theory in which the relevant
notions can be expressed.
BUT, if T is set theory, you have to be careful that
the Comprehension schema be used only with formulae from the original
language. If you extend Comprehension to involve formulae in f,
you will derive AC -- the extension is no longer conservative.
BUT, there are two situations in which the extension is still conservative,
even if you extend Comprehension to involve formulae in f:
a: Situation (1): where it is provable from T that for each y,z,
there is no more than one x satisfying P(y,z,x). Then each
formula in f is equivalent to a formula without f, so Comprehension
with formulae in f is still conservative.
b: P has no free variables other than x, so f is a Skolem constant.
This is OK because the Comprehension schema allows an arbitrary
number of fixed parameters.
Ken Kunen