Re: Computability and logic

(post 1)

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.

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

.

Relevant Pages

  • Re: Computability and logic
    ... as regards a mathematical formulation of a substring ... substring in a string with another substring? ... result of substituting a term for a variable in a formula'. ... As I recall, he doesn't get into replacing term for term, ...
    (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: Computability and logic
    ... Moe, I include both of your kind posts here for convenience. ... say v (which is a string of exactly one ... substring replacement) to be predefined. ... result of substituting a term for a variable in a formula'. ...
    (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)