0

In Enderton, Section 2.3, to prepare to prove Unique Readability for the wffs in FOL he proves a series of Lemmas involving a function K. On pg. 105 says the following about $K$:

"Recall that the terms are built up from the variables and constant symbols by operations corresponding to the function symbols. We now define a function $K$ on the symbols involved such that for a symbol $s$, $K(s)=1-n$, where $n$ is the number of terms that must follow $s$ to obtain a term:

  • $K(x)=1-0=1$ for a variable $x$;
  • $K(c)=1-0=1$ for a constant symbol $c$;
  • $K(f)=1-n$ for an $n$-place function symbol $f$."

He then sketches inductive proofs for general claims like: For any term $t$, $K(t)=1$.

Before attempting to flesh out this proof, I am having trouble understanding $K$. Take for example a 1-place function like the successor function $S$. Since $S$ is 1-place, by the above definition isn't $K(S)=1-1=0$. In contrast, take a 2-place function like $+$. Again, since $+$ is 2-place, by the above definition, $K(+)=1-2=-1$. What information do I get from the values of $K$?

Is it that by solving for $n$, I am told how many terms need to follow $s$ in order to get a term, i.e. so that $K(s)=1$?

beachtrees
  • 209

1 Answers1

0

Intuitively, $K(f)=1-n$ signals a need for $n$ terms, whereas $K(x)=1$ signals a supply of one term. In the end, you want to reach the number $1$, meaning that all demands have been met.

More formally, given a sequence $$ s_1 s_2 \ldots s_n $$ of symbols, parse the sequence from left to right while computing partial sums $$K(s_1)\;,\; K(s_1)+K(s_2)\;,\;\ldots\;,\;\sum_{i=1}^n K(s_i).$$ Then $s_1 s_2\ldots s_n$ is a well-formed term iff the lower sequence ends with $1$ and all previous numbers are $<1$.

For $m<n$, the number $\sum_{i=1}^m K(s_i)=1-k$ tells you that $k$ further terms have to be supplied as arguments to the function symbols in $s_1\ldots s_m$ until you obtain a well-formed expression.

E.g. given a binary function symbol $f$ ($K(f)=-1$) and a variable $x$ ($K(x)=1$), parsing the sequence $$ ffxxx $$ of symbols yields the sequence of partial sums $$ -1,-2,-1,0,1 $$ and so you do have a well-formed term, namely $f(f(x,x),x)$. The third number $-1 = 1-2$ in the list says that in $ffx$, there are still $2$ terms missing (namely, both the outer and the inner $f$ lack their second argument).

Timo
  • 1,059