Re: Skolem's Paradox and why is math the way it is?

From: J.E. (troubled6man_at_yahoo.com)
Date: 11/17/04 

Date: 17 Nov 2004 12:06:28 -0800

kramsay@aol.com (KRamsay) wrote in message news:<20041114225937.10298.00000039@mb-m25.aol.com>...
> In article <39d6e584.0411050909.504582a3@posting.google.com>,
> troubled6man@yahoo.com (J.E.) writes:
> |kramsay@aol.com (KRamsay) wrote in message
> |news:<20041104185237.21658.00000013@mb-m14.aol.com>...
> |> In article <39d6e584.0410301037.7c9b415@posting.google.com>,
> |> troubled6man@yahoo.com (J.E.) writes:

[snip: I think I understand that now, thank you.]

> | I think it's just that the
> |teachers I had before weren't clear, it seems like something has to
> |come first.
>
> It can be difficult to be clear without being philosophically
> heavy-handed. This happens when people teach quantum mechanics
> in a similar way. One has these several different "interpretations".
> One could pick one and teach as if it were so, which can be somewhat
> misleading. On the other hand, one could try to teach the various
> interpretations along with the more essential material, which could
> make it confusing. An instructor could try to stick to just the
> most essential material-- that part you need to understand to be
> able to compute the probability of observed outcomes.

I think the best way to teach quantum mechanics is to assume that the
wave-function is real (exists), and that the equations describe how it
moves, and that's it, in practise that's all you need and every
interpretation takes that seriously to the extent that the
interpretation takes anything seriously at all.
 
> To be completely "unbiased" and transparent with regard to such
> possible qualms as doubting that the natural numbers really exist
> probably seems like too much of a distraction. So the usual approach
> is basically not to worry about it. The platonist and the formalist
> will tend to sound the same as they are developing a theory, since
> deducing consequences from some assumptions typically sounds just
> like you believe the assumptions to be "actually true" in some
> domain. And then one can divert discussion of qualms to such venues
> as sci.math.

This seems rather ahistorical, the problem is that at one point people
took the existance of "classes" for granted and it created problems.
And "the point" of the modern theory is to avoid those problems, so
you have to be clear that everybody is doing the same thing so that if
someone gets a problem it's clear that the system is to fault, not the
person.
 
> | We can assume induction in the langauge and then latter
> |show there there is an induction INSIDE the theory as well, so that we
> |don't have to use induction outside the theory, but that's very very
> |different than proving induction without proving induction. That's
> |proving induction in a theory using induction outside the theory.
>
> Yes, *if* you assume induction for your original concept of "string",
> it's an informal assumption that can't come from inside the theory.
> Having proven mathematical induction from the axioms, to conclude that
> it applies to actual strings is a further step, requiring either
> believing the axioms are correct in some sense or something like that.

As I mentioned before, the PURPOSE of the formal theory was to avoid
problems, if you actually are depending on the informal theory (I'm
reading Quine now and so far it looks like formulas will be built out
of "philosophical statements" and not strings and that statements of
set theory will be based on other statements, and that the axioms will
likely be about assuming the truth of some statements (which is like
interpreting a schemata), I haven't finished it yet, so don't think
that's how I'm characterizing Quine, it's just my expectation based on
where I am so far and it seems at least not to be circular at this
point.
 
> | Set
> |theory can't do it's own model theory and have every existentionally
> |possible set be in the model,
>
> Note that I only have a vague idea of what "existentionally possible
> set" means. "Existentionally" looks like a cross between "existentially"
> and "extentionally".
>
> I also don't really know what you think "do it's own model theory"
> should mean. I don't consider any particular kind of self-application
> ("do your own model theory", "define your own truth-predicate", and
> the like) to be an important criterion for a theory. I can see how if
> one were looking for a theory to be the be-all and end-all of theories,
> one would need for it to be able to do to itself anything that any
> other theory could do to it. But the quest for the be-all and end-all
> of theories seems a bit quixotic. One surely would need to quit
> focussing on particular formal theories to serve as the be-all and
> end-all, and look instead at such things as the process by which we
> develop theories, and try to find the ultimate theory-development
> process.

Set theory was billed to me as the type-free be-all theory, and I'm
not sure if you are refuting that as a misrepresentation that my
teachers made or if yoy are agreeing with them, I can't tell. But IF
logic avoids having infinite regresses into higher-order logics so
that we CAN sit down and discuss how you make theories, so isn't that
worth considering? Consistent theories imply strategies. That's a
REAL implication. But people complain against IF-logic exactly
because it's the right size to do that because it isn't "the right
size" for NOT doing that (not the right size for formal deduction).
And that's silly because IF-logic has ordinary FOL as a part of it
anyway, so anything you do with oFOL you can do with IF-logic, just
stop using the / or // symbols.
 
> For theories with more realistic goals, I would say self-application
> is a bit like being able to lift all the rocks that one can make.
> It could be a sign that one is strong. Or it could be a sign that one
> has a limited ability to make rocks. IF logic can define its own
> truth-predicate, yes. But that's a combination of being strong in some
> ways, and being weak in others.

In what way do you think it is weak?
 
> | but that doesn't mean there isn't a
> |strong theory that *can* do it's own model theory that has set theory
> |(and hence everything based on it) as a component. That's what I'm
> |looking for now, and I think the excluded middle is the only thing in
> |the way really. There is a subsection of the universe where the
> |excluded middle holds, and that's what we call set theory, but it's
> |intended models (if it has any) live outside that subsection.
>
> Why?

Every model of set theory lacks a set that should exist as much as the
alleged "uncounted real" should exist. The proof depends on the
excluded middle, that every set A either has to belong to a set B or
not belong to B. That assumption has no basis real except for
mantaining an excluded middle. You could still have SOME sets with
that property (that everything is either in them or not in them), but
they simply wouldn't be "all sets". And if your goal is to have every
set that should be, then it looks like you have to have those
nonexclusive sets too because any axiomatic way to carve them out
takes other (normal) sets with it.

> I mean, I have no big problem with abandoning LEM. Perhaps it's a
> bit of a big step to propose that it be abandoned generally... but
> constructive mathematics proceeds without making any blanket
> assumption of LEM.
>
> It is consistent to assume that there exists a function from some
> subset of the integers onto the reals, e.g. the function taking the
> indices of Turing machines that compute real numbers to the real
> numbers that they compute. (Compute is in the sense of computing
> rational approximations to them.) Perhaps something of that nature
> would be more agreeable to you. It still doesn't mean that the reals
> are countable, however.

And once you extend the definition of set to have non-excluded
middles, the standard proof about the lack of a set with a specific
property goes away, the theorem becomes "the graph of the bijection
between a set and it's power set does not have an excluded middle,
even if it exists". And yes we can make a hierarchy based on
equivalnce classes of sets based on graphs with excluded middles,
it'll be just like cardinality theory if we do it right.

> |The math classes I took assumed that for every sentance T(x) such that
> |for every set X such that for all x (x in X) => ((T(x) is true ) or
> |(T(x) is false)) there exists a set Y such that for all y (y in Y) <=>
> |((x in X) and T(x)), where set and sentance were both undefined", then
> |the standard interpretation of set and sentance were "assumed" outside
> |the theory, but maybe the set part is fine, but they should have been
> |more honest about what was a valid sentance, some professors actually
> |wrote "the sky is blue" as an example sentance, with the proviso that
> |it is true.
>
> Well, you do realize that a lot of people consider it rather artificial
> to go around talking about "what is true inside the theory" and "what
> is true outside the theory" as if they were two very different spheres
> of discourse? It just sounds like a course being taught as if
> a standard realist point of view were valid.
>
> I don't see any problem with sets of natural numbers such as
>
> {n : there exists an Oscar award winner who has had n divorces}.
>
> To the extent that the sky being blue or actually being divorced have
> some degree of grey area, these may be somewhat fuzzily defined. But
> it's only when you decide to formalize the theory that you need to
> specify what kind of formulas are allowed.
>
> The problem only comes in when you want to formalize the axioms. If
> your instructor stated the selection axiom as above without noting
> that it's an axiom schema, and that the axioms generated by the
> schema can only have T(x) that is expressible in the language, then
> they've made a rather technical inaccuracy in the presentation. But
> if for some specific formula T(x) the above is an axiom in the language
> of ZFC, it obviously must be a T expressible in the language of ZFC.

I can grant that no deception was intended if you think it was just a
technical inaccuracy, I'm a bit scarred (as in maimed, not as in
afraid) in that I still do not know the order in which to resolve
things, but I'm still hoping this book of Quine's I'm reading will get
everything in the right order.
 
> Judging by the kinds of questions people ask on sci.math, imposing
> this kind of technical detail right away tends to be confusing to
> many students. Moreover, the informal assumption that this axiom
> continues to be true for any predicate is the more basic assumption
> than the axiom schema is.

Students should study a finitely axiomized version of ZFC first (IMO)
with clearly stated and defined terms of language (there's only a few
formulas in this baby-set-theory) and satisfaction and everything, and
then later you bring in the whole schemata, but why not take the
IF-logic first order translation of the negation of a second order
axiom, specifically the IF-logic first order translation of:

EF ~ (Ax Ey Az (zey) <-> (zex and 0=F[z]))

Then to say "T is a theorem" you can state that "it is true that
either the above true, or the some other axiom is false, or T is
true". I don't know why we need informal sentances or metalanguages
or schema at all. Just If-logic first order sentances, and assertions
(hypotheticals) that the universe of discourse is such as to make some
sentances false (like the f.o. translation of "EF ~ (Ax Ey Az (zey)
<-> (zex and 0=F[z]))").
 
> | But this sneaks a truth predicate into set theory that
> |isn't supposed to be there, and I know they were smart enough to know
> |better, so I'm left to conclude that they did it on purpose.
>
> You're a mighty suspicious guy.
>
> Including the phrase "is true", as you have it above, is often just
> a kind of verbal flourish. If someone defines "A or B" to mean "either
> A is true or B is true", that does not mean that they're intending to
> define "or" in terms of a truth-predicate. Failing to restrict to
> formulas in the language of ZF is a matter of allowing set theoretical
> language to intermix with ordinary language.

I am totally familiar with how to translate "either A is true or B is
true" into "(A or B) is true" by using ordinary language, I could even
evalute (A or ~A) as being "true in the case that there is no excluded
middle" without someone saying "A is true" or "A is false" to me, I
know that excluded middle is assumed to mean that one of those holds
regardless of what A is AND that "~A" is true when "A is false" is
true. I don't think this is about colloquialism. I think this is
about describing separation badly, I don't think it's about logic or
language at all, so is "EF ~ (Ax Ey Az (zey) <-> (zex and 0=F[z]))" a
good descrpition of what is intended by separation or not? I still
don't know.

> Don't confuse smartness with being sufficiently persnickety to avoid
> making technical slips on the order of the things you're describing
> here, or caring a lot about them. I realize that to you, the fact that
> the axiom schema in ZFC only guarantees selection for formulas in ZFC
> seems very important, but that's because of the kind of concern you
> have for explaining to yourself how models of ZFC can manage to be
> countable and things of that kind.

Smartness is related to knowing things, if someone asks if you're sure
and you say you are sure when in fact you are wrong, then either (1)
you were dishonest when you replied "yes I'm sure" or (2) you are not
a master of your material because you WERE sure and yet you were
wrong. Does that make sense yet? I tend to assume (1) because if I
assume (2) to everyone who makes an error then I have to reinvent
absolutely everything myself, and force everyone to use *my*
definitions and so on, which is socially too akword. Honestly, people
can be un-persnickety "in general", but to persist when someone asks
if you are sure is what makes people be capable of calling you
dishonest, especially when later conversations reveal that not only do
you know it was wrong, but if you claim you knew better at the time.
I agree that it could still just be a slip of the tongue, and a
mistake, but how many books and how many teachers before this
persistant slip seems to be a concerted case of either (1) or (2).
 
> NB: the technical error here is ONLY an issue if the instructor in
> question was stating the selection axiom schema this way *as a part
> of ZFC*. If they're just stating it as an axiom, then they're just
> giving an informal axiom.

The only thing the instructor talk about was ZFC, he never mentioned
schemas or formulas, he said "sentance" and he gave "the sky is blue"
as an example and he assumed truth and falseness of the sentance T(x)
for every x in a set X. And he said this was set theory, not
we-haven't-gotten-to-set-theory-yet.
 
> | And I
> |shouldn't have to wait for weeks to get a book that defines formulas
> |without assuming set theory first, it's a bit sad that so many people
> |do this in a non-rigorous way.
>
> Don't confuse rigor with formality. Only a formalist needs to have
> "formula" defined *inside* of a formal theory separately from outside.

I'm unfamiliar with your definitions of "realist", "formalist" and so
on, it just wasn't covered in my education. Some people on this
Usenet group have told me to take a set theory class, I have, they
didn't cover those terms. Are they covered inmost classes and was I
just unlucky?

I'm fine with IF-logic saying that some string represent well-defined
games and that some games have winning strategies for one side, and
some for the other, and some don't. I'm find with someone making a
claim that the set theoretical universe is such as to make the string
(~A1)or(~A2)or...(~An)or(T) true (when fleshed out with the right
axioms for A1 through An and the theorem for T, and if they say that
it's true for all theorems, then that just leads to the question "what
are the theorems", but that isn't confusing because we are forever
talking about actual games and these questions are about what elements
can be selected for substitution in the games and which atomic
sentances AeB are going to be true, and which are going to be false.
It's forever a discussion about the rules of the game, no infinite
regress into types.

This is FINE for physics because in physics we ALSO play verification
and falsification games in the laboratory, so I can make them match
up, and we make the SAME kinds of satements about the universe. "The
universe is such that when I do this experiment I get this kind of
results," and one can make DIFFERENT models to help CHOOSE new things
to TEST (in both math and physics). And based on the results, you
might decide to change the rules of the game (new axioms), or just
make new definitions to make existing questions easier (for people) to
ask, verify, or falsify.
 
> |Then there is the whole colloquialness of truth, theorem, theory,
> |model, proof, that people use. I don't think they were trying to be
> |dishonest there, but it's very very very difficult for students to
> |learn when people are using the words different ways.
>
> The responsibility for making an author-reader or teacher-student
> relationship work is a shared one. I don't think your teachers or
> the authors of the books you've read have failed you to the degree
> you're suggesting. Most students, although they may have some
> difficulties, tend not to get so hung up on the particular issues
> that you've described. I don't think you need to have regarded it
> as such an impediment.

The physics classes I've taken I can teach myself, why is math so into
hiding things? I couldn't honestly teach set theory today, even a
basic one, because I haven't seen a logical presentation. My physics
teachers would answer questions when the students got together and
demanded resolution (like when we asked to know how you know when to
treat a stick as single object versus each molecule like a separate
object, versus each atom as an object versus electrons and nucleuses
versus electons and quarks and gluons), and they did so in
non-circular ways. But the math proffessors just say "why are you so
interested in foundations, I thought you liked physics?", I'm just
simply tired of being discriminated with, I'm certain that they talk
not in circles amongst themselves, and I think it's down right rude to
hide the actual logical developement from people just for not being
"in the club", this isn't middle school this is science. I consider
math to be science.

One of the differences is that as a physicists I'm rewarded and
respected for being skeptical of everything, my work, the owrk of
others, results I see, etc., but in math that's praised until you ask
about ZFC, and then it's like "surely you don't doubt ZFC", but how
can I either doubt or trust it if no one tells me what it is?
 
> |> Mathematicians seem generally, even the ones who are not formalists,
> |> to treat the job of deducing consequences from axioms as playing a
> |> special role in doing mathematics. It is supposed to be what we can
> |> all agree on. I certainly hope that there is no circularity in your
> |> set theory books in that part! Your set theory books should contain
> |> many theorems that follow definitely from one of the usual sets of
> |> axioms for set theory.
> |
> |If the axioms aren't described clearly enough, it's not much an
> |exercise in anything.
>
> Clearly enough for *what*? I don't think you can name any exercise
> where you are asked to prove a result, and where the reason why it
> is difficult for you to complete the exercise is that it wasn't
> clear enough what the axioms were.

There is the translation from English to set theory and back
constantly, there is no way for me to tell that I'm doing it the same
way. The point is that someone can say "X is a theorem: Y, QED" but
if you don't know WHAT it is a thoerem of, then I can't turn around to
the guy next to me and say "X is a theorem" because if I'm asked
"theorem of what" then I can't answer, so the "theoremhood" of the
statement isn't really proven (I can't carry it around with me or
apply it outside of the set theory class), it was only stated as a
theorem of SOMETHING. Only after we know the axioms can we know that
X is IN FACT a theorem of THAT axiom system.

> [...]
> |Lost you on the definitions again. Is a theorem a truth of all models
> |or a provable statement of a language (assuming a fixed standard of
> |proof)?
>
> If a system of axioms is a formal system, then "theorem" means a well-
> formed formula that follows from the axioms by the rules of the system.
> If we simply give a set of statements as axioms, the theorems are the
> statements that logically follow from the axioms. If the language of
> a system is understood as being statements about a (variable) model,
> then this becomes "true in all models", since in that case, for a
> statement to follow logically from a collection of other statements
> simply means that it holds for all models in which the premises do.

With you so far then.
 
> I had in mind the common situation where one has a first-order theory.
> In that case, we have the Goedel completeness theorem that says the
> logical consequences of a set of axioms are the same as the consequences
> that can be deduced using standard first-order logic.

Are you sure about how you stated that? I'm assuming "standard
first-order logic" is ordinary first order logic (so not IF-logic or
SOL), but with IF-logic you can make first order statements that
aren't statements of ordinary first order logic, so you claim seems,
... a bit sensational. If it's true, then that's great, but I want to
know if that's what you meant.
 
> |If the latter, then what does it MEAN to be "interested in
> |whether a theorem follows from the axioms", since they all do?
>
> What I should have written was "whether a statement follows from
> the axioms", or "whether a statement is a theorem".
>
> In any case, those of us who are not formalists seldom care whether
> the Riemann hypothesis is a theorem of ZFC or PA or whatever, or
> whether the twin prime conjecture is a theorem of ZFC. We do care
> about whether they're true, however. The formalist thinks somehow
> that these questions are not well enough defined, but everybody
> else aside from Essenin Volpin as far as I know disagrees.

You totally lost me here, people care about whether a statement "is
true" when it's true in some models and false in others? Just
consider the models where it's true, now it's true. Or consider the
ones where it's false, now it's false. Why would anyone care about
this? Am I therefore a formalist to find this silly?
 
> [...]
> |The dependancy was in defining the axioms. What I think you call
> |formal (what I'm used to called pure,a s opposed to applied)
> |mathematics is about propositional relations, like x is a y, where you
> |don't say (or know) what x is or y is or even "is a" is or means, and
> |the statement "x is a y" is obviously netihre true or false, it's
> |meaningless. But what you do is assume that certain relations BETWEEN
> |propositional relations hold, like "for all x, for all y, (x is a y)
> |or (y is a x)", then you can consider what other propositional
> |relations must ALSO hold that hold INDEPENDANT of any meaning ascribed
> |to x, y, or "is a". Then later if a model exists, that means someone
> |can make an interpretation where the x's, y's, and "is a"
> |propositional relations are interpreted to be mean something, and the
> |model is faithful is the axioms (as propositional relations) hold true
> |in the model (as meaningful statements), and a theorem of the axiom
> |system is a statement in the language of the thoery that is true in
> |all faithful models of the axioms. That's how it works for group
> |theory,
>
> I don't think so.
>
> I just went over to my bookshelf and opened a group theory
> textbook at a random page. The theorem there was that the center
> of the group GL(n,F) consists of the set of diagonal matrices.
> GL(n,F) consists of the invertible n by n matrices with entries
> in the field F.
>
> What are the axioms that supposedly define GL(n,F)? We all know
> what natural numbers are, and what invertible n by n matricies
> are, but not because there are "axioms" for them. An n by n
> matrix is a function from {1,2,...,n}x{1,2,...,n} to F; invertibility
> means that there exists another such one that is its inverse, etc.
>
> The starting point is arithmetic, i.e., knowing what it means
> to have a natural number n. What complete axiomatization of
> arithmetic do you have in mind when doing group theory?

I'm really confused, I took this course called "abstract algebra" and
we didn't assume any axiomatization of arithmetic, if fact the "whole
point" was to avoid that, but instead to axiomize a "group" so that
later anything that was a group would have the group theory theorems
true of it. The group GL(n,F) satisfies the group axiom with the
multiplication that you would expect for it (any in fact since F
satisfies the field axioms by hypothesis, you can prove that GL(n,F)
is a group, which is GOOD because that makes the "nomen" group
well-definedish with the fact that GL(n,F) satisifes the group axioms,
the whole point is that the results we proved about the center of
abstract groups can then be applied to the subcase of groups GL(n,F).
Why you think this starts with arithmetic is comletely behind me, you
have an abstract field F, and from it you make a group GL(n,F), where
does arthemetic come in?
 
> | field theory,
>
> I don't really have a book just on field theory as far as I know,
> but it occurs to me that one field being algebraic over another
> isn't first-order definable. The property of a field extension,
> that the overfield is a *finite* dimensional vector space over
> the subfield, comes up often. The finiteness intended is what we
> (foolishly?) understood as just plain finiteness, not "finiteness
> relative to a model of [something]".

The common axiomization of "field" include the term "set", hence the
importance of the question "what is a set". If you threw in "F is a
field iff (FA1, and FA2, ... FAn, and STA1, STA2, ... , and STAn)"
(where FAk is a field axiom and STAk is a set theory axioms) then
you'd know what the models of fields are, but without, you have to beg
the question over to set theory and ask "is this a set" to know if
something is a model of the field axioms.
 
> | geometry, etc.
>
> How many colors are needed to color the points inside a unit
> square, so that no two points of the same color are a distance
> of 1/2 apart?
>
> When people doing Euclidean geometry talk about the Euclidean
> plane, they are talking about the one that's isometric to R^2,
> pairs of real numbers, not an arbitrary model of some first-order
> axiomatization of it.

Classical geometry is both complete (every statement with the
uninterpreted primatives or geometry is either a theorem or the
negation of a theorem) and categorical (all models are isomorphic) as
an axiomatic theory, so what is arbitrary about it's models? And
geometry doesn't have a primative "color". You've lost me completely
again. Isn't that really a question about functions from manifolds
into integers?
 
> Generally, your statement comes much closer to correct if we
> are considering relationships between second-order statements.
> But there's no formal deductive system for second-order statements
> that captures all the valid deductions that can be made in
> second-order logic. Second-order logic also involves referring
> to arbitrary subsets of the domain, which is the usual bugaboo
> of set theory.

Formal deductive methods don't work for set theory correct, but they
do for geometry I don't know why you think they don't. I don't know
why you keep bringing up formal deduction anyway, we don't use
deduction to design theories, so what is this prima facie reason for
such a hubbub about it? Work at finding the valid deductions in SOL
or IF-logic if you care about set theory, use formal deduction if you
care about geometry. How does this relate to anything we are talking
about?

And if someone is concerned about arbitrary subsets, don't quantify
over them, just stick to the IF-f.o. translations all the time, and
then it becomes a question of models and strategies the way it ALWASY
is. You don't have to consider arbitrary subsets, just strategies of
games based on formulas, and the ZFC games are the ones that start a
particular way, and the theorems are the one where you win regardless
of the model (because either the model fails to satisfy the axioms, or
you satisfy the statement of the theorem).

> [...]
> |> A formalist considers everything above the bottom line to be just a
> |> kind of rhetorical flourish. A Platonist will tend to regard the formal
> |> side as being just another technique for refining informal reasoning.
> |> Not many mathematicians are very much interested in either refining
> |> our explanation of what the undefined terms like "set" mean, or justifying
> |> the truth of the axioms in those terms, however. Whether a given
> |> mathematician believes the axiom of choice tends to be treated as a
> |> matter of personal belief.
> |
> |That's VERY annoying. I took a class in functional analysis where the
> |professor actually changed whether the axiom of choice was true
> |halfway through the semester, I basically had to go redo everything.
>
> That's a great story, and I agree that that's annoying, at least if
> he did it in a way that forced the class to redo work. If he had
> meant to do this, he should at least have started with the neutral
> theorems (ones not needing choice) and then added the additional ones
> that can be proven with choice.
>
> But whether to believe the axiom of choice is "really" true or not has
> no necessary connection with whether someone works using it or not. One
> formalist who doesn't believe that 10^n exists for each natural number
> n has proven results in set theory using all the usual "highfalutin'"
> assumptions.

The PROBLEM is using ONE word "set" when people ARBITRARILY CHOOSE to
have the word essentially MEAN different things, it's bad bad bad. If
the word "electron" meant something different depending on who said
it, physics would get nowhere fast. I agree that someone could write
out a proof (so could a Turing machine) without believing the theorem
to be true (so could a Turing machine), but if we are going to use the
word "set" it should mean something, not whatever the speaker imagines
in his head, that's one of my biggest problems, I'm trying to get a
straight answer about what is and is not a set, and I'm not getting
one.
 
> |Hintikka gives a justification about why mathematicians like the axiom
> |of choice because it translates the standard interpretation second
> |order formulas into equivalent first order formulas, but then he shows
> |that that doesn't work in general.
>
> Mathematicians do tend to like instances of quantifier-elimination,
> even when they are unaware of the concept of "quantifier-elimination".

I'm not sure how that's a response to my statement, there is NO model
of set theory where all such translations are valid. That's what the
proof-predicate at the first-order level shows. And if you start
dancind around the issue by taking a non-standard interpretation of
SOL, that's just silly to then insist on a standard interpretation of
ordinary FOL theories. Something seems to have to give here.

> | I think that's because he was
> |holding onto an "excluded middle" for atomic sentances when he didn't
> |need to, but that's his problem, there is no reason I can't assume no
> |excluded middle.
>
> Some properties of structures seem simply to be second-order and
> not first-order. Whether a graph is connected or not, for example.
> I don't see how one can get around it.
>
> Keith Ramsay

Set theory is "supposed" to be type free, e.g. you have a set of
points AND a set of edges AND they are both sets, everything is a set.
 So let A be the set of points and let B be a the set of unordered
pairs of elements of A such that {a,b}eB iff there is an edge between
a and b. Now let f: N->P(A) be a function such that f(0) = B, and
such that f(n+1)={CeP(A):ExEyEz (yeS(n)) & (zeS(n)) & (xey) & (xez) &
C=U({y,z})}, then the finite graph A is connected iff En Aef(n),
that's all f.o. set theory. If you had an infinite graph, then you'd
need a better definition of course, but I'd have to know what the
exact definition of "connected" is to get an iff going, for instance
"A is disconnected iff ErEs An ~ Et (tef(n)) & (ret) & (set)" might be
correct, I don't know. I think it's obvious that I'm failing to get
your point though, sorry.