Infinitely long statements (a proof)

This post addresses a point raised in the previous post: Is there a set of noncomputable but grammatical strings that are inherently impossible to cryptanalyze?

Again, we are assigning a digit to each symbol in some logic language (agreeing to first make sure we start out with a sufficiently high base number system). A string of digits then represents a string of symbols.

A grammatical string of symbols is one whereby certain substrings are barred as ungrammatical. But this does not mean we rule out logical contradictions or "false" statements. For example the string (A and not-A) is permitted. However, we see that the set of all proofs (defining proof as a statement verifying another statement) is a subset of our set of grammatical strings.

Whether an infinitely long grammatical string represents a proof, or a true or false, or undecidable, statement is a matter of philosophical preference.

But, to the matter at hand:

Can an infinitely long string be noncomputable but grammatical? The answer depends on the "reasonableness" of the grammatical rules. Note that in routine first-order logic notation our biggest concerns as to grammar are the right and left parentheses. If we had a set of 30 symbols, we would still have nearly 28 random choices for step n+1. So let's be generous and suggest that for language L, half the symbol set is disallowed.

[Note: I have been told that there is a proof that some such strings are satisfiable (have a truth value) and that others are undecidable.]

Now, using Zermelo-Frankel set theory's infinity axiom to permit use of induction, we consider the set of all n-length strings of base K digits (there are K^n strings).
By induction we see that we obtain the set of all possible strings, and this must be bijective with the set of reals.

Now suppose we add the proviso that at any n, we permit only (K^n)/2 strings. Yet by the ZF infinity axiom and induction we obtain half the reals, which is still a nondenumerable infinity. Since the computables have a denumerable cardinality, there must be a nondenumerable set of noncomputable but grammatical strings.

However, for grammatical rules that increasingly limit the number of choices for n, this theorem is not valid.

Related pages by Conant:
http://www.angelfire.com/az3/nfold/diag.html
http://www.angelfire.com/az3/nfold/choice.html
http://www.angelfire.com/az3/nfold/qcomp.html