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
<gottfried.bar...@gmx.com> 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-info@lists.sourceforge.net
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-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
