> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
> <Dan_Christen...@sympatico.ca> wrote:
> > The OP seemed to be interested in how set theory is used in formal
> > verification (of computer-programming code.) It's hard to imagine, but
> > he said that ZF is actually used in some formal verification packages.
> > Unless he is talking about a substantially modified form of ZF, IMHO
> > this can't be a very productive approach.
> Actually, originally, this discussion came up as a general assertion that
> set theory was simply the wrong paradigm for any formal reasoning.
I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
don't know how ignorant they are; and they are unwilling to learn.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
> "Aaron W. Hsu" wrote:
>> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
>> <Dan_Christen...@sympatico.ca> wrote:
>> > The OP seemed to be interested in how set theory is used in formal
>> > verification (of computer-programming code.) It's hard to imagine, but
>> > he said that ZF is actually used in some formal verification packages.
>> > Unless he is talking about a substantially modified form of ZF, IMHO
>> > this can't be a very productive approach.
>> Actually, originally, this discussion came up as a general assertion that
>> set theory was simply the wrong paradigm for any formal reasoning.
> I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
> Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
> don't know how ignorant they are; and they are unwilling to learn.
Thanks, Frederick, for warning our guest. As far as I am concerned, I take it you are talking about mathematical logic specifically: in fact, here is a distinction that is not popular in sci.logic.
<freddywilli...@btinternet.com> wrote:
> "Aaron W. Hsu" wrote:
>> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
>> <Dan_Christen...@sympatico.ca> wrote:
>> > The OP seemed to be interested in how set theory is used in formal
>> > verification (of computer-programming code.) It's hard to imagine, but
>> > he said that ZF is actually used in some formal verification packages.
>> > Unless he is talking about a substantially modified form of ZF, IMHO
>> > this can't be a very productive approach.
>> Actually, originally, this discussion came up as a general assertion
>> that
>> set theory was simply the wrong paradigm for any formal reasoning.
> I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
> Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
> don't know how ignorant they are; and they are unwilling to learn.
The very idea of taking any random Internet poster as having authoritative
information without real world references or having a corresponding CV
that demonstrates their good track record seems like a crazy idea, so, no
worries. :-) Then again, this applies equally well to you and me, as well.
-- Aaron W. Hsu | arcf...@sacrideo.us | http://www.sacrideo.us Programming is just another word for the Lost Art of Thinking.
> On Sun, 07 Oct 2012 17:50:32 -0400, Frederick Williams
> <freddywilli...@btinternet.com> wrote:
>> "Aaron W. Hsu" wrote:
>>> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
>>> <Dan_Christen...@sympatico.ca> wrote:
>>> > The OP seemed to be interested in how set theory is used in formal
>>> > verification (of computer-programming code.) It's hard to imagine, but
>>> > he said that ZF is actually used in some formal verification packages.
>>> > Unless he is talking about a substantially modified form of ZF, IMHO
>>> > this can't be a very productive approach.
>>> Actually, originally, this discussion came up as a general assertion
>>> that
>>> set theory was simply the wrong paradigm for any formal reasoning.
>> I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
>> Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
>> don't know how ignorant they are; and they are unwilling to learn.
> The very idea of taking any random Internet poster as having
> authoritative information without real world references or having a
> corresponding CV that demonstrates their good track record seems like a
> crazy idea, so, no worries. :-) Then again, this applies equally well to
> you and me, as well.
Very well said. :-)
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
> <Dan_Christen...@sympatico.ca> wrote:
>> The OP seemed to be interested in how set theory is used in formal
>> verification (of computer-programming code.) It's hard to imagine, but
>> he said that ZF is actually used in some formal verification packages.
>> Unless he is talking about a substantially modified form of ZF, IMHO
>> this can't be a very productive approach.
> Actually, originally, this discussion came up as a general assertion
> that set theory was simply the wrong paradigm for any formal reasoning.
This would somewhat contradict to the general belief that most important
mathematics (the natural numbers, real continuity, topological spaces
[Hausdorff for instance] , etc...) can be formalized in say ZFC.
> The assertion in question goes something like, "trying to do anything in
> set theory is simply always the wrong abstraction; category theory is
> the right one, or at least intuitionistic type theory." The fact that
> this came up in the course of discussion among computer scientists means
> that the resulting assertion does not surprise me. However, the claim
> seemed to be made going far beyond just the verification of computer
> programs.
> The claim seemed to encompass all formal reasoning.
I'm wondering though how much of "formal reasoning" would those CS's
would really care? Or even really realize?
> Where formal verification comes in is that my background in formal
> reasoning is largely among using interactive theorem provers to prove
> properties about computer programs or recursive structures. This is not
> to say that I am only concerned with this domain when talking about the
> above assertion. However, the system which I currently use is Isabelle,
> which provides two primary theories for use: HOL and ZF. Isabelle
> targets both verification of computer software as well as generalized
> mathematics. It has been used to do proofs on various "normal"
> mathematics as well as computational mathematics.
> My main interest is understanding the tradeoffs of set theory versus
> something like category theory or type theory, as I have always found
> set theory a little easier to think about.
I'd think so too. But there's a not-so-great side of set theory,
even in practicality.
For example, one wouldn't have a problem to undersealed a definition of
say "string" [finite, left to right], but it's so unpleasant to note
that for a string s, we would also have look-alike-strings: {s}, {{s}},
etc... At certain point in a formalization, these look-alike-strings
might impact on our intention to formalize our theory about "strings".
Sorry I have to go now but at next chance I'd present a similar
situation: instead of "string" formalization, it would be "elementary
particle", "atom", "molecule" formalizations. There, we'd judge for
ourselves how good, cumbersome (or even "abhorrent") an 1-epsilon
symbol set theory such as ZFC might be.
> Indeed, when I work in HOL,
> despite its type system, types to me are just sets, and I chose Isabelle
> partly because it had such a relatively weak type system and did not
> fully embrace the intuitionist theory of constructive types and all that
> which systems like Agda and Coq seem to do. Working in an untyped world
> has always been a bit more comfortable for me. However, I am surrounded
> on all sides by intuitionist zealots (I jest, in part) who really
> embrace type theory or category theory as the solution to all manner of
> things, to the point where they really have an abhorrence of set theory.
> I am trying to understand why, and why, if their abhorrence is so
> justified, the rest of the mathematical community seems to do a great
> deal of their practical mathematics using set theory rather than
> category theory.
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
> On 07/10/2012 2:13 PM, Aaron W. Hsu wrote:
>> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
>> <Dan_Christen...@sympatico.ca> wrote:
>>> The OP seemed to be interested in how set theory is used in formal
>>> verification (of computer-programming code.) It's hard to imagine, but
>>> he said that ZF is actually used in some formal verification packages.
>>> Unless he is talking about a substantially modified form of ZF, IMHO
>>> this can't be a very productive approach.
>> Actually, originally, this discussion came up as a general assertion
>> that set theory was simply the wrong paradigm for any formal reasoning.
> This would somewhat contradict to the general belief that most important
> mathematics (the natural numbers, real continuity, topological spaces
> [Hausdorff for instance] , etc...) can be formalized in say ZFC.
>> The assertion in question goes something like, "trying to do anything in
>> set theory is simply always the wrong abstraction; category theory is
>> the right one, or at least intuitionistic type theory." The fact that
>> this came up in the course of discussion among computer scientists means
>> that the resulting assertion does not surprise me. However, the claim
>> seemed to be made going far beyond just the verification of computer
>> programs.
>> The claim seemed to encompass all formal reasoning.
> I'm wondering though how much of "formal reasoning" would those CS's
> would really care? Or even really realize?
>> Where formal verification comes in is that my background in formal
>> reasoning is largely among using interactive theorem provers to prove
>> properties about computer programs or recursive structures. This is not
>> to say that I am only concerned with this domain when talking about the
>> above assertion. However, the system which I currently use is Isabelle,
>> which provides two primary theories for use: HOL and ZF. Isabelle
>> targets both verification of computer software as well as generalized
>> mathematics. It has been used to do proofs on various "normal"
>> mathematics as well as computational mathematics.
>> My main interest is understanding the tradeoffs of set theory versus
>> something like category theory or type theory, as I have always found
>> set theory a little easier to think about.
> I'd think so too. But there's a not-so-great side of set theory,
> even in practicality.
> For example, one wouldn't have a problem to undersealed a definition of
> say "string" [finite, left to right], but it's so unpleasant to note
> that for a string s, we would also have look-alike-strings: {s}, {{s}},
> etc... At certain point in a formalization, these look-alike-strings
> might impact on our intention to formalize our theory about "strings".
"... wouldn't have a problem to understand a definition ..." I meant
(Sorry)
> Sorry I have to go now but at next chance I'd present a similar
> situation: instead of "string" formalization, it would be "elementary
> particle", "atom", "molecule" formalizations. There, we'd judge for
> ourselves how good, cumbersome (or even "abhorrent") an 1-epsilon
> symbol set theory such as ZFC might be.
>> Indeed, when I work in HOL,
>> despite its type system, types to me are just sets, and I chose Isabelle
>> partly because it had such a relatively weak type system and did not
>> fully embrace the intuitionist theory of constructive types and all that
>> which systems like Agda and Coq seem to do. Working in an untyped world
>> has always been a bit more comfortable for me. However, I am surrounded
>> on all sides by intuitionist zealots (I jest, in part) who really
>> embrace type theory or category theory as the solution to all manner of
>> things, to the point where they really have an abhorrence of set theory.
>> I am trying to understand why, and why, if their abhorrence is so
>> justified, the rest of the mathematical community seems to do a great
>> deal of their practical mathematics using set theory rather than
>> category theory.
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
On Sun, 07 Oct 2012 19:55:01 -0400, Nam Nguyen <namducngu...@shaw.ca>
wrote:
> This would somewhat contradict to the general belief that most important
> mathematics (the natural numbers, real continuity, topological spaces
> [Hausdorff for instance] , etc...) can be formalized in say ZFC.
The claim had nothing to do with the power of ZFC, which they were willing
to acknowledge. It was whether or not expressing concepts in something
like ZFC (and, I suspect, any classical system) was worthwhile, rather
than being unnecessarily complex, unintuitive, and cumbersome, as opposed
to using category theory or type theory.
-- Aaron W. Hsu | arcf...@sacrideo.us | http://www.sacrideo.us Programming is just another word for the Lost Art of Thinking.
On Sun, 07 Oct 2012 19:55:01 -0400, Nam Nguyen <namducngu...@shaw.ca>
wrote:
> For example, one wouldn't have a problem to undersealed a definition of
> say "string" [finite, left to right], but it's so unpleasant to note
> that for a string s, we would also have look-alike-strings: {s}, {{s}},
> etc... At certain point in a formalization, these look-alike-strings
> might impact on our intention to formalize our theory about "strings".
Wouldn't you normally formalize the concept of a sequence first, with a
definition of equality and so forth, and only then formalize the concept
of a "string" on top of that as being a sequence of elements whose
elements are members of the set of characters considered valid for that
string? I would imagine then that this would isolate the issue of similar
strings behind the concept of a sequence. Or, wait, were you talking about
strings as sequences? I've always thought of sequences as nothing more
than ordered sets that may contain repeated elements, and then thought of
strings as sequences whose elements are all of a particular, finite
domain, usually with the assumption that members of that domain are only
to be dealt with as atomic entities, not to be decomposed; that is, you
wouldn't have strings of characters where the characters themselves might
be sets of characters, though, you might, for instance, represent
characters as code-points if you were in unicode, in which case you would
have some way of determining whether two characters were equal, even if
they were composed of different code-points. This sort of thing does come
up in practical CS applications and language specifications.
-- Aaron W. Hsu | arcf...@sacrideo.us | http://www.sacrideo.us Programming is just another word for the Lost Art of Thinking.
> On Sun, 07 Oct 2012 17:50:32 -0400, Frederick Williams
> <freddywilli...@btinternet.com> wrote:
> > "Aaron W. Hsu" wrote:
> >> On Sun, 07 Oct 2012 13:33:55 -0400, Dan Christensen
> >> <Dan_Christen...@sympatico.ca> wrote:
> >> > The OP seemed to be interested in how set theory is used in formal
> >> > verification (of computer-programming code.) It's hard to imagine, but
> >> > he said that ZF is actually used in some formal verification packages.
> >> > Unless he is talking about a substantially modified form of ZF, IMHO
> >> > this can't be a very productive approach.
> >> Actually, originally, this discussion came up as a general assertion
> >> that
> >> set theory was simply the wrong paradigm for any formal reasoning.
> > I should warn you that Dan Christensen, Nam Nguyen, Ludovico Van and
> > Ross A. Finlayson are all ignorant of logic. The are so ignorant, they
> > don't know how ignorant they are; and they are unwilling to learn.
> The very idea of taking any random Internet poster as having authoritative
> information without real world references or having a corresponding CV
> that demonstrates their good track record seems like a crazy idea, so, no
> worries. :-) Then again, this applies equally well to you and me, as well.
Oh indeed yes, I nothing about logic and yet I still manage to know more
than those I named.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
> Oh indeed yes, I nothing about logic and yet I still manage to know more
> than those I named.
Silly me, I meant to write 'I know nothing...' Sorry.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
> > The very idea of taking any random Internet poster as having
> > authoritative information without real world references or having a
> > corresponding CV that demonstrates their good track record seems like a
> > crazy idea, so, no worries. :-) Then again, this applies equally well to
> > you and me, as well.
> Very well said. :-)
I await with interest your real world references or CV that demonstrates
your good track record.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
> On Sun, 07 Oct 2012 19:55:01 -0400, Nam Nguyen <namducngu...@shaw.ca>
> wrote:
>> For example, one wouldn't have a problem to undersealed a definition of
>> say "string" [finite, left to right], but it's so unpleasant to note
>> that for a string s, we would also have look-alike-strings: {s}, {{s}},
>> etc... At certain point in a formalization, these look-alike-strings
>> might impact on our intention to formalize our theory about "strings".
> Wouldn't you normally formalize the concept of a sequence first, with a
> definition of equality and so forth, and only then formalize the concept
> of a "string" on top of that as being a sequence of elements whose
> elements are members of the set of characters considered valid for that
> string? I would imagine then that this would isolate the issue of
> similar strings behind the concept of a sequence. Or, wait, were you
> talking about strings as sequences? I've always thought of sequences as
> nothing more than ordered sets that may contain repeated elements, and
> then thought of strings as sequences whose elements are all of a
> particular, finite domain, usually with the assumption that members of
> that domain are only to be dealt with as atomic entities, not to be
> decomposed; that is, you wouldn't have strings of characters where the
> characters themselves might be sets of characters, though, you might,
> for instance, represent characters as code-points if you were in
> unicode, in which case you would have some way of determining whether
> two characters were equal, even if they were composed of different
> code-points. This sort of thing does come up in practical CS
> applications and language specifications.
My issue isn't with the definition of "string" as a set, which
of course in ZFC for instance everything is a set.
It's the issue that however the definition for a "string" is, {s}
is usually isn't a string by the definition, which depending
on some application of abstraction might not make much sense.
For example, given 2 string s and s' the ordered pair of these
2 strings would be:
(*) {{s}, {s,s'}}
so technically the following wouldn't be an ordered pair of s, s':
(*) {{{s}}, {{s},{{{{{s'}}}}}}}
but from an abstraction point of view it doesn't make much sense
to consider (*) as an ordered pair while not (**). And in some
application of set theory, this can cause problems in expressing
the underlying concepts through the language of the set theory
in question.
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
On Oct 9, 10:21 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> It's the issue that however the definition for a "string" is, {s}
> is usually isn't a string by the definition, which depending
> on some application of abstraction might not make much sense.
We may stipulate that a 'string' means 'finite sequence'. Also, we may
stipuate that with formal languages, no symbol is a string of other
symbols. Thus a string of symbols is such that no symbol in the string
is itself a string of other symbols.
What, if anything, do you think wouldn't make sense with that?
> For example, given 2 string s and s' the ordered pair of these
> 2 strings would be:
> (*) {{s}, {s,s'}}
> so technically the following wouldn't be an ordered pair of s, s':
> (*) {{{s}}, {{s},{{{{{s'}}}}}}}
I think you mean:
(**) {{{s}}, {{s},{{{{{s'}}}}}}}
> but from an abstraction point of view it doesn't make much sense
> to consider (*) as an ordered pair while not (**).
{{{s}}, {{s},{{{{{s'}}}}}}}
is an ordered pair?
It's not the ordered pair of s and s', i.e., <s s'>, i.e. {{s} {s
s'}}, but it's still an ordered pair.
I don't see what problem you find with this regarding strings.
> On Oct 9, 10:21 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> > It's the issue that however the definition for a "string" is, {s}
> > is usually isn't a string by the definition, which depending
> > on some application of abstraction might not make much sense.
> We may stipulate that a 'string' means 'finite sequence'. Also, we may
> stipuate that with formal languages, no symbol is a string of other
> symbols. Thus a string of symbols is such that no symbol in the string
> is itself a string of other symbols.
> What, if anything, do you think wouldn't make sense with that?
> > For example, given 2 string s and s' the ordered pair of these
> > 2 strings would be:
> > (*) {{s}, {s,s'}}
> > so technically the following wouldn't be an ordered pair of s, s':
> > (*) {{{s}}, {{s},{{{{{s'}}}}}}}
> I think you mean:
> (**) {{{s}}, {{s},{{{{{s'}}}}}}}
> > but from an abstraction point of view it doesn't make much sense
> > to consider (*) as an ordered pair while not (**).
> {{{s}}, {{s},{{{{{s'}}}}}}}
> is an ordered pair?
> It's not the ordered pair of s and s', i.e., <s s'>, i.e. {{s} {s
> s'}}, but it's still an ordered pair.
> I don't see what problem you find with this regarding strings.
> Nam Nguyen: There haven't been any objections to my post below. Should
> I take it that my post clears up the matter of symbols and strings for
> you?
There had been nothing to be cleared up by anybody, in my explanation
of the string viz-a-viz _one_ epsilon predicate symbol.
> On Oct 10, 12:49 pm, MoeBlee <modem...@gmail.com> wrote:
>> On Oct 9, 10:21 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>>> It's the issue that however the definition for a "string" is, {s}
>>> is usually isn't a string by the definition, which depending
>>> on some application of abstraction might not make much sense.
>> We may stipulate that a 'string' means 'finite sequence'. Also, we may
>> stipuate that with formal languages, no symbol is a string of other
>> symbols. Thus a string of symbols is such that no symbol in the string
>> is itself a string of other symbols.
>> What, if anything, do you think wouldn't make sense with that?
>>> For example, given 2 string s and s' the ordered pair of these
>>> 2 strings would be:
>>> (*) {{s}, {s,s'}}
>>> so technically the following wouldn't be an ordered pair of s, s':
>>> (*) {{{s}}, {{s},{{{{{s'}}}}}}}
>> I think you mean:
>> (**) {{{s}}, {{s},{{{{{s'}}}}}}}
>>> but from an abstraction point of view it doesn't make much sense
>>> to consider (*) as an ordered pair while not (**).
>> {{{s}}, {{s},{{{{{s'}}}}}}}
>> is an ordered pair?
>> It's not the ordered pair of s and s', i.e., <s s'>, i.e. {{s} {s
>> s'}}, but it's still an ordered pair.
>> I don't see what problem you find with this regarding strings.
As I had explained, the problem is that the _one_ epsilon predicate
symbol is so generic a binary predicate that it`d cause problems
in applying its interpretation to certain specific cases.
For instance, if you have 2 characters a and b as sets, then
you could define the string 'ab' as the following ordered pair:
>>> (*) {{a}, {a,b}}
However, that doesn't mean the the following can't be an equivalent
definition of the string 'ab':
>> (**) {{{a}}, {{a},{{{{{b}}}}}}}
The fact that within the same set context with _one_ epsilon symbol
one could interpret a concept (e.g. "string") in more than one way
would be problematic in some applications.
That's what I had conveyed.
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
> As I had explained, the problem is that the _one_ epsilon predicate
> symbol is so generic a binary predicate that it`d cause problems
> in applying its interpretation to certain specific cases.
> For instance, if you have 2 characters a and b as sets, then
> you could define the string 'ab' as the following ordered pair:
> >>> (*) {{a}, {a,b}}
> However, that doesn't mean the the following can't be an equivalent
> definition of the string 'ab':
> >> (**) {{{a}}, {{a},{{{{{b}}}}}}}
> The fact that within the same set context with _one_ epsilon symbol
> one could interpret a concept (e.g. "string") in more than one way
> would be problematic in some applications.
In what applications? In a usual set theory, with just '=' and 'in' as
its extralogical symbols, one could define the string ab to be either
{{a}, {a,b}} or one could define it to be {{{a}}, {{a},{{{{{b}}}}}}}. (Surely one wouldn't define it to be both; in any theory to define the
same thing in two different ways would be perverse.) There is no need
for the usual 'in' and some further 'in' to handle the (**) definition.
Also, in what sense is (**) an equivalent definition to (*). Since
{{a}, {a,b}} =/= {{{a}}, {{a},{{{{{b}}}}}}}
'equivalent' would seem to be the wrong word. The inequality holds in
the usual set theories, and I don't deny that in some set theory {x} may
= x for some x. Do you have in mind such a set theory?
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> you could define the string 'ab' as the following ordered pair:
> >>> (*) {{a}, {a,b}}
> However, that doesn't mean the the following can't be an equivalent
> definition of the string 'ab':
> >> (**) {{{a}}, {{a},{{{{{b}}}}}}}
They're not equivalent definitions, since (*) is not (**).
Equivalent definitions D1 and D2 are ones in which, for a predicate we
have "definiens of D1 iff definiens of D2", and for a function we have
"definiens of D1 = definiens of D2".
But, yes, of course, any author is free to make his own stipulative
definitions. So what?
Indeed, you're free to stipulate that by 'dog' you mean a typewriter.
> On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> you could define the string 'ab' as the following ordered pair:
>>>>> (*) {{a}, {a,b}}
>> However, that doesn't mean the the following can't be an equivalent
>> definition of the string 'ab':
>>>> (**) {{{a}}, {{a},{{{{{b}}}}}}}
> They're not equivalent definitions, since (*) is not (**).
You misunderstood what I said. I didn't say (*) <-> (**) is a tautology.
I only said both definitions could equally, equivalently, express the
concept-definition of a string. Note earlier I had said:
>> For example, one wouldn't have a problem to understand a definition
>> of say "string" [finite, left to right],
> Equivalent definitions D1 and D2 are ones in which, for a predicate we
> have "definiens of D1 iff definiens of D2", and for a function we have
> "definiens of D1 = definiens of D2".
> But, yes, of course, any author is free to make his own stipulative
> definitions. So what?
> Indeed, you're free to stipulate that by 'dog' you mean a typewriter.
Indeed, the realm of mathematical abstraction is vast - infinite - and
if one limits one's own imagination to only dog-to-typewriter kinds
of examples then of course dog-to-typewriter illustrations one could
only see.
On the other hand, I did have some examples to illustrate the problem
of defining strings using only one epsilon symbol, using say a
generalized Kuratowski's string definition:
Now, given a 2-dimensional infinite grid of squares (a la John Conway)
each of which has a finite range of states. We could define a string
worm life form as a series of finite consecutive square of a certain
states.
So, without loss of generality, a (worm) string of length n would be:
s1s2s3....sn-1sn
But then, using the generalized Kuratowski's definition above,
would the _sub-string_ s1s2 be expressed in the same way as
say the _sub-string_ sn-1sn?
Would a sub-string be of the same concept as that of a string,
under Kuratowski's definition?
Apparently not. So, there is the problem that you and Frederick
have missed.
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
> On 17/10/2012 10:03 AM, MoeBlee wrote:
> > On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> you could define the string 'ab' as the following ordered pair:
> >>>>> (*) {{a}, {a,b}}
> >> However, that doesn't mean the the following can't be an equivalent
> >> definition of the string 'ab':
> >>>> (**) {{{a}}, {{a},{{{{{b}}}}}}}
> > They're not equivalent definitions, since (*) is not (**).
> You misunderstood what I said. I didn't say (*) <-> (**) is a tautology.
> I only said both definitions could equally, equivalently, express the
> concept-definition of a string. Note earlier I had said:
> >> For example, one wouldn't have a problem to understand a definition
> >> of say "string" [finite, left to right],
> > Equivalent definitions D1 and D2 are ones in which, for a predicate we
> > have "definiens of D1 iff definiens of D2", and for a function we have
> > "definiens of D1 = definiens of D2".
> > But, yes, of course, any author is free to make his own stipulative
> > definitions. So what?
> > Indeed, you're free to stipulate that by 'dog' you mean a typewriter.
> Indeed, the realm of mathematical abstraction is vast - infinite - and
> if one limits one's own imagination to only dog-to-typewriter kinds
> of examples then of course dog-to-typewriter illustrations one could
> only see.
> On the other hand, I did have some examples to illustrate the problem
> of defining strings using only one epsilon symbol, using say a
> generalized Kuratowski's string definition:
> Now, given a 2-dimensional infinite grid of squares (a la John Conway)
> each of which has a finite range of states. We could define a string
> worm life form as a series of finite consecutive square of a certain
> states.
> So, without loss of generality, a (worm) string of length n would be:
> s1s2s3....sn-1sn
> But then, using the generalized Kuratowski's definition above,
> would the _sub-string_ s1s2 be expressed in the same way as
> say the _sub-string_ sn-1sn?
> Would a sub-string be of the same concept as that of a string,
> under Kuratowski's definition?
> Apparently not. So, there is the problem that you and Frederick
> have missed.
Above, what does <-> mean? I'm used to it meaning the material
biconditional.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
> > On Oct 16, 9:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> you could define the string 'ab' as the following ordered pair:
> >>>>> (*) {{a}, {a,b}}
> >> However, that doesn't mean the the following can't be an equivalent
> >> definition of the string 'ab':
> >>>> (**) {{{a}}, {{a},{{{{{b}}}}}}}
> > They're not equivalent definitions, since (*) is not (**).
> You misunderstood what I said. I didn't say (*) <-> (**) is a tautology.
No, I did not misunderstand what you said. I did not say that you
claimed "(*) <-> (**)" is a tautology.
> I only said both definitions could equally, equivalently, express the
> concept-definition of a string.
You said, "that doesn't mean the the following can't be an equivalent
definition of the string 'ab': [...]"
And I replied that they're not equivalent definitions.
You're welcome to say now that what you meant is something else, but I
responded to what you actually said.
> > Equivalent definitions D1 and D2 are ones in which, for a predicate we
> > have "definiens of D1 iff definiens of D2", and for a function we have
> > "definiens of D1 = definiens of D2".
> > But, yes, of course, any author is free to make his own stipulative
> > definitions. So what?
> > Indeed, you're free to stipulate that by 'dog' you mean a typewriter.
> Indeed, the realm of mathematical abstraction is vast - infinite - and
> if one limits one's own imagination to only dog-to-typewriter kinds
> of examples then of course dog-to-typewriter illustrations one could
> only see.
I don't "only" see such examples. Indeed, I mentioned that example in
analogy with YOUR example.
> On the other hand, I did have some examples to illustrate the problem
> of defining strings using only one epsilon symbol, using say a
> generalized Kuratowski's string definition:
In both instances, you have two terms with a biconditional between
them. I don't know what that means.
Moreover, even if you mean "=" instead of "<->" there, the second
instance is not the ordinary generalization of the Kuratowski
definition. Instead, it is:
<a1 a2 ... an-1 an> = <<a1 a2 ... an-1> an>
And again, I completely agree that one can stipulate alternative
defintions of mathematical terminology and notation, just as one can
stipulate that by 'dog' one means typewriter. Yes, if two people use
different defintions, then they may get different results. I don't see
any point you've made beyond that obvious fact.
> [...] using say a
> generalized Kuratowski's string definition:
> (a,b) <-> {{a}, {a,b}}
That's ok if we read '<->' as 'is defined to be'. (Which is
nonstandard, but never mind.)
> (a1, a2, ..., an-1, an) <-> (an-1,an).
But we can hardly read that as meaning (a1, a2, ..., an-1, an) is
defined to be (an-1,an). If that were so (1,2,3,4) and (5,6,3,4) would
both be defined to be (3,4).
You can define (a,b,c) as ((a,b),c) or as (a,(b,c)). I've seen both. And similarly with quadruples, etc. Or you can define n-tuples as
functions on {1,2,...,n} (or on {0,2,...,n-1}) with the appropriate
codomain.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
>> [...] using say a
>> generalized Kuratowski's string definition:
>> (a,b) <-> {{a}, {a,b}}
> That's ok if we read '<->' as 'is defined to be'. (Which is
> nonstandard, but never mind.)
Yes: for clarity, it should have been the notation "df=" here.
>> (a1, a2, ..., an-1, an) <-> (an-1,an).
> But we can hardly read that as meaning (a1, a2, ..., an-1, an) is
> defined to be (an-1,an). If that were so (1,2,3,4) and (5,6,3,4) would
> both be defined to be (3,4).
It was a typo on my part. It should have been (as you alluded to below):
(a1, a2, ..., an-1, an) df= ((a1,...,an-1),an)
> You can define (a,b,c) as ((a,b),c) or as (a,(b,c)). I've seen both.
> And similarly with quadruples, etc.
Now that it seems clear on the definition, would you see my point about
the problem of there being only 1 epsilon symbol, viz-a-viz the concept
of "sub-string", in relation to that of "string"?
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
> On Oct 17, 9:49 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> On the other hand, I did have some examples to illustrate the problem
>> of defining strings using only one epsilon symbol, using say a
>> generalized Kuratowski's string definition:
>> (a,b) <-> {{a}, {a,b}}
>> (a1, a2, ..., an-1, an) <-> (an-1,an).
> In both instances, you have two terms with a biconditional between
> them. I don't know what that means.
As I've just mentioned to Frederick, it was meant to be "df=";
and ...
> Moreover, even if you mean "=" instead of "<->" there, the second
> instance is not the ordinary generalization of the Kuratowski
> definition. Instead, it is:
> <a1 a2 ... an-1 an> = <<a1 a2 ... an-1> an>
it was a typo in my previous posts: your above is what I really meant.
> And again, I completely agree that one can stipulate alternative
> defintions of mathematical terminology and notation, just as one can
> stipulate that by 'dog' one means typewriter. Yes, if two people use
> different defintions, then they may get different results. I don't see
> any point you've made beyond that obvious fact.
With the definitions clarified, you'd see that the problem is about
"sub-string" vs. "string", not "dog" and "typewriter" as you might
have "feared". Would you not?
In summary, hope that you now would understand the point I made to
the op that there being only 1 epsilon (binary) relation symbol would
be a weakness in some applications of (typical) set-theories.
-- ----------------------------------------------------
There is no remainder in the mathematics of infinity.
On Oct 18, 9:19 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> hope that you now would understand the point I made to
> the op that there being only 1 epsilon (binary) relation symbol would
> be a weakness in some applications of (typical) set-theories.
Nam Nguyen wrote:
> Now that it seems clear on the definition, would you see my point about
> the problem of there being only 1 epsilon symbol, viz-a-viz the concept
> of "sub-string", in relation to that of "string"?
Strings and their substrings can be discussed without the need for set
theory, for example as in generative grammar. Or as in the theory of
free monoids. It would seem to me that the symbol epsilon is
irrelevant.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
