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