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.

  • $\begingroup$ If you are looking for a formally simple system, did you look at combinatorial logic? $\endgroup$ – Emil Jeřábek supports Monica Sep 13 at 6:15
  • $\begingroup$ @EmilJeřábek I am looking to define the base class of the generic notion of a formal system such that every formal system that could possibly exist would inherit its common functionality from this single base class. I am doing this from the mathematical formalist perspective of finite string manipulation rules. $\endgroup$ – polcott Sep 13 at 14:02
  • $\begingroup$ One possible formal system is the empty one... $\endgroup$ – Andrej Bauer Sep 13 at 19:05
  • $\begingroup$ @AndrejBauer if we define formal systems as relations between finite strings that formal system would have the single relation of the empty string. $\endgroup$ – polcott Sep 13 at 19:08
  • $\begingroup$ How about a function taking two strings represented by church-encoded lists of church encoded letters and returning church-encoded boolean? $\endgroup$ – Łukasz Lew Sep 25 at 4:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.