On 9/7/2012 3:01 PM, Josef Urban wrote:
I think this may belong more to the FOM list.
Josef,
I think you might be right. I went over to look at the archives, and the
contributions look pretty interesting. I saw some posts on 2nd order logic.
But I ended up at a web site I had gotten a free book off of in the
past, which is Simpson's "Foundations of Mathematics":
http://www.math.psu.edu/simpson/notes/
What's making me paranoid is Drake's phrase "almost impossible".
So I'm looking at Simpon's FOM page 93, and he's introducing
abbreviations rather than using a conservative extension. For example,
he says:
/"x = 0 and x = { } are abbreviations for \<forall>u (u \<notin> x)."/
Then he states the empty set axiom:
/"2. Empty Set Axiom: \<exists> x ( x = 0 )."/
And so that simple substitution works out, and doesn't violate the rules
for forming FOL formulas.
I look for the first place in which he uses the empty set, 0, with the
membership predicate. For his Axiomatic Set Theory chapter, there's page
92, 93, 94, and then on page 95, at the top, there's finally a formula
in which he uses 0 on the left-hand side of the membership predicate. If
I can sort through the layers of substitutions, then I'm home free.
There are only three pages, but I can't find an abbreviation for the
formula "0 \<in> z" that's used in the big formula. These are the kind
of things I know:
1) He's said nothing about extentions.
2) He says "We can expand the Language L_e indefinitely by introducing
abbreviations.
3) You can't use a constant that's not in the language.
4) Predicates only take constants or variables.
5) In 3 pages, the only place I've seen 0 defined is in an abbreviation
using the formula "x = 0".
If I could wander the halls of the Penn State mathematics department,
I'd be dropping by his office, student or not.
Surely this is simple stuff. Well, other than the ridiculous amount of
convolution that occurs due to using substitutions rather than an extension.
I have to sort through 15 substitution definitions to figure out how "0
\<in> z" actually ends up being used in a substitution, or nested
substitutions, to generate a legitimate formula, because 0 as a constant
is not in the language.
I'm back to the possibility that these set theorists with PhDs really
have worked out a huge convoluted mess that requires no constants in the
language.
Thanks for the FOM suggestion. I may end up submitting a question:
"Please, using Simpson's FOM book, can you give me the FOL formula for
(0 \<in> 0), and how your derived it?"
This is the end of this thread for me, but the conservative extension
references are a good find, regardless how the substitution stuff works.
I assume it'll work.
I have a conjunction in the scope of an existential quantifier, but I
can't find the pattern, and I notice that the abbreviation for a
function is so long it's not fit for human consumption.
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
