infinitary structures

[RE01 Rice Brian T. EM2]

well, before i introduce a bunch of new operators to flesh out the arrow
language, i guess i'd better tackle the monster to which i've repeatedly
referred: the infinity 'barrier'.

in the theory of computation, we have finite-state machines, Turing
machines, languages with varying grammar extents (regular vs context-free
and context-sensitive), lots of first-order languages and fragments, and
many-sorted first-order languages.  the arrow language is designed to
trascend these ideas.  the boundary of the arrow language needs to exceed
all of these.

a simple way to express this is that we have the goal of expressing at least
a countable number of types within this language, remembering of course that
just about everything imaginable is available for first-order analysis, even
_without_ reflection.  instead of a many-sorted language, our (for now)
pseudo-reflective language will be infinitely sorted.  this system is
designed to encode all kinds of reasoning systems and procedural-logic so
that it can reflect on what it does as well as what it is.

the only results that i have so far for expressing an infinite number of
things is rather weak: axiomatic specification.  with axiomatic
specification, the _number_ of things referred to is irrelevant,
theoretically.  in actuality, it of course matters a great deal if the
axiomatization gives:
	0,
	1,
	a finite linearly-calculable number,
	an NP-hard (or NP-complete) calculable number,
	a countable number (as many as the natural numbers),
	or any of the uncountable quantities of numbers of solutions.

even this description fails to account for undecidable or undefinable
numbers of 'solutions' to our 'equational axioms', to take an analogy.

well, probably a good place to start chiseling at this problem  would be
where Godel and Church started: at the countable level and at the decidable
level.  basically, for countability, we probably would need a good arrow
description of a general finite-state machine and describe the
transformations which yield (all?) equivalent machines.  this would tell us
if simple iteration would terminate on some procedure, which is obviously
useful in procedural logic and type checking for recursive enumerability.
this also seems very simple to do without resorting to infinitary measures.
now, i know that standard first-order predicate logic has been proven not to
be able to distinguish the number of natural numbers from uncountable
structures, so this system will probably look very unorthodox.  this seems
like a good viewpoint to start from, and i will add to it in the next post.

for decidability, we would have to look both at the axioms and the logical
symbols of the system within which the axioms are based.  i happen to have
some papers which ask such questions about logical systems, particularly
several nuances associated with logical operators within various arrow
systems, and i have to admit that most of the work involves simply coming up
with an intuitive understanding of the meaning of these symbols, so that i
understand the limits of the system.