Hi,
My last email to the list was actually only email (e - 1) before the
"end of this thread for me", but I do this email because I can end
everything on a completely satisfactory note, give credit where credit
is due, acknowledge that certain claims that people are making are true,
and briefly tie this into proof assistants.
First, though, thanks to Rob for the tips about Mendelson, and again, to
Konrad for the Shoenfield reference.
The way it has worked out is that not only did I get textbook references
for conservative extensions, but Josef's explanation below eliminated a
misconception I had developed, and it specifically answered the question
I asked in the header of this email.
With a conservative extension, I can get, for example, a symbol 0 with
an axiom (!x. ~(x \in 0)) that allows me to use 0 as the empty set. That
led me to think that I'm dependent on my conservative extension when I
do that. But I'm not, where the key point is in the wiki article Josef
references, "...the formula psi^* has the same meaning as psi, but the
new symbol f has been eliminated".
Josef's answer could be called "a constructive answer".
/"Does a formula exist to do it?" /
/"Here you go. Here's a formula." /
/"Alright. I'll take a constructive answer over an existence answer any
day."/
So the professional mathematician tells me that all defined notation can
be replaced so that we end up using only ZF as it's initially defined,
that is, defined with no constant symbols, no function symbols, and only
one non-logical predicate.
I say, "Then please, someone give me a formula for (0 \in 0) to prove to
me that this can be done."
And so Josef gave me (!z. (!u. ~(u \in z)) --> (z \in z)), which would,
if equivalent to (0 \in 0), allow me to prove something like this:
/
/theorem "~(!z. (!u. ~(u \in z)) --> (z \in z))"
I can see now that part of my misunderstanding is that I was trying to
replace 0, rather than replace formulas that use 0, and I didn't see
that all that matters is that the new formula is logically equivalent.
So, it's true what the professional mathematicians are saying, that
every formula used in set theory can be reduced to a form that doesn't
use constants. That is rather amazing. Actually, what's amazing is the
recursive definition on the Wikipedia page.
Now, not wanting to be nice just to be nice, I asked the question, "Yea,
but if I have to resort to a conservative extension to prove that the
substituted formulas are logically equivalent to the formulas they
replace, is the primitive ZF really independent of its conservative
extension?"
I eventually answered, "Yes." The only challenge was, "Give me formulas
to get rid of the constants that you put in your notation." There was
never a limit on the amount of notation that could be introduced. It
could be that notation would have to be defined for every "constant
using" formula". It was never said what reasoning was going to be used
to get these formulas. It was only said, or implied, that it could be
done, and that it would be logically equivalent. If the reduced form is
logically equivalent, then it's logically equivalent. Arguing whether a
person has to formally state what justifies the replacement of the
"notational form" with the "reduced form", I'll just consider that as
arguing.
Partly why I didn't want to continue the thread is because I have a lot
of respect for professional mathematicians, even when I'm thinking
they're doing something wrong, and my respect is tied into the fact that
I've learned in the past that when I think I'm right and they're wrong,
I'm usually wrong. This same respect is there for others with PhDs in
technical subjects. I've learned that the understanding of a person with
a PhD in a technical subject is usually a substantial step above those
with only Bachelors or Masters degrees.
(Small Tangent: Much of what I said still holds about people making ZF
sets out to be a simpler language than what it is. Axiom schemes require
thousands of axioms. Basic keywords are not optional. We have to know
whether a formula is an axiom, theorem, proof, etc. If people don't use
huge FOL formulas for proofs, which they don't, then proof language
keywords in the language do exist, however non-standardized they may be.
Collectively, all that, and more, makes the language based on ZF more
complicated than just a set of FOL symbols.)
*The Potential Use of Conservative Extensions in Proof Assistants*
In a paper of theirs, Paulson and Blanchette say, "...thinking is
difficult...":
http://www4.in.tum.de/~blanchet/iwil2010-sledgehammer.pdf
<http://www4.in.tum.de/%7Eblanchet/iwil2010-sledgehammer.pdf>
It's true. It can be. Sometimes you don't want to think. You want a
calculator.
Breaking down the meaning of a FOL formula requires thinking, so I
plugged this into an ATP:
/theorem "(0 \<in> 0) <-> (!z. (!u. ~(u \in z)) --> (z \in z))"/
The the ATP proved it.
I put this right under my empty set axiom (!x. x \<notin> 0):
/theorem "~(!z. (!u. ~(u \in z)) --> (z \in z))"/
It proved it with the empty set axiom. I said, "How does it know to do
that?" So I had to think, at least a little, and I got this:
/?z. (!u. ~(u \in z)) & ~(z \in z))./
And so I said, "Well, yea, it's the conjunction for a statement
describing (0 \in 0), that the empty set exists and that it's not in
itself."
And I had been saying to myself, "With no constants in the language, how
am I supposed to replace (0 \in 0)? There are no quantifiers in the
formula. Quantifiers can only be used with variables, and all the
variables have to be bound, so a statement like (x \in x) is not a
sentence that can be stated as a theorem."
And so the recursive definition on the wiki page has taken me to next
level of understanding.
This ability to replace all my constants offers possibilities. I said
that it's inescapable that I have to use HOL functions for my constants,
such as 0. That is true, but if I use the recursive definition on the
wiki page to get rid of all my constants, there's no constants requiring
HOL functions. Is that significant? It's very significant.
Okay. My membership predicate is a HOL function constant. I can't get
rid of it. That's okay, as if I have a choice.
It's also occurred to me that I could actually do what the axiom schemes
says and introduce the hundreds of axioms, and then I would only be
quantifying over atomic variables.
If I did all that, then other than that the connectives and quantifiers
are HOL functions, there would only be one HOL function that I
specifically introduced, which would be my membership predicate. Would I
want to do that? It's a thought, and something to keep in mind in case I
hit a dead end. Where saying all of this is premature.
But there's my empty set axiom. I need a calculator to get an equivalent
formula for (x \<notin> 0), to get rid of my constant in the axiom. Of
course when information overload is happening, the most trivial of
things can blow my mind, so after a 30 second "blow my mind period", I
simply replace the empty set axiom that's using a constant, with the
standard empty set axiom that uses quantifiers.
There are possibilities for me to try that weren't there before I
learned the details of extensions by definitions.
Regards,
GB
On 9/8/2012 5:19 AM, Josef Urban wrote:
can you give me the FOL formula for (0 \<in> 0), and how your derived it?"
This is explained in
http://en.wikipedia.org/wiki/Extension_by_definitions#Definition_of_function_symbols
.
The empty set is obtained by proving
?!y: !u : ~(u \in y)
so, to match their notation, \phi is then "!u : ~(u \in y) " and f is then 0.
Then you asked to expand the empty set in an atomic formula \psi: "0 \in 0" .
So just follow their instructions: [...] choose an occurrence of f in \psi,
and let \xi be obtained from \psi be replacing that occurrence by a
new variable z. Then since f occurs in \xi one less time than in \psi, the
formula \xi* has already been defined, and we let \psi^* be "!z:
\phi(z) => \xi^*"
In your case, this is (after two expansions for each 0):
!z1: (!u1 : ~(u1 \in z1)) => (!z: (!u : ~(u \in z)) => (z \in z1))
or in a simplified form:
!z: (!u : ~(u \in z)) => (z \in z)
The conservativity claim is then that T' |- \psi<=> \psi^* .
Josef
------------------------------------------------------------------------------
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
