0

I want to show that

$$ S^{m} \underline{n} = \underline{n+m} $$

where $S$ is successor function and $\underline{m},\underline{n}$ are Church numerals. Note that $S^m (x) = \underbrace{S(S(..(S}_\text{m-times}x)..))$. Also successor function S is defined: $S(\underline{n}) = \underline{n+1}$.

Here's my try:

$$ S^{m} \underline{n} = (\lambda nfx. \underline{m} f (nfx)) \underline{n} = \lambda fx. \underline{m} f (\underline{n} fx) = \lambda fx. f^m (f^n x) = \lambda fx. f^{n+m} x = \underline{n+m} $$

$\square$

Are the steps correct and reasonable? Thanks a bunch!

Logan Lee
  • 249
  • 1
    What does the underscore mean? What is $f$? Also, I suspect induction would be better to use – whoisit Nov 16 '22 at 06:46
  • @whoisit i did it by using definition of successor function S. – Logan Lee Nov 16 '22 at 06:50
  • 2
    The steps look reasonable, though I can't tell whether you have theorems/definitions for each intermediate step available. – 8bc3 457f Nov 16 '22 at 06:52
  • 1
    The description of $S$ which you give, is not well-formed, because in $S:n\to n+1$ we expect $n$ and $n+1$ to be sets, which they aren't... – 8bc3 457f Nov 16 '22 at 06:55
  • @8bc3457f ok. i just wanted to hastily define it so readers know what it does. – Logan Lee Nov 16 '22 at 06:56
  • 1
    Your correction is still wrong. The arrow is the problem. The notation $f: A\to B$ for a function $f$ specify its domain and codomain as being $A$ respectively $B$. In your case it'd be better to use something like $S(\underline{n})=\underline{n+1}$ or since we're in lambda-calculus, $S\underline{n}=\underline{n+1}$. – 8bc3 457f Nov 16 '22 at 07:01
  • @8bc3457f ok. i'll fix it now. – Logan Lee Nov 16 '22 at 07:02
  • @8bc3457f yes i can provide definitions used. – Logan Lee Nov 16 '22 at 07:17

0 Answers0