I many times encountered the concept of soundness and completeness in proof related articles, such as type system, logic. description of these two concepts in logic
I had a discussion recently and that appeared again, but in a topic related to $lambda$-calculus. I could not imagine these two concepts in $\lambda$-calculus as clear as the above link description of their meaning.
Note that I know the soundness and completeness of the type systems. I am asking in terms of untyped $\lambda$-calculus. Could anyone point out any good article about it or explain to me. Thanks in advance.