Re: tedious sledding re set existence in FOL

george wrote:
> MoeBlee wrote:
> > I stated precisely the sense in which I mean that the semantics don't
> > have to be mentioned.
>
> What UTTER bull***.

A precise sense was given in the sentence that followed.

> *I* am the one who has stated the sense in which the semantics
> don't have to be "mentioned"

You stated your sense; I stated another.

> > One can compile an entire tome of proofs without
> > even specifying that there is a semantics for the language.
>
> One can specify some strings but they are NOT "proofs" JUST
> because of the grammar via which they were specified.

If they are members of the set of proofs, then they're proofs. The set
is specified entirely in terms of certain kinds of sequences of
strings.

> That would not be an extrapolation. That would simply be the
> truth. You have insisted 500 times that semantics "need not
> be mentioned". That insistence DOES constitute a denial of importance,
> no extrapolation required.

I said that as to the precise question of the theoremhood of the
formula in question, we are not required to mention semantics. It just
occurred to me: I hope you don't think that by 'need not' I mean we
should not. I simply mean that we are not required. I don't deny any
importance by simply stating that in a certain context, we are not
required to mention something.

> > or that it would be rational to have a semantics that clashes
> > with the proof syntax.
>
> OF COURSE it would be rational.

Why would it be rational?

> The case HAS to be considered.
> ANY semantics can clash with ANY syntax!

Who denies this?

> As you yourself have been
> AT PAINS to (irrelevantly) belabor, ANY old chain of
> string-derivations
> can be CALLED a proof! THAT notion is purely syntactic! There IS A
> REASON
> why some semantic constraints are relevant.

I agree. You're just pounding away on points of agreement.

> AzExAy[phi(x,y,z)] is a theorem but if the domain is empty,
> THERE IS NO z for which
> ExAy[phi(x,y,z)] is true.

You keep pounding on points of agreement.

> > If we check the
> > definition of 'theorem' we will confirm that the formula is a theorem,
>
> ***. WHOSE definition of "theorem"??

Virtually any definition in any textbook on logic.

> SOME people ACKNOWLEDGE the relevance of the standard
> semantics of the logic in deciding what is or isn't a theorem,
> ESPECIALLY when that semantics impacts the whole question
> of the SOUNDness of the inference rules of the logic!
> Do you really think you get to keep using a definition of
> "theorem", LET ALONE of "logic",
> in which the inference rules are known not to be sound??

I wouldn't advise it.

> If you've chosen a semantics under which your inference rules
> are not sound then your claim to STILL BE doing "proofs" or "theorems"
> or even "logic" is NOT going to stand.

I can see your point about 'logic', but not about 'proofs' and
'theorems'. Call them 'deductions' or 'transfomations', or whatever
you want, though.

> > or have chosen
> > no semantics.
>
> If you haven't made a choice then you DAMN well better be in a
> situation
> where the choice CAN'T MATTER.

Okay, but I've already made a choice.

> > It's a proof by virtue of satisfying the requirements given in the
> > definition of 'proof'.
>
> Sound inference rules ARE one of those requirements, DUMBASS.

Then please tell me where I can get a book that has your definition as
opposed to the usual definitions. Or please tell me where I can view
your system of vocabulary.

> In the absence of some assumption (mentioned or not) about
> non-emptiness of the domain, the proof YOU gave of the existence
> of the empty set IS SUCH an incorrectly purported proof.

Not according to any book I can find.

> > But something is either a proof or not a proof.
>
> What UTTER bull***. CONTEXT of interpretation ALWAYS
> matters. And if people are still arguing over the context then
> they can still argue over what's a proof and what isn't.

I did not claim that people can't argue about what a proof is. Just
that given the usual defintions of 'proof', there is no such thing as
an incorrect proof. That is quite different from giving an incorrect
definition of 'proof'.

> > And if something is a proof, then 'correct proof' is redundant.
>
> Again, BULL***. If person A OPINES that something is a proof
> and person B OPINES that it is not, then natural rules of English
> usage DICTATE that BOTH sides are going to KEEP calling it
> a "proof" until the argument is over, even though the mere existence
> of the conversation implies acknowledgment that that terminology
> could be "incorrect". You canNOT get this cut and dried about these
> things IN A CONTEXT WHERE *BASIC* foundational tenets, things
> that NORMALLY CAN'T be debated (like, whether the domain is non-
> empty -- OF COURSE it's non-empty, normally, UNTIL you have
> the temerity to suggest that the empty set might not exist) ARE being
> debated.

Given a precise mathematical defintion of 'proof', there are no
incorrect proofs.

> > However, if the semantics and the proof syntax don't jibe,
>
> Bzzzt. You lose.
> What EXACTLY do you MEAN by "jibe" here??

The soundness theorem fails would be one indication.

> DEFINE "jibe"! It will turn out that WHAT IT MEANS for
> "the semantics and syntax to jibe" will be "for the alleged proof
> to actually BE a proof", i.e., for it to be a CORRECT proof, which will
> entail, amongy MYRIAD OTHER constraints, some usually mentioned,
> far MORE usually NOT, that the inference rules used in the proof
> BE SOUND in the context in which they are being deployed and presented!

Okay. That's noble.

> More to the point, you argue as though The Completeness Theorem had
> never been proved. Once the completeness theorem HAS been proved,
> the world becomes a different place. The completeness theorem implies
> (among other things) that SEMANTICS DOESN'T MATTER, that things that
> are provable/decidable have the same truth-value under ALL relevant
> semanticses. THAT IS SOMETHING THAT PEOPLE *DON'T* want to give up.
> If you start out with some syntactic rules but then broaden your
> semantics
> in such a way that this no longer holds, then it is ENTIRELY reasonable
> to
> say that that broadening has slagged the proof-hood of certain proofs
> or the
> theorem-hood of certain theorems. THAT'S WHAT YOU GET for flying to
> the moon (i.e. for changing the definition of BASIC terms, like "what a
> domain
> is" in the context of first-order logic).

I don't argue as if the completeness theorem had not been proved.

> then I don't disagree
> > that it would be incorrect to say that the proof can be interepreted as
> > demonstrating validity in a semantics in which the proof does not
> > demonstrate validity.
>
> Dip***: THE COMPLETENESS THEOREM HAS BEEN PROVEN.
> THEREFORE, NO proof CAN demonstrate validity "in a semantics"!
> BY DEFINITION, *VALIDITY* IS *UNIVERSALLY* quantified over ALL
> POSSIBLE semanticses! THAT'S WHAT *valid* *MEANS*! It means
> true under ALL semanticses! But your claim about your proof of the
> empty set is NOT true under an empty semantics! THAT proof is RATHER
> a proof IN CLASSICAL FIRST-ORDER LOGIC. You have to SAY WHAT LOGIC
> you are using BEFORE we can argue about what constitutes a proof!

I'm not familiar with that definition of validity. My understanding of
validity is taken from the usual textbooks.

I understand a sentence to be valid if it is true in all models. And I
understand a semantics to be given by specificaion of what a structure
is and, in the case of standard first order semantics, the
specification of a certain function proven to exist by the definition
by recursion theorem. But I don't know what it means for validity to be
quantified over a class of semantics. I am happy to learn about that
notion, though.

> >
> > > > One can specify what a
> > > > proof is without mentioning models.
> > >
> > > of course, but the whole content of the completeness theorem
> > > is that this DOES have implications for models. More to the point,
> > > the proof-scheme YOU're using ISN'T EVEN SOUND when the domain
> > > can be empty.
> >
> > That doesn't contradict anything I've said,
>
> You are SO full of ***. You have said that semantics
> "need not be mentioned"

I said it is not required to mention with regard to certain precise
questions.

> and you have alleged that it is rational
> to keep thinking of your alleged proof of the existence of the empty
> set as a proof of the existence of the empty set EVEN in a context
> where the instantiations it depends on are not sound inference rules.

I think that with the exact mathematical definition of 'proof', it is
possible to have proofs that are unsound with respect to a particular
semantics.

> The issue you were TRYING to investigage was, how do we prove the
> existence of the empty set?

No it wasn't. I knew how to prove ExAy ~yex long before this thread.

> FROM WHAT does the existence of the
> empty set follow?

'Follow' in the sense of theoremhood. It follows from the axioms -
logical and non-logical. And one can also show that it follows as a
sound inference (of course, not allowing the empty domain). There's no
contradiction there.

> My point remains that it DOES NOT follow from
> any proof you have presented.

I'll defer to whatever special sense you have for the word 'follow'
then. Nevertheless, the formula is proven.

> What it DOES follow from is the
> assumption
> that SOME set must exist.

That the inference be sound, yes. But, proof-wise, its derivability
requires only a rule of inference, logical axioms, and one non-logical
axiom. (Or in your system, rules of inference and one non-logical axiom
(or 'axiom' or whatever you want to call it).)

> WITHOUT THAT ASSUMPTION, YOU CANNOT
> prove the existence of the empty set.

I can prove the formula ExAy ~yex. Whether that proves "existence" I
can only leave to your glossary entry for 'prove existence'. I never
claimed it proves existence in a model if we allow the empty domain.
Only that the formula is a theorem.

> The fact that the
> pure-string-inference
> rules still produce what they produce does NOT entitle you to infer
> the existence of an empty set IF the domain MIGHT be empty.

Yes, as to existence in some model. I've never disputed that. I'm just
saying that the formula ExAy ~yex is a theorem, even if we were all
suddenly struck by complete amnesia regarding semantics.

> > nor does it inform me on
> > anything I didn't already know.
>
> Your failure to be informed is due purely to your own stupidity.
> You could've just admitted that you were wrong and I was right.
> THEN you would've been informed.

I would love to do that. But it's not true that I am wrong and you are
right. And as to stipulative definitions, I prefer to navigate with
those in the usual textbooks, unless you can offer an alternative
system of vocabulary that I can study.

> > Which, is what I consider unfortunate.
> > There is so much I could learn from you, instead of this senseless
> > argument. Granted, that's my selfish perspective. I can't speak for
> > your perspective, but as far as I can tell, it seems to be that of
> > demanding your pound of flesh, even when it's not owed to you.
>
> Oh, but it is.

No jury would agree.

> Alleging that something is irrelevant because it "need not be
> mentioned",
> when the reason WHY it is not mentioned is that it is SO INDISPENSABLY
> relevant that people BUILD IT INTO THE BACKground framework, so they
> don't have to KEEP mentioning it, is just plain intellectually
> dishonest.

Quite so. But I didn't post that semantics is irrelevent. Why would I
aspire to work through a 550 page book on the subject if I thought it
were irrelevent? What I said was that as to the precise question of the
provability of the formula, we don't have to consult semantics. Only by
a gigantic non sequitur could you think that I hold that semantics is
irrelevent, as you leave 'irrelevent' unqualified and out of context of
the exact claim I made.

> > > Half these alleged "theorems" with their "proofs" that you are talking
> > > about
> > > ARE FALSE in the empty domain!
> >
> > They're not merely alleged. They are theorems and proofs.
>
> They are proofs UNDER THE ASSUMPTION THAT THE DOMAIN IS
> NON-EMPTY. They are proofs from a set of inference rules that
> ADVERTISES ITSELF AS BEING standard classical first-order logic,
> that ADVERTISES ABOUT ITSELF IN ITS DEFINITION that it DOES
> have semantic import, that it DOES depend, for soundness, on the
> semantic assumption that the domain is non-empty. Despite the
> fact that you chose inference rules that had this pedigree, you alleged
> that their semantic import was irrelevant because it did not "need to
> be mentioned". That is execrable.

It's not execrable, but it is other things that are not good, that you
continue to post that I've made claims that I have not made.

> > And I've always known, since I first read the words 'structure for a language'
>
> Oh, shut up.
> You didn't know what those words meant then and you don't know now.

Yes I do. They're precisely understood.

> > that in this context (since I don't know the details of free logic)
> > existence claims are false in the empty domain.
>
> They CANNOT simultaneously be false under some relevant or important
> semantics AND PROVABLE. THat is what the completeness theorem says
> and IT, TOO, IS PROVABLE. In order for these "proofs" to be sound
> (which MEANS valid, which MEANS holding WITHOUT regard to semantics),
> the empty domain HAS to deprecated as a degenerate case. That act of
> deprecation is MORE relevant to proof of the existence of the empty set
> THAN the axioms you were talking about.

In the overall picture, I very much understand that point. Too bad
you've convinced yourself that what I've said contradicts it. All I
wanted to know, really, was why you feel this is especially important
for the empty set theorem. Or, is it as important (I mean 'important'
in the sense of understanding the big picture or the deep content
rather than 'important' technically) for all other applications of
quantifier instantiation. All I was getting at is why do we vindicate
the empty set theorem with a semantic explanation any more than we
would vindicate any other theorem of set theory (that relies on
instantiation) with semantic explanation? Instead of getting into that
matter, on which I would benefit by your insights, you lit off onto
some bizarre warpath about vocabulary that I even used right in line
with standard texts. I don't get that.

> > Yet you still insist that the ZF axioms "prove" the existence of
> > an empty set. Wow.

Just for the record, in that formatting, that appears to by me quote,
though it's yours.

What I claim is proven is a certain formula. It is proven. I have never
claimed that there is an empty domain in which there exists an empty
set, if that's what you're trying to say I'm claiming.

> Bull***. You have posted that this theorem maintains its theoremhood
> even in the face of its falsehood in the empty domain. I don't know
> what
> you think "existence proof" means.

Did I use the term 'existence proof'? What I have said is that the
formula, which begins with an existential quantifier, is a theorem, and
that the question of its theoremhood is settled by just showing a
proof. I've never claimed that the theoremhood of that formula proves
the existence of something in the non-empty domain.

> > > IN PARTICULAR, ALL SET-EXISTENCE
> > > statements are false in the empty domain, unless you universally
> > > quantify
> > > them (in which case they are NO longer existential in character).
> > > What good is a universal generalization that you CAN'T INSTANTIATE??
> >
> > I can't think of any good.
>
> Bull***. It is still good for proving theorems, ACCORDING TO YOU.
> All of its instances REMAIN THEOREMS, EVEN if there is a context
> in which it can't be instantiated.

But I didn't say that would be good. Not good for me, at least.

> > I don't know why I should be asked the question.
>
> Because you alleged that semantics didn't need to be mentioned,
> THAT'S why.

Cf. about a hundred lines of previous post explainging why it is not
true that I ever made an UNQUALIFIED claim that semantics don't have to
be mentioned. I said semantics don't have to be mentioned to settle a
particular question - theoremhood of a particular formula. Please stop
posting, with omission of my very clear qualifications and context,
that I claimed that semantics is irrelvent

> > I never advocated a semantics that would make the proof
> > theory incompatible with the semantics.
> DIP***: YOU NEVER DISALLOWED the semantics that refuted
> your allegation EITHER!

First, it's not refuted that the formula is a theorem, irrespective of
semantics. Second, I'm not on the semantics correctness squad so that I
have to explicitly disavow this or that semantics. That I showed that
the theorem is provable, no matter the semantics, does not entail that
I propose people start using semantics that would make the theorem
invalid nor does it entail that I have to explicitly warn anyone not to
use semantics that would make the theorem invalid. Unless, I guess,
there were some clear and present danger that some poor unsuspecting
readers would do what they're not supposed to try at home, which is to
tamper with the semantics! How ridiculous.

> IN ORDER to disallow that semantics,
> YOU HAVE to acknowledge the relevance of semantics! There
> are BUNCHES AND BUNCHES of classical proofs-in-ZF of things
> that ARE true in free logics or in the empty domain, or when terms
> don't have to refer totally! Saying about THOSE that "semantics
> doesn't matter" could've been helpful! But saying about a proof
> of the existence of the empty set is just stupidity.

Cf. etc.

> > > > Regardless of whether one MENTIONS the non-emptiness or not,
> > > one DOES in fact have to PRESUME non-emptiness in order to
> > > perform this proof.
> >
> > No, one sets up a proof system such that all derivations are ensured to
> > be valid only if the domain is non-empty.
>
> That is NOT a NO, dumbass! THAT IS A *YES*! *IF* you define
> your inference rules such that they are unsound in some semanticses
> and sound in others, THAT CONSTITUTES alleging that you EXPECT AND
> WANT the semanticses in which they ARE sound to be treated as relevant,
> to be the universe TO WHICH WE RESTRICT our attention, when using
> your inference rules! THAT CONSTITUTES deprecating the semanticses in
> which your rules are UNsound as irrelevant! THAT CONSTITUTES making
> a semantic assumption! And your use of "valid" above is simply
> incorrect.

Cf. etc.

> You MEANT to say "sound". "Valid" applies to the inputs and outputs of
> inference rules, or to conditionals connecting the former to the
> latter.
> It does not apply to rules themselves.

That I can live with. You're right. 'Sound' is better for proofs, and
'valid' for formulas.

> > But just to perform the proof
> > one need not mention nor even presume any semantics whatsoever.
>
> I repeat, BULL***. THAT proof must be performed with THOSE inference
> rules, and THOSE inference rules are UNSOUND over the empty domain.
> THEREFORE, using them in a derivation and CALLING that derivation a
> proof, USING it, pragmatically, in this context, COMMITS you to the
> semantic assumptions EMBODIED IN and MADE BY those rules, and
> existential import in the domain IS ONE of them.

Cf. etc.

> > To choose a semantics that clashes with the proof syntax would be silly,

> That's MY point, dumbass, NOT yours.

It's a point with which I've always agreed. By posting it, I was
granting the senses in which I agree with you about the importance of
semantics. Nor did I claim that it wasn't a point you had already made.
You want full credit? It's yours. You are the Progenitor, the Unmoved
Mover, of all that is Good and Holy in the Blessed Unity of Syntax and
Semantics.

> YOUR point was that semantics
> "need not be mentioned", and THAT point is BULL***.
> We HAPPEN to be using inference rules with the property that
> semanticses for which they are unsound DO EXIST.
> To make this work, to actually guarantee that the existence of
> this derivation CORRESPONDS WITH the actual existence of an actual
> empty set, WE MUST EXCLUDE those semanticses, somehow.
> The fact that that "somehow" is NOT normally "mentioned" has THOROUGHLY
> deceived you.

I don't know about joining up in your campaign to eradicate errant
semantics, but I promise I won't play around with anything but standard
semantics until I see a reason to do otherwise.

> > but the precise question of provability
>
> is something with which you personally are NOT
> philosophically conversant, so KINDLY shut the *** up.

If you insist that it is a philosophical question, in this context. I
had more in mind the mathematical definitions.

> > does not require
>
> In your personal ignorant and irrelevant opinion.
>
> > semantical justificaiton nor presumptions.
>
> But thanks to the completeness theorem, IT HAS THEM ANYWAY,
> required or not. And given that the last 70 years of logic HAVE been
> conducted in AWARENESS of the completeness theorem, OUR
> tastes regarding what WE are going to "require" are a little better
> educated than yours.

Darn, and to think that now I can't be a member of the WE.

> > > Several of its steps are NOT SOUND when the
> > > domain is empty.
> >
> > Again, since I know this well,
>
> Oh, bull***.
> If you had known that the thing you were presenting as a proof
> of the existence of the empty set was based on inference rules
> that were unsound, you would not have presented a proof using
> THOSE rules AS your proof the existence of the empty set.

In context of formal systems, if I didn't know, or at least didn't have
reason to trust, that the inference rule is sound, then it would be
less interesting and meaningful for me to use. But that does not
preclude me from studying a logisitic system of which I do not know
anything about semantics for it.

> There WAS an Original Question here! It was, "how do we know
> the empty set exists? From what does that existence follow?
> What do we NEED to prove that?" You alleged that we needed
> the Axiom of Replacement and I pointed out that that would NOT
> get you an empty set UNLESS you already had some set to
> which to instantiate Replacement, Replacement being a universal
> generalization OVER SETS. Universal generalizations PRESUME
> existence, they DON'T imply it.

Just for the record, it was the axiom schema of separation. And, on a
separate matter, you've completely missed the point of just about
everything I've posted in this thread.

> > your repeating it again and again does
> > not contribute to my knowledge or understanding.
>
> The issue at this point IS NOT your knowledge or understanding.
> It is your repetition of "proofs is proofs", as though nothing else
> mattered.
> You may rest well assured that THAT repetition is not contributing to
> anybody's
> well-being EITHER.

There is no "as if nothing else mattered" to be inferred from my posts.

> > > Instantiation of universal quantifers is not sound
> > > when the domain is empty and instantiation of existential ones is not
> > > even possible.
> >
> > Again...
>
> "Again" my ass. In order for there to be an again, there would have
> to be a first time. But the FIRST time, you thought that proving the
> existence of the empty set (or of any set at all, for that matter) was
> something
> that was WITHIN the power of ZF.

FOL with an instance of the axiom schema of separation proves the
formula ExAy ~yex. As to existence in a model, I never claimed that one
can prove existence in a model if the domain is empty. I'm not nuts. If
the domain is empty, then nothing exists in it. But no, you don't get a
pound of my flesh for that, because it was never an issue.

> EVERY last set-existence proof in ZF involves an inference that is
> unsound UNLESS you PRESUME, as PRIOR background, that a
> set already exists, or unless you are using a version of ZF that posits
> the existence of either the empty set or the infinite set as an axiom.

What do you mean by 'the infinite set'?

And I don't understand (I am not challenging it) your point about an
empty set axiom. With respect to domains, the standard semantics
precludes empty domains. Exactly. And, as I imagine you would stress,
this is more basic than set theory, since even the theorems of logic
alone (if you don't like that vocabulary, then I'm sorry; it's commonly
understood, and you know what I mean, and you can suggest whatever
alternative you want) wouldn't hold. So what does having an empty set
axiom do to bolster existence (existcence in a model, not merely proof
of ExPhi, since we can get existence anyway - GIVEN STANDARD SEMANTICS
- from the axiom schema of separation?

> Obviously, therefore, IF your background LOGIC must PRESUME that
> a set exists, then the real reason why the empty set exists IS THAT
> PRESUMPTION, AND NOT any proof from ZF.

I see your point. All along, perhaps you were thinking that I was
claiming to have proven existence in a model, even allowing the empty
domain. Of course it would be nuts to claim that. I just mean that a
certain formula is a theorem. That may be unsatisfying to someone
asking a question about existence in a model. But my points have never
even been directed to that issue. I was curious about another aspect of
this, which does tie in with models, but not in a way that contradicts
what I've been saying all along.

MoeBlee

.

Quantcast