I am trying to validate the simplest possibly notion of a formal system as relations between finite strings. I know that Lambda Calculus has the expressive power of a Turing Machine:
<λexp> ::= < var > | λ . <λexp> | ( <λexp> <λexp> )
I was thinking that it might be possible so somehow convert the functionality of lambda calculus into syntax that is closer to predicate logic by defining named functions that take finite string arguments and return finite string values.
Since we already know that Lambda Calculus is Turing complete we might see if Lambda calculus syntax could be specified more generically as functions taking finite string arguments that evaluate to finite strings.