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

[Konrad S. <kon...@gm...>]

Hi Gottfried,

  I didn't read all of your (long) message. However,
I agree with Josef: conservative extension principles for FOL are
well known, even if not discussed in all set theory texts. I just consulted
two (Shoenfield's "Mathematical Logic" and Moschovakis "Notes on
Set Theory"): the former has a detailed discussion, while the latter
discusses Zermelo's idea of a "definite condition" in reasonable depth.

 On the other hand, you might enjoy reading the following article by
Adrian Mathias:

   http://www.dpmms.cam.ac.uk/~ardm/inefff.dvi

Cheers,
Konrad.


On Fri, Sep 7, 2012 at 10:13 AM, Gottfried Barrow
<got...@gm...> wrote:
> On 9/7/2012 4:41 AM, Josef Urban wrote:
>> 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
>
> Josef,
>
> Thanks for the link. That tends to confirm my basic idea that when the
> many mathematicians say that axiomatic ZFC is the language of
> mathematics, as described in a typical axiomatic set theory book, it's
> not. The language of mathematics based on ZFC sets is possibly something
> as described by the wiki page. All I care about is that the
> mathematicians of the world acknowledge what the real, traditional
> language of mathematics has been for the last 100 years or so.
>
> For me it's not a HOL vs. FOL thing at all. I'm totally out of the
> mentality that I have to choose one or the other. In fact, I'm currently
> assuming that I can acceptably get FOL through HOL. It makes sense. Just
> because HOL provides 2-order and greater logic doesn't mean I have to
> resort to 2-order or greater logic. Actually, it is inescapable that I
> have to resort to a few higher-order functions to get access to the
> constants I need to use in FOL formulas. And, of course, all the FOL
> logical connectives are HOL functions. So maybe it's a matter of I'm
> assuming I can acceptably get the semantics of FOL using HOL, but still,
> other than the constants and predicates that have to be defined with HOL
> functions, I'm primarily limiting myself to the FOL logical connectives
> and quantifiers that HOL gives me.
>
> I'm totally committed to doing math as traditional as possible with
> theorem assistants, but if ZFC sets isn't a complete language, as
> proposed by the many axiomatic set theory books, then it can't ever be
> formalized using proof assistants exactly as it's traditionally
> specified, where I gave the basic specifications in the first email,
> which, of course, have nothing to do with me.
>
> Here's the summary of what I'm doing, and will be doing:
>
> I'm looking for quotes from mathematics, logicians, or computer
> scientists, who have authoritative credentials
> in the field of logic or set theory, to counter the idea that ZFC is a
> complete language, and to counter the idea
> that ZFC has ever really qualified as a complete solution for a formal
> language of mathematics, because of how
> it's been specified and locked in as a language of FOL.
>
> But before I go any further, I'm open to the idea that I have a basic,
> simple misunderstanding of first-order logic, and that's why I pose the
> simple question, "Can someone please tell me how to define a constant
> for the set which exists which has no elements, and do so using only the
> symbols that have been given to ZFC sets, as ZFC sets has been
> specifically defined and initially locked in according to the general
> FOL specification?"
>
> I looked at Mendelson's book. He may discuss logic extensions somewhere
> in the book similar to what the wiki page describes, but starting on
> page 288, he gives a two page summary of ZF sets. I don't see that his
> summary challenges the traditional view that traditional mathematics
> can, in principle, be reduced down to FOL formulas according to the ZFC
> sets definition, which is based on the general FOL specification.
> Mendelson says this:
>
> ZF is now the most popular form of axiomatic set theory: most of the
> modern research in set theory on
> independence and consistency proofs has been carried out with ZF sets.
>
> That sentence implies the typical "in principle" idea, that everything
> based on ZF can be reduced down to FOL formulas using only the logical
> symbols and non-logical symbols initially given to ZF sets, per the FOL
> specification.
>
> I explain some of my motivation below about why I care about this. My
> main practical concern is that mathematicians are perpetuating this idea
> that ZFC, as traditionally specified, is a complete language, with the
> result that people reject other mathematical languages, in particular,
> languages implemented in proof assistants. I only care to have some ammo
> for the challenge "It's different. It's not exactly ZFC sets. I reject it."
>
> On the other hand, I would be more than happy to know that I'm wrong,
> but the wiki link you provided is giving me the idea I'm right. However,
> it doesn't provide a quote from anyone with authoritative credentials
> that I can use for emphatic, authoritative ammo.
>
> Here's a quote from Thomas Jech's advanced set theory book ,"Set Theory,
> The Third Millennium Edition, revised and expanded".
>
> Page 4, Section "Language of Set Theory, Formulas",
>
> The Axiom Schema of Separation as formulated above uses the vague notion
> of a property.
> To give the axioms a precise form, we develop axiomatic set theory in
> the framework of the first
> order predicate calculus. Apart from the equality predicate =, the
> language of set theory consists
> of the binary predicate ∈, the membership relation.
>
> and page 5.
>
> In practice, we shall use in formulas other symbols, namely defined
> predicates, operations, and
> constants, and even use formulas informally; but it will be tacitly
> understood that each such formula
> can be written in a form that only involves ∈ and = as nonlogical symbols.
>
> Jech's two set theory books are authoritative, classic set theory texts,
> but I'm getting bolder here, and I say it's nonsense when these
> mathematicians say that, in principle, mathematics based on ZFC sets can
> be reduced down to FOL formulas that meet the definition of Axiomatic
> Set Theory as exactly specified and locked in per the general FOL
> specification.
>
> The FOL specification is flexible, but I can see from the three
> definitions that I referenced, that once you lock in a FOL language,
> such as ZFC sets, you don't have the freedom to do anything other that
> what your specific FOL language allows you to do. As to extending one
> FOL language with another FOL language, that's a different subject,
> though related.
>
> Of course, in reality, ZFC sets isn't locked in as they describe, or we
> wouldn't be able to use it. We have to have set constants to use for
> those sets which are proved to exist and which are unique.
>
> Again, I've learned I'm usually wrong on a particular topic when I start
> thinking that professors and authors with PhDs in mathematics are wrong,
> especially when I start to challenge a long established result. However,
> the FOL specification as given by the three definitions I listed isn't
> mathematical rocket science.
>
> Here's the wiki counterpart to your link along with a typical "in
> principle" quote:
>
> http://en.wikipedia.org/wiki/Set_theory
> Set theory as a foundation for mathematical analysis, topology, abstract
> algebra, and discrete
> mathematics is likewise uncontroversial; mathematicians accept that (in
> principle) theorems in
> these areas can be derived from the relevant definitions and the axioms
> of set theory.
>
> This will be an uphill battle to get people to acknowledge that ZFC
> sets, as specified, locks it in as an FOL language, with no constants,
> and it's 9 or so locked in axioms or axiom schemas. And because it is
> locked in, it has to almost immediately start being replaced with
> "extensions". I don't say that based on an authoritative understanding
> of logic. I say that based on my assumption that the standard FOL
> specification means what it says.
>
> Do we get to start with a definition, and then get to discard parts of
> it because its too restrictive, and then get to tell everyone that we're
> meeting the requirements of the definition, to give the impression that
> our mathematical foundation is simple and elegant?
>
> I don't think saying this three times is too many times: I'm happy to be
> shown I'm wrong when it comes to logic. I'm always happy to learn
> something which bumps up my level of knowledge.
>
> Here's been my basic question:
>
> What really is the traditional language of mathematics?
>
> If Jech says that the traditional language of mathematics can be
> completely reduced down to the FOL language of axiomatic ZFC sets, who
> am I to challenge the staus quo?
>
> Okay, all I'm doing is trying to collect a little ammo for a future
> conversation that will go something like this (in principle, of course):
>
> Somebody: Uh, this math you're doing in a proof assistant is different.
> It's not exactly
> the same as ZFC sets, and ZFC sets rules the world, as you should know.
> I give your stuff the big reject.
>
> Me: Of course it's not exactly the same. It can't be exactly the same.
> ZFC sets, as
> specified in the many axiomatic set theory books, is not a complete
> language.
> I love the mathematics that starts with the ZFC set definition, but ZFC
> sets, as
> specified, can't be a final solution for a logical foundation.
>
> Last year, I pretty much fit in the "Somebody" category above.
>
> You give the reference to Mendelson, and I definitely have a more
> in-depth study of FOL on my agenda, but I only need a basic
> understanding of the FOL specification, which I gave with the 3
> definitions from Bilaniuk, to understand that ZFC sets, as specified, is
> not a complete language, and cannot be a final solution for a logical
> foundation. That it's not is not a big, logical deal, as described by
> the wiki page you gave me, which I accept naively, and which supports
> the naive ideas I currently have about all this.
>
> As to proof assistants, the question, "What is the language of
> mathematics?", becomes a mute point, and my understanding of logic has
> no bearing on the logic foundation of a proof assistant. I'm not the
> developer. I'm only a user.
>
> It's not a case of where I obtain theoretical knowledge and then conform
> a proof assistant to my theory. No, it's a case of me finding a proof
> assistant, and then deciding whether the logical foundation of the proof
> assistant is acceptable. The only thing to discuss is how the language
> and logic of the proof assistant compares to the traditional development
> of logic and set theory.
>
> For proof assistants, "What is the language of mathematics?" is a simple
> question.
>
> If I choose Mizar, then the language of mathematics is the syntax and
> semantics of Mizar.
>
> If I choose HOL4, then the language of mathematics is the syntax and
> semantics of HOL4, where the possibility exists for me to extend it with
> axioms.
>
> If I choose the proof assistant "Whatever", then the language of
> mathematics is the syntax and semantics of "Whatever".
>
> Thanks for the comment and the link. Wikipedia is great when it comes to
> mathematics.
>
> What? Most the mathematicians that specialize in logic and set theory
> are too proud to admit that something like what's described in
> http://en.wikipedia.org/wiki/Extension_by_definitions is really what the
> traditional language of mathematics is. That's what I think. Practically
> speaking, it makes no difference, other than you don't get to say, "The
> foundation of our language is really simple, which makes it really elegant."
>
> Myself, I try to stay humble. It's hard, but not having the best of
> credentials is of great help in trying to do that.
>
> A fourth time: I don't care if what I wrote above makes all sorts of
> bogus assertions. I only care to know whether I'm right or wrong about
> this FOL specification thing, about whether it locks in a language once
> the language is defined per the FOL specification. Obviously it does,
> but it would be nice to have someone with the right credentials to
> confirm what I'm saying, or tell me that I'm wrong, which I wouldn't
> accept unless they gave me a constant for the empty set using only the
> symbols given to ZF sets by its initial definition, not the symbols from
> some extension of ZF.
>
> Regards,
> GB
>
>>
>> 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
>>>
>
>
> ------------------------------------------------------------------------------
> 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