Re: Computability and logic

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.

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

.

Relevant Pages

  • Re: Computability and logic
    ... say v (which is a string of exactly one ... substring replacement) to be predefined. ... substituting a formula for a sentence letter in a formula; ... to come to grips with such technicalities as rigorous definitions for ...
    (sci.logic)
  • Re: Computability and logic
    ... say v (which is a string of exactly one ... substring replacement) to be predefined. ... substituting a formula for a sentence letter in a formula; ... to come to grips with such technicalities as rigorous definitions for ...
    (sci.logic)
  • Re: My investigations into Godels Incompleteness Theorem
    ... The result of substituting "The result of substituting x for 'x' in ... The number of characters in the string x is 52. ... The number of characters in the string "abcdefg" is 52. ... and perform a diagonalization, we get the string ...
    (sci.logic)
  • Re: My investigations into Godels Incompleteness Theorem
    ... The result of substituting "The result of substituting x for 'x' in ... The number of characters in the string x is 52. ... The number of characters in the string "abcdefg" is 52. ... and perform a diagonalization, we get the string ...
    (sci.logic)
  • Re: My investigations into Godels Incompleteness Theorem
    ... The result of substituting "The result of substituting x for 'x' in ... The number of characters in the string x is 52. ... The number of characters in the string "abcdefg" is 52. ... and perform a diagonalization, we get the string ...
    (sci.logic)
Loading