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

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Hi,

just a quick comment before this becomes into some HOL vs FOL issue:
(conservative) extension by definitions
(http://en.wikipedia.org/wiki/Extension_by_definitions) is a standard
FOL method that used very often (e.g., when building up math in ZFC).
I believe standard logic textbooks (like Mendelson) discuss this
early.

Best,
Josef

On Fri, Sep 7, 2012 at 5:54 AM, Gottfried Barrow
<got...@gm...> wrote:
> 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
>
>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>