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

[Josef U. <jos...@gm...>]

Hi Gottfried,

I think this may belong more to the FOM list.

In short, I think people are OK with viewing a theory and its
definitional extension as "practically" the same thing.

Perhaps one way how to think about this could be to choose the names
of newly defined symbols based on some Goedel numbering [1] of the
defining formulas (and the necessary existence/uniqueness
proofs). That way, the "fully extended" theory (with "all names") is
uniquely determined by the initial theory . And if you wish, you can
then say that you work in the "fully extended" ZFC, and given a
symbol, you can decode it and find out if it is in the "full"
language. And from the "full" language, you can obviously get back to
the "minimal" language by expansion.

I also agree that mathematicians invent (and prove correct) all kinds
of other shortcuts, e.g., new inference rules. And this process is
interesting (also for proof search), and when we fully understand it,
we might have AI :-). But again, as soon as you formulate precisely
(parts of) this process as some (conservative) extension rule, you can
again make the leap and say "now I work in the fully extended system"
(and the appropriate correctness proofs will show that it has the
"same strength" as the original).

Best,
Josef

[1] I once thought of some practical use for this in
http://ceur-ws.org/Vol-767/paper-09.pdf :-)

On Fri, Sep 7, 2012 at 5:13 PM, 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