[Hol-info] Can I define a ZF FOL constant using only FOL symbols?

[Gottfried B. <got...@gm...>]

On 9/4/2012 1:53 AM, Ramana Kumar wrote:

THIS IS FROM: Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

>
>     I don't understand the question.  You know more than I do about
>     types & constants in HOL than I do, and I think these don't exist
>     in FOL.  I tried to explain that much of the ZC/FOL axioms (power
>     set, products...) are encoded in the HOL type system (->, prod/#).
>
>
>
> Constants do exist in FOL: they are called function/relation and 
> predicate symbols. In ZC/FOL you have constants like set-membership 
> and equality (both relations). But you can be more or less formal 
> about how you define new constants. In HOL, since we actually define 
> things like the logical connectives and quantifiers 
> (and,or,not,forall,etc.) rather than having them built into the 
> syntax, we have principles of definition.

Ramana,

I haven't been paying attention completely, so I don't know if the FOL 
constants you're talking about are the same constants I'll be asking about.

I'm interested in FOL constants because I'm trying to answer the 
question of whether ZF sets, as a FOL language, justifies statements 
like this:

    (Classic Set Theory, by Derek Goldrei, page 71)
    Before we give axioms for set theory, we must specify the framework 
within  which these axioms sit.
    That is the aim of this section. We shall write the axioms using a 
very limited language, one that fits
    a formal logical treatment using the predicate calculus. For the 
purposes of this book, it is important
    to be able to use and interpret the formal language, but not to 
construct formal proofs using it. /

    It is, however, important to realize that such formal proofs can in 
principle be given./ (emphasis mine)

So supposedly, we can translate any proof into the formal, first-order 
language of ZF sets as originally specified, that is, by not 
substituting an enhanced FOL language in its place.

As I'm seeing it, ZF sets gives us no ability to define constants and 
notation, and so it must be supplemented as a language, or it must be 
replaced by another language of FOL.

For example, how do I name the empty set using only the FOL symbols that 
ZF sets has been specified to have?

That's my basic question. Whether that can or can't be done answers my 
bigger question.

For reference, I'm using "A Problem Course in Mathematical Logic" by 
Bilaniuk. Unlike him, I assume all the standard logical symbols.
http://euclid.trentu.ca/math/sb/pcml/pcml.html
     Definition 5.1: Symbols (page 24)
     Definition 5.2: Terms (page 26)
     Definition 5.3: Formulas (page 27)

I can see that theorems and axioms can be stated for ZF sets with FOL 
formulas.

However, please consider the empty set. It is described by a formula:

     \<exists> x \<forall> y ~(y IN x) .

For ZF sets we have the following available:

     Definition 5.1
     LOGICAL SYMBOLS: (, ), ~, -->, \<exists>, \<forall>, an infinite 
number of variables, =.
     NON-LOGICAL SYMBOLS: membership predicate, no constants, no functions.

     Definition 5.2:
     TERMS: the only terms are the variables.

     Definition 5.3: FORMULAS
         (1) If x and y are variables, then (x IN y) is a formula.
         (2) If x and y are variables, then x = y is a formula.
         (3) If phi is a formula then (~phi) is a formula.
         (4) If alpha and beta are formulas, the (alpha --> beta) is a 
formula.
         (5) If phi is a formula and x is a variable, then (\<forall>x. 
phi) is a formula.
         (6) Nothing else is a formula.

Okay, so I assume the other formulas from the other standard logical 
connectives, and I paraphrased some of the sentences, because the only 
terms are variables.

So maybe you can tell me how to define a constant for the empty set, so 
we can use it on the LHS or RHS side of the two predicates, membership 
and equal.

The empty set is inseparable from the universal quantifer. You can't use 
a FOL formula on the LHS or RHS of the membership predicate.

My answer to my question is that what's being done is a new FOL language 
for ZF sets is replacing the previous FOL language every time a new set 
constant is introduced.

After all, in the FOL specification, a FOL language can have as many 
constants as it wants, and I'm thinking that typical set builder 
notation is a string of characters that qualifies for item (6) in 
Definition 5.1:

     (6) A (possibly empty) set of constant symbols.

If you can help answer my question, please do.

Regards,
GB