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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
