From: zeleny@scws7.harvard.edu (Michael Zeleny)
Newsgroups: sci.math,comp.theory,sci.logic
Subject: Self-Reference and Coding
Date: 1 Jan 93 17:27:44 GMT
Organization: The Phallogocentric Cabal

Consider a formula in the language of Robinson Arithmetic.  Ask the
question whether it is self-referential, in the sense of containing a
term which encodes it via some scheme of G\"odel numbering.  To what
extent can this question be answered, effectively or otherwise?

Motivation: assume a compositional intensional semantics, i.e. an
ontology of concepts for all constants and formulae.  The fundamental
rule is that the concept of a formula is an appropriate function on
the concepts of its terms.  Example: for $1+1=2$ (pardon my TeX, --
the dollar sign is a math delimiter), have the concept $1_1 +_1 1_1
=_1 2_1$, where the subscript 1 indicates the first concept of each
thing, whether individual, function, or relation.  Agree to omit
subscripts from function and relation constants, -- they can be
restored from the context.  We say that terms and formulae express
their concepts; the concept of a formula is also called a proposition.

Define a relation of synonymy, which partitions the concepts into
equivalence classes, and induces a Lindenbaum algebra of the
corresponding sentences, to be that of logical equivalence.  (This is
Church's Alternative (2); another notion of synonymy is given by the
Alternative (1), which takes \lambda-convertibility as its definition.
Since the language is typed, the latter relation is decidable.)  So,
for instance, $1_1+1_1$ is synonymous with $2_1$ as concepts of the
integer 2.  Unfortunately, this means that the synonymy relation is
undecidable, inasmuch as our language may allow us to express the same
concept via such rocky roads as the Goldbach conjecture or Fermat's
last theorem.

Now, to exclude G\"odel-type sentences, I stipulate that a necessary
condition for a concept to be meaningful, is that it not contain any
well-formed constituents synonymous with itself.  Note that this is
precisely the intensional analogue of the set-theoretic Axiom of
Foundation, which ensures that all meaningful concepts may be assigned
a rank in the cumulative hierarchy of concepts. Thus, in particular,
the sentences $\psi$, for which $$\psi \equiv \neg \mbox{Pr}_{\cal
Q}(\lceil \psi \rceil),$$ (incidentally, what is the proper AMS LaTeX
symbol for corner quotes?) that is, such that they are materially
equivalent to the sentence denying the provability in Robinson
arithmetic of the sentence with their G\"odel number, are deemed
meaningless.  Since nothing depends on the negation, the L\"ob
sentences, which assert their own provability, are likewise excluded.
All meaningless sentences (i.e. ones not expressing a meaningful
concept) are regarded as bereft of truth-values.  All formal proofs
are required to be valid, i.e to contain only meaningful formulae.
Now say that synonymy is *provable* logical equivalence, and
reconstrue the above accordingly.

In accordance with the above considerations, this means that
meaningfulness is not an effectively decidable notion.  (Gerald Sacks
says that Church tried what sounds like a similar approach towards
analyzing G\"odel's results.  I am unaware of any published work, so
references would be greatly appreciated.)  However, it appears to be
semi-decidable.  What else can be said about this notion?

Happy New Year to all.

cordially,
mikhail zeleny@husc.harvard.edu
"Les beaulx bastisseurs nouveaulx de pierres mortes ne sont escriptz
en mon livre de vie.  Je ne bastis que pierres vives: ce sont hommes."