Re: Computability and logic

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

.

Relevant Pages

  • Re: Computability and logic
    ... couldn't come up with a way to formulate an operation of substituting a ... languages as definitions in a formal meta-theory (which is Z set ... execution process equivalent to the formalization of Bew? ... Am I really after Bew? ...
    (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)
Loading