What does Kx mean in this equation? [in Carnap or Russell and Whitehead's logical notation]

Question

Hope this is the right forum for this. I am reading a seminal "mathematical biophysics" paper from 1943 by MucCulloch and Pitts, and I got into a little bit of a rabbit hole trying to understand this equation in old-style logical notation.

This is the equation in question:

By following this link, I think I got most of it figured out, and I'm assuming x’) means "predecessor of x", and so the equation should be read as something like "The property S(P) holds for t if and only if P holds for Kx and t is the predecessor of x? But what does Kx mean? Doesn't this equation fulfill the definition if Kx were just replaced by x in the definition?

Thanks for any guidance on this!

Answer 1

As you can see in the References, R.Carnap (1938) is :

Rudolf Carnap, Logical Syntax of Language, Routledge (German ed.1934; 1st English ed.1937).

Language II is Carnap's versione of W&R's Principia theory of types.

The K-operators correspond to the bounded and unbounded $\mu$-operator.

The definitional axiom (it is a contextual definition) for the bounded one is (in slightly modernized symbols) :

$G(Kx_{x \le y}[F(x)]) \leftrightarrow [ (\lnot (\exists x)_{x \le y}[F(x)] \land G(0)) \lor (\exists x)_{x \le y} (F(x) \land \forall z_{z \le x} [\lnot (z=x) \to \lnot F(z)] \land G(x))].$

Thus, $(Kx)y[F(x)]$ reads : "$\text {the least (natural) number } x \text { less-equal to } y \text { such that } F$".

In the same way, $(Kx)[F(x)]$ reads: "$\text {the least (natural) number } x \text { such that } F$".

---

If so, the expression:

$S(P)(t) \equiv P(Kx) (t=x'),$

where $S$ is a functor that applies to properties, reads:

"$S(P)$ is a property that holds for (number) $t$ if and only if the property $P$ holds for the least number $x$ that is the predecessor of $t$ [$t=x'$ means that $t$ is the successor of $x$]".