Hello,
I am almost half way through Boolos’s Computability and logic. It has a
truly magnificent graph of the logical dependence of the chapters,
which I have prestudied with deepest care and respect.
The landscape is outstanding!
Please, may I ask for a reading suggestion, as well as, perhaps, some
kind commentary, as regards a mathematical formulation of a substring
replacement?
With the poorest of tools (intuition) at my disposal at the moment, I
repeatedly tried to give the problem some formulation, but to no avail.
I merely fail to substitute (and compare, of course) formally, and
without the aid of intuition.
I realize that _properly formulated definitions of truth/provability
predicates involve diagonalization, still, in the end, one does apply
rules of inference to theorems (or a state to the tape), whereas I fail
to provide anything plausible _mathematically.
I would not dare ask if I knew the answer were a matter of another
several months or so of self-study.
Thank you very much indeed, and I am sorry for all intrusion.
Tom
Tom wrote:
> Please, may I ask for a reading suggestion, as well as, perhaps, some
> kind commentary, as regards a mathematical formulation of a substring
> replacement?
…..
> I realize that _properly formulated definitions of truth/provability
> predicates involve diagonalization, …
Hi, I think you are going to have to clarify your question …it is
very unclear what you are asking for.
But note that *diagonalization* doesn’t have to be defined using
*substitution* (i.e. "substring replacement") at all. Boolos, Burgess
and Jeffrey explain how at pp. 221-222.
Peter_Smith wrote:
Thank you very much for writing, Peter.
> > Please, may I ask for a reading suggestion, as well as, perhaps, some
> > kind commentary, as regards a mathematical formulation of a substring
> > replacement?
> …..
> > I realize that _properly formulated definitions of truth/provability
> > predicates involve diagonalization, …
> Hi, I think you are going to have to clarify your question …it is
> very unclear what you are asking for.
With your kind permission, I am asking for a mathematically acceptable
way to compare and substitute (i.e. to replace a substring of a string
with another string according to a replacement rule). I mentioned other
things to manifest that ever since I read Turing I am unwilling to
assume /anything/ without professional mathematical expertese. My
appeal to authority is because I am incapable of making any assumptions
on my own and diagonality _seems to be much of a problem here, to say
the least.
> But note that *diagonalization* doesn’t have to be defined using
> *substitution* (i.e. "substring replacement") at all. Boolos, Burgess
> and Jeffrey explain how at pp. 221-222.
Yes, thank you. The second edition discusses the decidability without
multiplication at this point. Much that I would love to apply these
results to my present problem, I merely fail to do so. I am sorry about
that.
To make a long story short: please, how do I compare and substitute and
somehow ignore the infinite regress (involved)?
Thank you very much indeed for your help.
Tom
> I am asking for a mathematically acceptable
> way to compare and substitute (i.e. to replace a substring of a string
> with another string according to a replacement rule).
> To make a long story short: please, how do I compare and substitute and
> somehow ignore the infinite regress (involved)?
Why do you have a worry about infinite regress?
Here’s one expression:
(Fx –> Fx)
and I want to uniformly replace the substring "x" by, e.g, the numeral
"3". No infinite regress.
Even if I want to replace the substring "Fx" by "(Fx ^ Hx)", still no
regress if I’m just asked to do a single round of substitutions.
- Hide quoted text — Show quoted text -
Peter_Smith wrote:
> > I am asking for a mathematically acceptable
> > way to compare and substitute (i.e. to replace a substring of a string
> > with another string according to a replacement rule).
> > To make a long story short: please, how do I compare and substitute and
> > somehow ignore the infinite regress (involved)?
> Why do you have a worry about infinite regress?
> Here’s one expression:
> (Fx –> Fx)
> and I want to uniformly replace the substring "x" by, e.g, the numeral
> "3". No infinite regress.
> Even if I want to replace the substring "Fx" by "(Fx ^ Hx)", still no
> regress if I’m just asked to do a single round of substitutions.
Yes, thank you very much for your kind attention, Peter.
The object string is "(Fx –> Fx)", the
meta(production/substitution)string is "x subs 3" (using my rubbish
non-standard notation).
Now, to apply the latter the system compares:
1. "x" with "(" – no match, then
2. "x" with "F" - no match, then
3. "x" with "x" - match, substitution, then
4. "x" with " " – no match, then
5-9. "x" with "-", "-", ">", " ", "F" - no match, then
10. "x" with "x" - match, substitution, then
11. "x" with some end marker, terminating condition.
Just how the very comparison is effected(!), where the result of the
first comparison is returned, i.e. how the subsequent stages of
comparison (and substitution) communicate with each other, and how the
process knows which are the first two and the subsequent two and
further and further symbols /i.e. primitive strings/ to be compared –
remains a mistery to me when I attempt to give a mathematically
plausible exposition of an automaton that performs this. One that
accepts the string:
(x subs 3)apply_on(Fx –> Fx)
and yields the desired string. This knowledge must be in the system
already, and yet I am only attempting to define it.
That knowledge is always in the metasystem. Distinguishability _seems
ample but the knowledge of it appears to be always in the metasystem.
All I am asking is a reading suggestion that treats these matters in an
honest and transparent way, i.e. mathematically.
Again, thank you very much indeed for your kind attention, Peter.
Tom
Tom wrote:
> Just how the very comparison is effected(!), where the result of the
> first comparison is returned, i.e. how the subsequent stages of
> comparison (and substitution) communicate with each other, and how the
> process knows which are the first two and the subsequent two and
> further and further symbols /i.e. primitive strings/ to be compared –
> remains a mistery to me when I attempt to give a mathematically
> plausible exposition of an automaton that performs this. ..
> ….
> All I am asking is a reading suggestion that treats these matters in an
> honest and transparent way, i.e. mathematically.
Well I confess I don’t really see what you are after. You gave, so to
speak, a low-level software description (compare the contents of two
memory registers, if they’re the same, do this, if they’re not do that,
etc, etc,), and you now ask "how the very comparison is effected" which
looks like an engineering problem, how to get some hardware to execute
that kind of program step. *That* doesn’t look like a mathematical
problem at all. But I’m sure I’m missing your point, so I’ll stop.
>> Just how the very comparison is effected(!), where the result of the
>> first comparison is returned, i.e. how the subsequent stages of
>> comparison (and substitution) communicate with each other, and how the
>> process knows which are the first two and the subsequent two and
>> further and further symbols /i.e. primitive strings/ to be compared –
>> remains a mistery to me when I attempt to give a mathematically
>> plausible exposition of an automaton that performs this. ..
> Well I confess I don’t really see what you are after. You gave, so to
> speak, a low-level software description (compare the contents of two
> memory registers, if they’re the same, do this, if they’re not do that,
> etc, etc,), and you now ask "how the very comparison is effected" which
> looks like an engineering problem, how to get some hardware to execute
> that kind of program step. *That* doesn’t look like a mathematical
> problem at all. But I’m sure I’m missing your point, so I’ll stop.
It sounds like a proof that Post systems are equivalent to Turing
machines would fit the bill (since Post systems use substitution as
a computational primitive). Anybody know of a neat one?
============== j-c ====== @ ====== purr . demon . co . uk ==============
Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
<http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
Tom wrote:
> Please, may I ask for a reading suggestion, as well as, perhaps, some
> kind commentary, as regards a mathematical formulation of a substring
> replacement?
Are you asking for a rigorous mathematical definition of replacing a
substring in a string with another substring?
MoeBlee
Peter_Smith wrote:
>> Tom wrote:
> > Just how the very comparison is effected(!), where the result of the
> > first comparison is returned, i.e. how the subsequent stages of
> > comparison (and substitution) communicate with each other, and how the
> > process knows which are the first two and the subsequent two and
> > further and further symbols /i.e. primitive strings/ to be compared –
> > remains a mistery to me when I attempt to give a mathematically
> > plausible exposition of an automaton that performs this. ..
> > ….
> > All I am asking is a reading suggestion that treats these matters in an
> > honest and transparent way, i.e. mathematically.
> Well I confess I don’t really see what you are after.
Mathematical truth. /Now and always/.
> You gave, so to speak, a low-level software description (compare the contents of two
> memory registers, if they’re the same, do this, if they’re not do that,
> etc, etc,), and you now ask "how the very comparison is effected" which
> looks like an engineering problem, how to get some hardware to execute
> that kind of program step.
> *That* doesn’t look like a mathematical problem at all.
Yes, Peter. Still, IMHO, comparison and substitution is a mathematical
problem entirely (as are all engineering problems, again, IMHO).
> But I’m sure I’m missing your point, so I’ll stop.
I am very sorry to have mispronounced my intentions. I though I did
express a need for an entirely /mathematical and _abstract treatment of
comparison and substitution/, and a mathematical treatment of a way to
concatenate these arbitrarily. I think you understood me perfectly,
still, I myself seem to be missing something important here.
Thank you very much indeed for writing.
Tom
MoeBlee wrote:
> Tom wrote:
> > Please, may I ask for a reading suggestion, as well as, perhaps, some
> > kind commentary, as regards a mathematical formulation of a substring
> > replacement?
> Are you asking for a rigorous mathematical definition of replacing a
> substring in a string with another substring?
Yes please, Moe.
Tom
- Hide quoted text — Show quoted text -
Jack Campin wrote:
> >> Just how the very comparison is effected(!), where the result of the
> >> first comparison is returned, i.e. how the subsequent stages of
> >> comparison (and substitution) communicate with each other, and how the
> >> process knows which are the first two and the subsequent two and
> >> further and further symbols /i.e. primitive strings/ to be compared –
> >> remains a mistery to me when I attempt to give a mathematically
> >> plausible exposition of an automaton that performs this. ..
> > Well I confess I don’t really see what you are after. You gave, so to
> > speak, a low-level software description (compare the contents of two
> > memory registers, if they’re the same, do this, if they’re not do that,
> > etc, etc,), and you now ask "how the very comparison is effected" which
> > looks like an engineering problem, how to get some hardware to execute
> > that kind of program step. *That* doesn’t look like a mathematical
> > problem at all. But I’m sure I’m missing your point, so I’ll stop.
> It sounds like a proof that Post systems are equivalent to Turing
> machines would fit the bill (since Post systems use substitution as
> a computational primitive). Anybody know of a neat one?
Please, is there a text which discusses the how’s and why’s of this
usage? It is what I am after truly.
I could then attempt to do the proof on my own and as an analogy to the
beautiful expositions of correspondences in Boolos&Jeffrey.
- Hide quoted text — Show quoted text -
> ============== j-c ====== @ ====== purr . demon . co . uk ==============
> Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
> <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
> stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
Tom wrote:
> MoeBlee wrote:
> > Tom wrote:
> > > Please, may I ask for a reading suggestion, as well as, perhaps, some
> > > kind commentary, as regards a mathematical formulation of a substring
> > > replacement?
> > Are you asking for a rigorous mathematical definition of replacing a
> > substring in a string with another substring?
> Yes please, Moe.
It seems to me that there are at least two methods in the context I
just described.
One method is to use "dummy variables". For example, suppose we want to
replace the term t in the formula P with the term t’ (P is a string and
t and t’ are strings). Then we choose (with certain technical
restrictions) a dummy variable, say v (which is a string of exactly one
symbol). Meanwhile, by recursion, we will have already defined ‘the
result of substituting a term for a variable in a formula’. That
recursive definition will be easy since we are substituting a term
(which is a string of possibly many symbols) for a variable (which is a
single symbol), and such "many for one" substitutions are easy to do
recursively. The notation for this will look like:
We set P to
P’[t|v]
where v is a variable not in P.
In other words, P has the term t in P all along, but we "mark" where t
occurs in P by "pretending" that t is substituted for v everywhere v
occurs in P’; so v marks where t occurs.
Then the result of substituting a term t’ for term t in a formula P
will be be the formula:
P’[t'|v]
In other words, instead of v marking where t occurs, now v marks where
t’ occurs, and t’ occurs exactly where t occured, viz. where v
occurred.
I’m leaving out some of the technicalities, but this is the general
idea. I suggest Enderton’s ‘A Mathematical Introduction To Logic’ for
background. As I recall, he doesn’t get into replacing term for term,
but he does explain replacing term for variable, which is the first
step needed. And van Dalen’s ‘Logic And Structure’ discusses the dummy
variable technique.
Another method is more general but more complicated (I haven’t gone
through the details myself). Say we want to substitute a string t’ for
a substring t in a string s (t, t’, and s being any strings, not
necessarily terms and formulas). Then we note the positions that t
occupies in s (e.g., in the string ‘xxyzuvwyzux’, the substring ‘yzu’
occupies positions 3-5 and positions 8-10). Then we note the length of
t’. Then we concatenate:
positions 1-2 of t with
t’ with
positions 6-7 of t with
t’ with
position 11 of t.
Formalizing a GENERAL definition of such a concatenation operation
would be somewhat complicated, but I am pretty sure that it can be
done, especially since computer programs such as word processors do
those kinds of concatenations (e.g., substituting a word for another
word throughout a document).
MoeBlee
Moe, thank you very much for writing. With permission, I will save your
kind post and study it _carefully at home. I shall answer properly
tomorrow.
Thank you very much for your bibliographical suggestions. I trust those
are great(!) books as I have had plenty of chance to study your
competent posts and learn of your great mathematical skill. I will put
them on the top of my reading list. Boolos&Jeffrey are pretty much
self-contained, though, and if you think about it (this item has
received great applause from many a mathie). It is just that little
part I mentioned that has continued to make me bounce off for several
months now. Seems like a nut too tough for a complete newbie like me.
Kindest regards,
Tom
Tom wrote:
> Boolos&Jeffrey are pretty much
> self-contained, though, and if you think about it (this item has
> received great applause from many a mathie). It is just that little
> part I mentioned that has continued to make me bounce off for several
> months now. Seems like a nut too tough for a complete newbie like me.
Yes, Boolos, Jeffrey, and Burgess is a great book. But I think youl’ll
find the explanations in Enderton also help a great deal, especially
his explanations of the relation between induction and recursion.
It’s interesting to me that you’re concerned with this level of detail.
Most people don’t pursue questions of rigor to the extent that you are
doing. But I too like to follow up with the rigor, at least in the
formation and syntax of the first order languages used for mathematics,
so that I am very clear that every step is truly rigorous (and, by the
theorem about represantability, therefore recursive). I think you’ll
find that if you hold to that demand, then there are many steps that
you have to fill in for yourself that the textbooks (understandably)
take for granted as formal steps we could complete though tedious to do
so. I have learned a lot about logic and formal syntax just by plowing
through to fill in every step, even though it can be tedious to do so
and I don’t recommend that everyone should do it.
MoeBlee
Moe, I include both of your kind posts here for convenience.
(substring replacement)
Moe wrote:
> It seems to me that there are at least two methods in the context I
> just described.
> One method is to use "dummy variables". For example, suppose we want to
> replace the term t in the formula P with the term t’ (P is a string and
> t and t’ are strings). Then we choose (with certain technical
> restrictions) a dummy variable, say v (which is a string of exactly one
> symbol). Meanwhile, by recursion,
I am sorry, Moe. I tried to think about it as carefully /as I can/. It
seems that at this point we assume comparison and substitution (i.e.
substring replacement) to be predefined.
- Hide quoted text — Show quoted text -
> we will have already defined ‘the
> result of substituting a term for a variable in a formula’. That
> recursive definition will be easy since we are substituting a term
> (which is a string of possibly many symbols) for a variable (which is a
> single symbol), and such "many for one" substitutions are easy to do
> recursively. The notation for this will look like:
> We set P to
> P’[t|v]
> where v is a variable not in P.
> In other words, P has the term t in P all along, but we "mark" where t
> occurs in P by "pretending" that t is substituted for v everywhere v
> occurs in P’; so v marks where t occurs.
> Then the result of substituting a term t’ for term t in a formula P
> will be be the formula:
> P’[t'|v]
> In other words, instead of v marking where t occurs, now v marks where
> t’ occurs, and t’ occurs exactly where t occured, viz. where v
> occurred.
Yes, I see.
> I’m leaving out some of the technicalities, but this is the general
> idea. I suggest Enderton’s ‘A Mathematical Introduction To Logic’ for
> background. As I recall, he doesn’t get into replacing term for term,
> but he does explain replacing term for variable, which is the first
> step needed. And van Dalen’s ‘Logic And Structure’ discusses the dummy
> variable technique.
I trust those are great(!) books and put them on the top of my reading
list. ‘Logic and Structure’ seems particularly encouraging.
> Another method is more general but more complicated (I haven’t gone
> through the details myself). Say we want to substitute a string t’ for
> a substring t in a string s (t, t’, and s being any strings, not
> necessarily terms and formulas). Then we note the positions that t
> occupies in s (e.g., in the string ‘xxyzuvwyzux’, the substring ‘yzu’
> occupies positions 3-5 and positions 8-10).
Here again, we pre-used substring replacement for computing both pairs
of numbers. I.e. to determine the position of the target string we need
to execute a number of comparisons. Those have to communicate by
passing their results to subsequent stages, so substitution is
involved, again, IMHO.
> Then we note the length of
> t’. Then we concatenate:
> positions 1-2 of t with
> t’ with
> positions 6-7 of t with
> t’ with
> position 11 of t.
> Formalizing a GENERAL definition of such a concatenation operation
> would be somewhat complicated,
By all means. You number-theorize your constructors and selectors. Then
you reduce arithmetic to FOPL. Then you goedelize logic. The result
being a single natural number is re-applied to itself.
> but I am pretty sure that it can be
> done, especially since computer programs such as word processors do
> those kinds of concatenations (e.g., substituting a word for another
> word throughout a document).
Yes, sure. Word processors use it a lot.
(Boolos, Jeffrey, Burgess)
> > Tom wrote
> > Boolos&Jeffrey are pretty much
> > self-contained, though, and if you think about it (this item has
> > received great applause from many a mathie). It is just that little
> > part I mentioned that has continued to make me bounce off for several
> > months now. Seems like a nut too tough for a complete newbie like me.
Moe wrote:
> Yes, Boolos, Jeffrey, and Burgess is a great book.
Thank you.
> But I think youl’ll find the explanations in Enderton also help a great deal, especially
> his explanations of the relation between induction and recursion.
Yes, and please be assured that both of your kind bibliographical
suggestions are on the top of my reading list.
> It’s interesting to me that you’re concerned with this level of detail.
Thank you, Moe.
> Most people don’t pursue questions of rigor to the extent that you are
> doing.
IMHO, it’s because they usually it doing with some implementation in
mind, and as soon as the description is good enough their job is done.
> But I too like to follow up with the rigor, at least in the
> formation and syntax of the first order languages used for mathematics,
> so that I am very clear that every step is truly rigorous (and, by the
> theorem about represantability, therefore recursive).
Yes, I see.
> I think you’ll find that if you hold to that demand, then there are many steps that
> you have to fill in for yourself that the textbooks (understandably)
> take for granted as formal steps we could complete though tedious to do
> so.
But I love doing that! After all, nothing else is there, or is there?
> I have learned a lot about logic and formal syntax just by plowing
> through to fill in every step, even though it can be tedious to do so
> and I don’t recommend that everyone should do it.
Completely agree with you. I mean, not unless they are after less than
the mathematical truth itself.
Thank you so much for writing, Moe.
Kindest regards,
Tom
Tom wrote:
> Moe wrote:
> > One method is to use "dummy variables". For example, suppose we want to
> > replace the term t in the formula P with the term t’ (P is a string and
> > t and t’ are strings). Then we choose (with certain technical
> > restrictions) a dummy variable, say v (which is a string of exactly one
> > symbol). Meanwhile, by recursion,
> I am sorry, Moe. I tried to think about it as carefully /as I can/. It
> seems that at this point we assume comparison and substitution (i.e.
> substring replacement) to be predefined.
I can understand that it might seem that way, but if we were to start
at the beginning, you’d see that by using recursion we avoid
presupposition.
I’m not expert at this, but I have worked through some details. If I
understand you correctly, your question is roughly the same question I
was asking myself about a year ago, except my question was not general
regarding any substrings whatever but rather substrings that are terms
in formulas or that are subformulas in formulas. This is the problem I
asked myself about:
I understand how to recursively define substituting a term for a
variable in a formula; and I understand how to recursively define
substituting a formula for a sentence letter in a formula; but I don’t
know how to define substituting a term for a term in a formula nor
substituting a formula for a formula in a formula.
Substituting a term for a variable or a formula for a sentence letter
is a "many for one" substitution. We substitute a string that may be
more than one symbol for just a single symbol. That’s easy to define by
recursion. But substituting a term for a term or a formula for a
formula is a "many for many" substitution, and I couldn’t figure out
how to rigorously define that.
Then I thought that the best approach might not be so direct. Instead
of directly defining substituting a term for a term, what I did instead
was to COMPARE two different results of substitutng a term for a
variable. Suppose I want to substitute the term t’ for the term t in
the formula P. So I take the formula Q, where Q is just like P except Q
is "gutted out" so that some variable v occurs where t occurred in P.
Now, that might be where you think substitution is presumed as we are
subsituting v for t. But we don’t actually substitute v for t. Rather,
we reach even further back as if to START with the formula Q so that P
is Q[t|v]. I know that doesn’t seem right, but if I gave you the full
technical context, you’d see it actually works out correctly without
presupposition. So I substitute the term t for the variable v in the
formula Q (notated as Q[t|v]) and that is actually just the formula P.
And I substitute the term t’ for the variable v in the formula Q
(notated as Q[t'|v]). So (with certain other technical restrictions)
Q[t'|v] is the result of substituting t’ for t in P. Then, by some more
technical details (such as specifying that v is the first variable that
does not occur free in P while Q is the unique formula such that P is
Q[t|v], blah blah blah), we can make this a formal definition. And the
same method works, mutatis mutandis, for substituting a formula for a
formula in a formula.
Notice that this provides for substituting t’ for ALL occurrences of t
in P. Sometimes we want to allow for substituting t’ for only SOME
occurences t in P (for example, in stating a theorem schema of identity
theory, we would want to say that the formulas t=t’ and P together
imply any formula that is the result of t’ substituted for t in zero or
more (not necessarily all) places in P). But that too can be formalized
with yet more technical rigmarole. However, to specify substituting for
a PARTICULAR occurrence of t requires even more technical rigmarole.
> > Another method is more general but more complicated (I haven’t gone
> > through the details myself). Say we want to substitute a string t’ for
> > a substring t in a string s (t, t’, and s being any strings, not
> > necessarily terms and formulas). Then we note the positions that t
> > occupies in s (e.g., in the string ‘xxyzuvwyzux’, the substring ‘yzu’
> > occupies positions 3-5 and positions 8-10).
> Here again, we pre-used substring replacement for computing both pairs
> of numbers. I.e. to determine the position of the target string we need
> to execute a number of comparisons. Those have to communicate by
> passing their results to subsequent stages, so substitution is
> involved, again, IMHO.
I don’t follow you here. We’re given a string of symbols. A string may
be regarded as a function on a natural number (or often we "bump up" so
that the domain excludes 0 so that we start at 1 instead of 0). So
every entry in the string is indexed by a number, which is the position
of that entry in the string. So I can say that in the string
‘xxyzuvwyzux’, we have the substring ‘yzu’ occurring in positions 3-5
and 8-10 (except that, technically, the domain of the string ‘yzu’ is
not {1 2 3} but rather {3 4 5} and {8 9 10}, and we can "adjust" those
back down to {1 2 3}). There are no presuppositions about subsitution
so far. Then we pull the whole thing apart, using POSITIONS to keep
track of where substrings start and end, then put it all back together
(concatenation, which can be rigorously defined) with different values
for some of the positions. Still, no presupposition about subsitution.
By the way, you’ll find a lot of the formalization regarding syntax for
first order languages is done in the proof of incompleteness. That’s
where you usually find the explicit recursive functions that are only
informally given in earlier chapters of a logic textbook. You don’t
usually find a formalization of the GENERAL function of replacing a
string for a string in a string, but at least you’ll find the recursive
definition of P[t|v], which is the most important instance as far as
syntax for first order languages is concerned.
> By all means. You number-theorize your constructors and selectors. Then
> you reduce arithmetic to FOPL. Then you goedelize logic. The result
> being a single natural number is re-applied to itself.
Okay, so I see you already knew about what I just mentioned.
> > Most people don’t pursue questions of rigor to the extent that you are
> > doing.
> IMHO, it’s because they usually it doing with some implementation in
> mind, and as soon as the description is good enough their job is done.
Yes, for example, if one had the assignment of writing a computer
program to verify all these syntactical operatons, then one would have
to come to grips with such technicalities as rigorous definitions for
substitutions.
> > I think you’ll find that if you hold to that demand, then there are many steps that
> > you have to fill in for yourself that the textbooks (understandably)
> > take for granted as formal steps we could complete though tedious to do
> > so.
> But I love doing that! After all, nothing else is there, or is there?
Well, that’s a subject for some philosophical debate! But I think most
people at least agree that it helps to understand not just every
technical step but also to have an intuitive understanding of what it
all adds up to.
MoeBlee
MoeBlee wrote:
> > > One method is to use "dummy variables". For example, suppose we want to
> > > replace the term t in the formula P with the term t’ (P is a string and
> > > t and t’ are strings). Then we choose (with certain technical
> > > restrictions) a dummy variable, say v (which is a string of exactly one
> > > symbol). Meanwhile, by recursion,
> > I am sorry, Moe. I tried to think about it as carefully /as I can/. It
> > seems that at this point we assume comparison and substitution (i.e.
> > substring replacement) to be predefined.
> I can understand that it might seem that way, but if we were to start
> at the beginning, you’d see that by using recursion we avoid
> presupposition.
Moe, I am afraid I am not competent enough to pursue a more technical
argument, much that I would indeed like. I take your word for my being
mistaken about the whole thing, and very happily. Yet, the idea in my
head remains which is that we are really speaking of the same thing in
a different way. Unfortunately, I have no precise proof for this. Your
position is that recursion is the key, I agree. I mean, anyone with at
least a little sense does.
> I’m not expert at this, but I have worked through some details. If I
> understand you correctly, your question is roughly the same question I
> was asking myself about a year ago, except my question was not general
> regarding any substrings whatever but rather substrings that are terms
> in formulas or that are subformulas in formulas.
- Hide quoted text — Show quoted text -
> This is the problem I asked myself about:
> I understand how to recursively define substituting a term for a
> variable in a formula; and I understand how to recursively define
> substituting a formula for a sentence letter in a formula; but I don’t
> know how to define substituting a term for a term in a formula nor
> substituting a formula for a formula in a formula.
> Substituting a term for a variable or a formula for a sentence letter
> is a "many for one" substitution. We substitute a string that may be
> more than one symbol for just a single symbol. That’s easy to define by
> recursion. But substituting a term for a term or a formula for a
> formula is a "many for many" substitution, and I couldn’t figure out
> how to rigorously define that.
> Then I thought that the best approach might not be so direct. Instead
> of directly defining substituting a term for a term, what I did instead
> was to COMPARE two different results of substitutng a term for a
> variable. Suppose I want to substitute the term t’ for the term t in
> the formula P. So I take the formula Q, where Q is just like P except Q
> is "gutted out" so that some variable v occurs where t occurred in P.
> Now, that might be where you think substitution is presumed as we are
> subsituting v for t. But we don’t actually substitute v for t. Rather,
> we reach even further back as if to START with the formula Q so that P
> is Q[t|v]. I know that doesn’t seem right, but if I gave you the full
> technical context, you’d see it actually works out correctly without
> presupposition. So I substitute the term t for the variable v in the
> formula Q (notated as Q[t|v]) and that is actually just the formula P.
> And I substitute the term t’ for the variable v in the formula Q
> (notated as Q[t'|v]). So (with certain other technical restrictions)
> Q[t'|v] is the result of substituting t’ for t in P. Then, by some more
> technical details (such as specifying that v is the first variable that
> does not occur free in P while Q is the unique formula such that P is
> Q[t|v], blah blah blah), we can make this a formal definition. And the
> same method works, mutatis mutandis, for substituting a formula for a
> formula in a formula.
> Notice that this provides for substituting t’ for ALL occurrences of t
> in P. Sometimes we want to allow for substituting t’ for only SOME
> occurences t in P (for example, in stating a theorem schema of identity
> theory, we would want to say that the formulas t=t’ and P together
> imply any formula that is the result of t’ substituted for t in zero or
> more (not necessarily all) places in P). But that too can be formalized
> with yet more technical rigmarole. However, to specify substituting for
> a PARTICULAR occurrence of t requires even more technical rigmarole.
Again, I will save and study it very carefully.
> > > Another method is more general but more complicated (I haven’t gone
> > > through the details myself). Say we want to substitute a string t’ for
> > > a substring t in a string s (t, t’, and s being any strings, not
> > > necessarily terms and formulas). Then we note the positions that t
> > > occupies in s (e.g., in the string ‘xxyzuvwyzux’, the substring ‘yzu’
> > > occupies positions 3-5 and positions 8-10).
> > Here again, we pre-used substring replacement for computing both pairs
> > of numbers. I.e. to determine the position of the target string we need
> > to execute a number of comparisons. Those have to communicate by
> > passing their results to subsequent stages, so substitution is
> > involved, again, IMHO.
> I don’t follow you here.
It must be because of the terrible sloppiness of my thinking. I am
sorry.
> We’re given a string of symbols. A string may
> be regarded as a function on a natural number (or often we "bump up" so
> that the domain excludes 0 so that we start at 1 instead of 0). So
> every entry in the string is indexed by a number, which is the position
> of that entry in the string. So I can say that in the string
> ‘xxyzuvwyzux’, we have the substring ‘yzu’ occurring in positions 3-5
> and 8-10 (except that, technically, the domain of the string ‘yzu’ is
> not {1 2 3} but rather {3 4 5} and {8 9 10}, and we can "adjust" those
> back down to {1 2 3}). There are no presuppositions about subsitution
> so far. Then we pull the whole thing apart, using POSITIONS to keep
> track of where substrings start and end, then put it all back together
> (concatenation, which can be rigorously defined) with different values
> for some of the positions. Still, no presupposition about subsitution.
Well, you added a little more description here. I need time to study
it.
If you don’t mind me asking at this point, what in your opinion
presupposes comparison?
> By the way, you’ll find a lot of the formalization regarding syntax for
> first order languages is done in the proof of incompleteness.
Thank you. I will surely use that information.
> That’s where you usually find the explicit recursive functions that are only
> informally given in earlier chapters of a logic textbook. You don’t
> usually find a formalization of the GENERAL function of replacing a
> string for a string in a string, but at least you’ll find the recursive
> definition of P[t|v], which is the most important instance as far as
> syntax for first order languages is concerned.
Yes, I see.
> > By all means. You number-theorize your constructors and selectors. Then
> > you reduce arithmetic to FOPL. Then you goedelize logic. The result
> > being a single natural number is re-applied to itself.
> Okay, so I see you already knew about what I just mentioned.
Oh, I just gave you a large-scale map in my mind. I need to do some
more hiking to fill it in.
> > > Most people don’t pursue questions of rigor to the extent that you are
> > > doing.
> > IMHO, it’s because they usually it doing with some implementation in
> > mind, and as soon as the description is good enough their job is done.
> Yes, for example, if one had the assignment of writing a computer
> program to verify all these syntactical operatons, then one would have
> to come to grips with such technicalities as rigorous definitions for
> substitutions.
"The Sprit of Truth" is my favourite chapter of my most favourite book
ever: A. Hodges, "Alan Turing".
> > > I think you’ll find that if you hold to that demand, then there are many steps that
> > > you have to fill in for yourself that the textbooks (understandably)
> > > take for granted as formal steps we could complete though tedious to do
> > > so.
> > But I love doing that! After all, nothing else is there, or is there?
> Well, that’s a subject for some philosophical debate!
Well, IMHO, the Church-Turing thesis /holds/ philosophy really tight.
> But I think most people at least agree that it helps to understand not just every
> technical step but also to have an intuitive understanding of what it
> all adds up to.
Yes, indeed. And Moe, I can not tell you how greatful I am to you for
taking this while with me. Thank you very much for your patience and
attention.
Kindest regards,
Tom
- Hide quoted text — Show quoted text -
Tom wrote:
> > We’re given a string of symbols. A string may
> > be regarded as a function on a natural number (or often we "bump up" so
> > that the domain excludes 0 so that we start at 1 instead of 0). So
> > every entry in the string is indexed by a number, which is the position
> > of that entry in the string. So I can say that in the string
> > ‘xxyzuvwyzux’, we have the substring ‘yzu’ occurring in positions 3-5
> > and 8-10 (except that, technically, the domain of the string ‘yzu’ is
> > not {1 2 3} but rather {3 4 5} and {8 9 10}, and we can "adjust" those
> > back down to {1 2 3}). There are no presuppositions about subsitution
> > so far. Then we pull the whole thing apart, using POSITIONS to keep
> > track of where substrings start and end, then put it all back together
> > (concatenation, which can be rigorously defined) with different values
> > for some of the positions. Still, no presupposition about subsitution.
> Well, you added a little more description here. I need time to study
> it.
> If you don’t mind me asking at this point, what in your opinion
> presupposes comparison?
I don’t know what you mean by ‘presupposing comparision’.
> "The Sprit of Truth" is my favourite chapter of my most favourite book
> ever: A. Hodges, "Alan Turing".
Thanks, I’ll look for that book at the library.
> Well, IMHO, the Church-Turing thesis /holds/ philosophy really tight.
It’s important to my own attempts to make sense of things, for sure!
MoeBlee
(post 1)
- Hide quoted text — Show quoted text -
MoeBlee wrote:
> Your question is roughly the same question I
> was asking myself about a year ago, except my question was not general
> regarding any substrings whatever but rather substrings that are terms
> in formulas or that are subformulas in formulas.
> This is the problem I asked myself about:
> I understand how to recursively define substituting a term for a
> variable in a formula; and I understand how to recursively define
> substituting a formula for a sentence letter in a formula; but I don’t
> know how to define substituting a term for a term in a formula nor
> substituting a formula for a formula in a formula.
> Substituting a term for a variable or a formula for a sentence letter
> is a "many for one" substitution. We substitute a string that may be
> more than one symbol for just a single symbol. That’s easy to define by
> recursion. But substituting a term for a term or a formula for a
> formula is a "many for many" substitution, and I couldn’t figure out
> how to rigorously define that.
> Then I thought that the best approach might not be so direct. Instead
> of directly defining substituting a term for a term, what I did instead
> was to /COMPARE/ two different results of substitutng a term for a
> variable. Suppose I want to substitute the term t’ for the term t in
> the formula P. So I take the formula Q, where Q is just like P except Q
> is "gutted out" so that some variable v occurs where t occurred in P.
> Now, that might be where you think substitution is presumed as we are
> subsituting v for t. But we don’t actually substitute v for t. Rather,
> we reach even further back as if to START with the formula Q so that P
> is Q[t|v]. I know that doesn’t seem right, but if I gave you the full
> technical context, you’d see it actually works out correctly without
> presupposition. So I substitute the term t for the variable v in the
> formula Q (notated as Q[t|v]) and that is actually just the formula P.
> And I substitute the term t’ for the variable v in the formula Q
> (notated as Q[t'|v]). So (with certain other technical restrictions)
> Q[t'|v] is the result of substituting t’ for t in P. Then, by some more
> technical details (such as specifying that v is the first variable that
> does not occur free in P while Q is the unique formula such that P is
> Q[t|v], blah blah blah), we can make this a formal definition. And the
> same method works, mutatis mutandis, for substituting a formula for a
> formula in a formula.
> Notice that this provides for substituting t’ for ALL occurrences of t
> in P. Sometimes we want to allow for substituting t’ for only SOME
> occurences t in P (for example, in stating a theorem schema of identity
> theory, we would want to say that the formulas t=t’ and P together
> imply any formula that is the result of t’ substituted for t in zero or
> more (not necessarily all) places in P). But that too can be formalized
> with yet more technical rigmarole. However, to specify substituting for
> a PARTICULAR occurrence of t requires even more technical rigmarole.
Thank you very much for sharing this, Moe. I spent several hours
pondering it. It is most encouraging to see other people troubling
their heads about the same problems as one does. It is true that this
exactly matches my present endeavours. The word /COMPARE/ used at the
outset, however, IMHO, presupposes substitution, or maybe (as I have
been thinking all this morning) the whole idea of comparison rests or
is even identical to that of isomorphism, or put another way, identity
under given interpretation relation, so that comparison and
substitution are really the same thing.
- Hide quoted text — Show quoted text -
> > > Another method is more general but more complicated (I haven’t gone
> > > through the details myself). Say we want to substitute a string t’ for
> > > a substring t in a string s (t, t’, and s being any strings, not
> > > necessarily terms and formulas). Then we note the positions that t
> > > occupies in s (e.g., in the string ‘xxyzuvwyzux’, the substring ‘yzu’
> > > occupies positions 3-5 and positions 8-10).
> > Here again, we pre-used substring replacement for computing both pairs
> > of numbers. I.e. to determine the position of the target string we need
> > to execute a number of comparisons. Those have to communicate by
> > passing their results to subsequent stages, so substitution is
> > involved, again, IMHO.
> I don’t follow you here. We’re given a string of symbols. A string may
> be regarded as a function on a natural number (or often we "bump up" so
> that the domain excludes 0 so that we start at 1 instead of 0). So
> every entry in the string is indexed by a number, which is the position
> of that entry in the string. So I can say that in the string
> ‘xxyzuvwyzux’, we have the substring ‘yzu’ occurring in positions 3-5
> and 8-10 (except that, technically, the domain of the string ‘yzu’ is
> not {1 2 3} but rather {3 4 5} and {8 9 10}, and we can "adjust" those
> back down to {1 2 3}). There are no presuppositions about subsitution
> so far. Then we pull the whole thing apart, using POSITIONS to keep
> track of where substrings start and end, then put it all back together
> (concatenation, which can be rigorously defined) with different values
> for some of the positions. Still, no presupposition about subsitution.
Again, you used the term /function/ at the outset of the paragraph
above. That, IMHO, is the very presupposition in question. But I _may
very well be mistaken.
Thanks to your kind attention I have clarified my position a lot this
morning. IMHO, the point is, as we have already agreed, haven’t we,
that in any way we end up with a single string. That string needs to be
applied to itself and comparison and substitution are involved _solely.
But the string cannot be grabbed from the inside … but haven’t we
said that /everything/ is in the string already(?) – contradiction.
This is my point. If we supplement the string with some meta-function
we have not improved anything since we still obtain a single string. It
seems that I will only understand it at the point where I am able to
thoroughly appreciate the role of diagonalization in e.g. FOPL
(Goedel/Church/Turing). There is just not enough room for all of its
semantics. The power of its truths is greater than the power of natural
numbers, hence its incomputable.
But that is just my unlearned babbling. I am sorry.
(post 2)
> I don’t know what you mean by ‘presupposing comparision’.
Being defined in terms of?
> > Well, IMHO, the Church-Turing thesis /holds/ philosophy really tight.
> It’s important to my own attempts to make sense of things, for sure!
I want to be frank, so I will speak my mind. IMHO, CTT is very
straightforward and /all/ embracing:
http://britton.disted.camosun.bc.ca/escher/liberation.jpg
I know this is an artistic impression but we’ve been talking about
getting the general idea, or an intuitive understanding of what it all
adds up to. I am 100% THOROUGHLY CONVINCED that this is what it all
adds up to.
Moe, thank you so much for your time.
Kindest regards,
Tom
Tom wrote:
> It is just that little
> part I mentioned that has continued to make me bounce off for several
> months now.
In this context (as opposed to the Post context), substitution is
for supplying arguments to functions, or for applying functions
defined with argument-VARIABLES, TO argument-TERMS.
You have a function definition like F(x,y,z)=df=
‘stuff’x'otherstuff’y'morestuff’z
and you want to know what F(1,2,3) is; you want to substitute 1 for x,
2 for y,
and 3 for z to get F(1,2,3)=’stuff’1′otherstuff’2′morestuff’3.
I have shown the thing on the right, the result, as a string, composed
of other concatenated strings, but in this paradigm, that is NOT the
default composition of things in general. Things in general are TERMS.
They look like p(a,b,c) or s(s(s(0)); they the SAME kind of TREE
structure
that function-applications and predicate-applications have.
These trees do not have to be binary but they can all be re-represented
as binary.
My point is that there is a vast amount of literature in logic and
term-
rewriting involving TERM-substitutions (for variables) as opposed to
substring
substitutions that will accomplish the same objective.
- Hide quoted text — Show quoted text -
george wrote:
> Tom wrote:
> > It is just that little
> > part I mentioned that has continued to make me bounce off for several
> > months now.
> In this context (as opposed to the Post context), substitution is
> for supplying arguments to functions, or for applying functions
> defined with argument-VARIABLES, TO argument-TERMS.
> You have a function definition like F(x,y,z)=df=
> ‘stuff’x'otherstuff’y'morestuff’z
> and you want to know what F(1,2,3) is; you want to substitute 1 for x,
> 2 for y,
> and 3 for z to get F(1,2,3)=’stuff’1′otherstuff’2′morestuff’3.
> I have shown the thing on the right, the result, as a string, composed
> of other concatenated strings, but in this paradigm, that is NOT the
> default composition of things in general. Things in general are TERMS.
> They look like p(a,b,c) or s(s(s(0)); they the SAME kind of TREE
> structure
> that function-applications and predicate-applications have.
> These trees do not have to be binary but they can all be re-represented
> as binary.
> My point is that there is a vast amount of literature in logic and
> term-
> rewriting involving TERM-substitutions (for variables) as opposed to
> substring
> substitutions that will accomplish the same objective.
Yes, George, I understand. Thank you. I was just thinking I am really
trying to establish what Goedel’s Bew(x,y) really is, you know. I mean,
I am trying to reach a single string which incorporates both the
starting sequences and the rules of inference (Bew) from the inside,
which is impossible. But, again, if it is impossible how we do that at
all? I mean, given a TM description and a tape, how do you apply the
description to the tape to obtain another tape. Don’t you need a meta,
and meta-meta, and meta-meta-meta … machine to do that? You do.
Still, we manage to do the thing. How?
Thank you very much for writing.
Tom
- Hide quoted text — Show quoted text -
Tom wrote:
> MoeBlee wrote:
> > Substituting a term for a variable or a formula for a sentence letter
> > is a "many for one" substitution. We substitute a string that may be
> > more than one symbol for just a single symbol. That’s easy to define by
> > recursion. But substituting a term for a term or a formula for a
> > formula is a "many for many" substitution, and I couldn’t figure out
> > how to rigorously define that.
> > Then I thought that the best approach might not be so direct. Instead
> > of directly defining substituting a term for a term, what I did instead
> > was to /COMPARE/ two different results of substitutng a term for a
> > variable. Suppose I want to substitute the term t’ for the term t in
> > the formula P. So I take the formula Q, where Q is just like P except Q
> > is "gutted out" so that some variable v occurs where t occurred in P.
> > Now, that might be where you think substitution is presumed as we are
> > subsituting v for t. But we don’t actually substitute v for t. Rather,
> > we reach even further back as if to START with the formula Q so that P
> > is Q[t|v]. I know that doesn’t seem right, but if I gave you the full
> > technical context, you’d see it actually works out correctly without
> > presupposition. So I substitute the term t for the variable v in the
> > formula Q (notated as Q[t|v]) and that is actually just the formula P.
> > And I substitute the term t’ for the variable v in the formula Q
> > (notated as Q[t'|v]). So (with certain other technical restrictions)
> > Q[t'|v] is the result of substituting t’ for t in P. Then, by some more
> > technical details (such as specifying that v is the first variable that
> > does not occur free in P while Q is the unique formula such that P is
> > Q[t|v], blah blah blah), we can make this a formal definition. And the
> > same method works, mutatis mutandis, for substituting a formula for a
> > formula in a formula.
> > Notice that this provides for substituting t’ for ALL occurrences of t
> > in P. Sometimes we want to allow for substituting t’ for only SOME
> > occurences t in P (for example, in stating a theorem schema of identity
> > theory, we would want to say that the formulas t=t’ and P together
> > imply any formula that is the result of t’ substituted for t in zero or
> > more (not necessarily all) places in P). But that too can be formalized
> > with yet more technical rigmarole. However, to specify substituting for
> > a PARTICULAR occurrence of t requires even more technical rigmarole.
> The word /COMPARE/ used at the
> outset, however, IMHO, presupposes substitution, or maybe (as I have
> been thinking all this morning) the whole idea of comparison rests or
> is even identical to that of isomorphism, or put another way, identity
> under given interpretation relation, so that comparison and
> substitution are really the same thing.
I wasn’t using ‘compare’ in any technical sense there. I was just
talking about a heuristic. In other words, I thought that even though I
couldn’t come up with a way to formulate an operation of substituting a
term for a term in a formula, I could take a workaround. The workaround
is that whenever I need to speak of substituting a term for a term in a
formula, instead I could speak of two separate formulas with a common
dummy variable. And indeed this works for my purposes. Then it occured
to me that I maybe I can also bring that workaround into an explicit
definition of an operation of substituting a term for a term in a
formula. As I mentioned, for a formula P and terms t’ and t, we could
define "the result of substituting t’ for t in P" as "P if t does not
occur in P; and Q[t'|v] where v is the first variable that is in not in
P, t, or t’, and Q is the unique formula such that P is Q[t|v], if t
occurs in P". If I’m not mistaken, all that it would take to make that
airtight is proving that there is such a unique Q (which I don’t think
would be a problem?).
> Again, you used the term /function/ at the outset of the paragraph
> above. That, IMHO, is the very presupposition in question. But I _may
> very well be mistaken.
For my own study, I regard all of the formulation of syntax for object
languages as definitions in a formal meta-theory (which is Z set
theory). So I take a string to be, set theoretically, a certain kind of
function.
> Thanks to your kind attention I have clarified my position a lot this
> morning. IMHO, the point is, as we have already agreed, haven’t we,
> that in any way we end up with a single string. That string needs to be
> applied to itself
I don’t know what you mean by ‘applied to itself’.
My own study just procedes from the axioms of set theory using first
order logic. (Of course, there is an infinite escalation of
meta-theory, since I’m using a formal meta-theory to study formal
object languages and object theories; so my formal meta-theory would
require a formal meta-meta-theory, ad infinitum. But I cut that
escalation at the meta-meta-theory by taking the meta-meta-theory to be
infomal but in principle formalizable but not necesssary to formalize
since such formalization would just be a "clone" of the formalization
I’ve already accomplished in the meta-theory. I take further escalation
to be a kind of "successor" operation. Once you’ve formalized one
meta-theory, then you know just what it is involved in formalizing the
next level up – just go through all the formalization of the
meta-theory, but regard it as being one level up, like taking a
"successor level". Or, a more relaxed notion is just to say, "Look,
it’s got to stop somewhere. I stop by taking the meta-meta theory to be
informal but using, informally, just the very reasonable principles
I’ve formalized in the meta-theory.")
> I want to be frank, so I will speak my mind. IMHO, CTT is very
> straightforward and /all/ embracing:
The Church-Turing thesis is crucial for my understanding, but I don’t
know in what sense it is "all embracing".
> http://britton.disted.camosun.bc.ca/escher/liberation.jpg
> I know this is an artistic impression but we’ve been talking about
> getting the general idea, or an intuitive understanding of what it all
> adds up to. I am 100% THOROUGHLY CONVINCED that this is what it all
> adds up to.
Hmm, okay. Escher’s art is illuminating. But I don’t know that it is
what our intuitions "all add up to".
MoeBlee
MoeBlee wrote:
> I wasn’t using ‘compare’ in any technical sense there. I was just
> talking about a heuristic.
I see.
> In other words, I thought that even though I
> couldn’t come up with a way to formulate an operation of substituting a
> term for a term in a formula, I could take a workaround. The workaround
> is that whenever I need to speak of substituting a term for a term in a
> formula, instead I could speak of two separate formulas with a common
> dummy variable.
Yes. I understood that.
> And indeed this works for my purposes. Then it occured
> to me that I maybe I can also bring that workaround into an explicit
> definition of an operation of substituting a term for a term in a
> formula. As I mentioned, for a formula P and terms t’ and t, we could
> define "the result of substituting t’ for t in P" as "P if t does not
> occur in P; and Q[t'|v] where v is the first variable that is in not in
> P, t, or t’, and Q is the unique formula such that P is Q[t|v], if t
> occurs in P". If I’m not mistaken, all that it would take to make that
> airtight is proving that there is such a unique Q (which I don’t think
> would be a problem?).
For me it would be, I am afraid.
> > Again, you used the term /function/ at the outset of the paragraph
> > above. That, IMHO, is the very presupposition in question. But I _may
> > very well be mistaken.
> For my own study, I regard all of the formulation of syntax for object
> languages as definitions in a formal meta-theory (which is Z set
> theory). So I take a string to be, set theoretically, a certain kind of
> function.
OK.
> I don’t know what you mean by ‘applied to itself’.
I don’t either. Say, we have a linear TM description and a tape. What
exactly is the process of executing the first state and passing control
to other states? _This is my question. Is the formalization of this
execution process equivalent to the formalization of Bew(x,y)?
> My own study just procedes from the axioms of set theory using first
> order logic. (Of course, there is an infinite escalation of
> meta-theory,
That’s it. Does it apply to what I am asking about? (Please see
above.) Am I really after Bew?
> since I’m using a formal meta-theory to study formal
> object languages and object theories; so my formal meta-theory would
> require a formal meta-meta-theory, ad infinitum.
Yes. Precisely. Bew causes these problems, doesn’t it? And it seems
most likely that this is my present problem, to find Bew. Is it?
> But I cut that escalation at the meta-meta-theory by taking
> the meta-meta-theory to be infomal
Precisely! Since I am not in a position to say that, I did not say
that. Please, is there an honest text which discusses this?
> but in principle formalizable but not necesssary to formalize
Yes, exactly.
> since such formalization would just be a "clone" of the formalization
> I’ve already accomplished in the meta-theory. I take further escalation
> to be a kind of "successor" operation.
Right.
> Once you’ve formalized one meta-theory,
But you can’t /really/ since you need the meta-meta-theory. And because
you don’t have the meta-meta-theory you use the workaround to be
clarified subsequently.
> then you know just what it is involved in formalizing the
> next level up – just go through all the formalization of the
> meta-theory, but regard it as being one level up, like taking a
> "successor level". Or, a more relaxed notion is just to say, "Look,
> it’s got to stop somewhere. I stop by taking the meta-meta theory to be
> informal but using, informally, just the very reasonable principles
> I’ve formalized in the meta-theory.")
Yes. But this is professional talk, Moe. I am levels down.
A simple question, if I may. Given the TM problem I described above, is
Bew what I am really after? I mean, if I know what I am looking for, I
can start looking. Just that, please, am I after Bew?
> The Church-Turing thesis is crucial for my understanding, but I don’t
> know in what sense it is "all embracing".
(OK, I really have my back on the well here.) Everything else is utter
rubbish. And, please, don’t make me say more, because I will.
> Hmm, okay. Escher’s art is illuminating. But I don’t know that it is what our intuitions "all add up to".
IMHO, Escher’s art adds up to Goedel’s results, i.e. the problems in
defining Bew.
Thank you for writing again, Moe.
Tom
Please, is my problem finding Bew?
If I had a kind confirmation I would be set until the last page of
Boolos&Jeffrey. And this is just three letters. May I, please, ask for
the three letters?
Please,
Tom
Tom wrote:
>I was just thinking I am really
> trying to establish what Goedel’s Bew(x,y) really is, you know.
It’s just a defined binary first-order predicate.
In Godel’s original it was in the language of PM but
for our purposes it would be in the first-order language of
Peano Arithmetic. If you use FOL with equality and 1 instead of s(.)
then this is a VERY simple language; its only terms are 0 and 1
and what you can build from them with + and x . It doesn’t have
or need any predicates at all (since = is already built-in).
But because that makes most statements in it every bit as
unreadable as machine language (compiled into 0′s and 1′s),
there is a mechanism for adding DEFINED predicates and functions.
E.g. less(x,y)<=df=>Ez[(x+1)+y=z], or
prime(x)<=df=>Ayz[ less(y,2)v less(z,2)v less(x,y)v less(x,z)v
~(y*z=x)]
Just as prime is defined in terms of less, here Bew is defined in terms
of a high tower of other things that were defined earlier. But it is a
NUMERIC
function. Strings are NOT actually involved here except to the extent
that
(1 + (1 + (1+ (1 + 0 )))) is a string (which it isn’t, actually; it’s a
term).
> I mean, I am trying to reach a single string which incorporates both the
> starting sequences and the rules of inference (Bew) from the inside,
You don’t have to "reach" Bew; it was already defined in Godel.
> which is impossible.
Given that it’s been done, it can hardly be impossible, unless you are
saying
that it was done in some non-string way, and what you are trying to do
is
translate it into a string. But again, the framework is PA, is
NUMBERS, NOT
strings. Why would you be trying to redo FOL where the whole framework
is strings and not terms? Aren’t terms plenty string-like enough
already?
If you can finesse the difference between a character and a
string-of-length-1,
you can already articulate some simple axioms about how strings work.
> But, again, if it is impossible how we do that at all?
I’m losing your antecedents of "it" and "that" here.
> I mean, given a TM description and a tape, how do you apply the
> description to the tape to obtain another tape. Don’t you need a meta,
> and meta-meta, and meta-meta-meta … machine to do that?
Well, no, me, personally, I don’t. I can just look at it.
> You do.
No, I don’t. The fact that there is a TM that can confirm for me
that the string II concatenated with the string III yields the string
IIIII
does NOT mean that I *need* this TM *before* I can do that.
*My* brain is Turing-equivalent modulo finitude (despite the
fact that Turing was a lot smarter than I am).
More to the point, mathematical functions in general don’t "need"
a TM-implementation *before* they can operate; they just operate
on their arguments and produce the results they produce from them.
Instantaneously. For all arguments. IN PARALLEL. IN AETERNAM.
> Still, we manage to do the thing. How?
I didn’t realize how old your question was.
In the popular literature, this question occurs in
Hofstadter’s "Godel, Escher, Bach" in the context of
how we determine that inference rules are sound.
If we know P is non-contradictory, if we know
P-Q is true, and we know modus ponens is sound,
then, yes, we can infer Q, but how do we know that
all the machinery we used in making THAT inference was sound?
We can prove by truth-tables that
If we have P, and we have P->Q, then we can infer Q.
But how do we know that the truth-table method is sound?
Don’t we need some further justification for that?
Hofstadter is continuing a thread begun by Lewis Carroll
in "What the Tortoise Said to Achilles" some 80 years prior.
If you have children then one of them may at some point
around age 4 have gotten into the habit, once you
gave an explanation in response to a question of type
"Why?", of iterating the question: "Why?"
There is in principle no end of that.
That is what AXIOMS are for.
At some point you can have to be able to say that
you can tell ad oculos, by inspection, that something
matches a pattern that makes it acceptable by fiat,
just because we said so, just because we agreed NOT
to seek DEEPER justification for things of THAT shape.
This raises 2 concerns. Either 1) we might be mistaken
in recognizing the thing as matching the pattern (this is
why axiom-sets have to be recursive, and why proof-predicates
have to be PRIMITIVE-recursive), or 2) the reasoning might
actually BE unsound and might lead us to accept something
contradictory. In the case of first-order logic we rebut this
objection by simply pointing out that since it is complete
(the LOGIC, NOT a rich theory IN it) and since first-order
consequence is r.e., then if we have accepted something that
entails a contradiction, WE CAN PROVE that eventually, and
thus evolve away from the contradiction.
The problem in any case is NOT about "producing" strings or tapes.
TMs are thought of as just "having" their programs inside them
somewhere, as you might know the recipe for baking a cake.
The fact that the recipe can also be written down in a cookbook
does NOT imply that you have to know how to read before you can
know how to bake a cake.
- Hide quoted text — Show quoted text -
Lee Rudolph wrote:
> Recently in sci.math, in a thread with Subject: "question about
> Cartesian products", agapito6…@aol.com asked:
> > Given sets X, Y, and Z, let
> > A = X x (Y x Z) and B= (X x Y) x Z
> and wondered if there were any examples in which A = B are non-empty
> and equal. Dave Renfro showed that the existence of such an example
> is inconsistent with the Axiom of Foundation. Yesterday I noticed
> (I hope, correctly) that, in ZF-Foundation+Aczel’s Axiom of Anti-Foundation,
> the (unique) set X such that X = {X} is a non-empty Cartesian idemopotent
> (that is, X = X x X, where I am using–maybe inappropriately–the
> fairly standard definitions A x B = {(a,b) | a in A, b in B} and
> (a,b) = {{a}, {a,b}}, so that in particular (a,a) = {{a}} for any a),
> whence X x (X x X) = (X x X) = X.
> This makes me wonder how much daylight there is between the two
> results. In particular (what seems unlikely), is the Axiom of Foundation
> actually equivalent to the non-existence of non-empty Cartesian idempotents?
> More generally, are there any (other?) interesting equivalents of the
> Axiom of Foundation, as there are certainly many interesting equivalents
> of the Axiom of Choice?
> I beg the pardon of sci.logic if this is something everyone knows or
> should know. My entire stock of knowledge of logic is not much larger
> than the quoted fact about Aczel’s Axiom of Anti-Foundation, gleaned from
> an interested but inattentive skimming of a book by Barwise and Wozzname
> several years ago. I’m just slumming here.
> Lee Rudolph
This may come as a shock to you, but assuming the ZF except the axiom
of foundation, the axiom of choice is equivalent to the axiom of
foundation.
lugit…@gmail.com wrote:
> This may come as a shock to you, but assuming the ZF except the axiom
> of foundation, the axiom of choice is equivalent to the axiom of
> foundation.
Well that comes as a shock to me. Reference?
Peter_Smith wrote:
> lugit…@gmail.com wrote:
> > This may come as a shock to you, but assuming the ZF except the axiom
> > of foundation, the axiom of choice is equivalent to the axiom of
> > foundation.
> Well that comes as a shock to me. Reference?
http://en.wikipedia.org/wiki/Axiom_of_regularity
lugit…@gmail.com wrote:
> Peter_Smith wrote:
> > lugit…@gmail.com wrote:
> > > This may come as a shock to you, but assuming the ZF except the axiom
> > > of foundation, the axiom of choice is equivalent to the axiom of
> > > foundation.
> > Well that comes as a shock to me. Reference?
> http://en.wikipedia.org/wiki/Axiom_of_regularity
That doesn’t say that AC is equiv to AF, only that two versions of AF
)
are equivalent given AC. On a hurried read
Peter_Smith wrote:
> lugit…@gmail.com wrote:
> > Peter_Smith wrote:
> > > lugit…@gmail.com wrote:
> > > > This may come as a shock to you, but assuming the ZF except the axiom
> > > > of foundation, the axiom of choice is equivalent to the axiom of
> > > > foundation.
> > > Well that comes as a shock to me. Reference?
> > http://en.wikipedia.org/wiki/Axiom_of_regularity
> That doesn’t say that AC is equiv to AF, only that two versions of AF
)
> are equivalent given AC. On a hurried read
It says "Hence, in the view of the other axioms, the two axioms are
equivalent."
- Hide quoted text — Show quoted text -
lugit…@gmail.com wrote:
> Peter_Smith wrote:
> > lugit…@gmail.com wrote:
> > > Peter_Smith wrote:
> > > > lugit…@gmail.com wrote:
> > > > > This may come as a shock to you, but assuming the ZF except the axiom
> > > > > of foundation, the axiom of choice is equivalent to the axiom of
> > > > > foundation.
> > > > Well that comes as a shock to me. Reference?
> > > http://en.wikipedia.org/wiki/Axiom_of_regularity
> > That doesn’t say that AC is equiv to AF, only that two versions of AF
)
> > are equivalent given AC. On a hurried read
> It says "Hence, in the view of the other axioms, the two axioms are
> equivalent."
It was badly written but meant: the axiom of regularity and the claim
that there are no infinite downward chains are equivalent in the light
of the other axioms (including AC).
I’ve corrected it.
) AC and AF are not equivalent!
lugit…@gmail.com wrote:
>This may come as a shock to you, but assuming the ZF except the axiom
>of foundation, the axiom of choice is equivalent to the axiom of
>foundation.
That certainly is shocking. Especially since ZF (including
Foundation) + not AC is well-known to be consistent.
Hmm, I guess that means that ZF + AC + not AC is consistent… Oh,
no! All of mathematics has collapsed! So much for this newsgroup…
–
Stephen J. Herschkorn sjhersc…@netscape.net
Math Tutor on the Internet and in Central New Jersey and Manhattan
I wrote:
> lugit…@gmail.com wrote:
>> This may come as a shock to you, but assuming the ZF except the axiom
>> of foundation, the axiom of choice is equivalent to the axiom of
>> foundation.
> That certainly is shocking. Especially since ZF (including
> Foundation) + not AC is well-known to be consistent.
> Hmm, I guess that means that ZF + AC + not AC is consistent… Oh,
> no! All of mathematics has collapsed! So much for this newsgroup…
Correction: It is well-known that if ZF is consistent, then so is ZF +
not AC. I guess what we have here is a proof that ZF is not consistent.
Oh, well. Back to the drawing board.
–
Stephen J. Herschkorn sjhersc…@netscape.net
Math Tutor on the Internet and in Central New Jersey and Manhattan
- Hide quoted text — Show quoted text -
Stephen J. Herschkorn wrote:
> I wrote:
> > lugit…@gmail.com wrote:
> >> This may come as a shock to you, but assuming the ZF except the axiom
> >> of foundation, the axiom of choice is equivalent to the axiom of
> >> foundation.
> > That certainly is shocking. Especially since ZF (including
> > Foundation) + not AC is well-known to be consistent.
> > Hmm, I guess that means that ZF + AC + not AC is consistent… Oh,
> > no! All of mathematics has collapsed! So much for this newsgroup…
> Correction: It is well-known that if ZF is consistent, then so is ZF +
> not AC. I guess what we have here is a proof that ZF is not consistent.
> Oh, well. Back to the drawing board.
> —
> Stephen J. Herschkorn sjhersc…@netscape.net
> Math Tutor on the Internet and in Central New Jersey and Manhattan
It is also known (Robert Vaught’s book on set theory gives a reference
to references-he says due to Bernays) that in ZFC but without
Foundation (= the Axiom of regularity) that it is not possible to prove
Foundation.regards,smn
On 24 Sep 2006 17:20:14 -0700, smn wrote:
- Hide quoted text — Show quoted text -
> Stephen J. Herschkorn wrote:
>> I wrote:
>> > lugit…@gmail.com wrote:
>> >> This may come as a shock to you, but assuming the ZF except the axiom
>> >> of foundation, the axiom of choice is equivalent to the axiom of
>> >> foundation.
>> > That certainly is shocking. Especially since ZF (including
>> > Foundation) + not AC is well-known to be consistent.
>> > Hmm, I guess that means that ZF + AC + not AC is consistent… Oh,
>> > no! All of mathematics has collapsed! So much for this newsgroup…
>> Correction: It is well-known that if ZF is consistent, then so is ZF +
>> not AC. I guess what we have here is a proof that ZF is not consistent.
>> Oh, well. Back to the drawing board.
>> —
>> Stephen J. Herschkorn sjhersc…@netscape.net
>> Math Tutor on the Internet and in Central New Jersey and Manhattan
> It is also known (Robert Vaught’s book on set theory gives a reference
> to references-he says due to Bernays) that in ZFC but without
> Foundation (= the Axiom of regularity) that it is not possible to prove
> Foundation.regards,smn
Assuming ZFC-Foundation is consistent.
–
Dave Seaman
U.S. Court of Appeals to review three issues
concerning case of Mumia Abu-Jamal.
<http://www.mumia2000.org/>
In article <1159066200.634637.49…@m7g2000cwm.googlegroups.com>,
<lugit…@gmail.com> wrote:
>Lee Rudolph wrote:
>> Recently in sci.math, in a thread with Subject: "question about
>> Cartesian products", agapito6…@aol.com asked:
……………….
>This may come as a shock to you, but assuming the ZF except the axiom
>of foundation, the axiom of choice is equivalent to the axiom of
>foundation.
This is false. The axiom of foundation, and also its
negation, are independent of the axiom of choice.
–
This address is for information only. I do not claim that these views
are those of the Statistics Department or of Purdue University.
Herman Rubin, Department of Statistics, Purdue University
hru…@stat.purdue.edu Phone: (765)494-6054 FAX: (765)494-0558