1

I would like to know if lambda-calculus have been built using ZFC theory ? Or if it is not, on what kind of theory lambda-calculus is based on ?

toto
  • 165
  • Common sense :) – Wojowu Jun 13 '17 at 19:22
  • Do you means that lambda calculus only lays on itself and no other theory ? – toto Jun 13 '17 at 19:33
  • My previouis comment was just a (stupid) joke. The lambda calculus is usually considered without any foundations in mind, but it can be formalized over ZFC, or in fact many weaker systems, including Peano arithmetic. – Wojowu Jun 13 '17 at 19:34
  • Cool, but can you explain how ? – toto Jun 13 '17 at 19:37
  • Lambda calculus was devised shortly after combinator theory. They are techniques to formalize the concept of variable and function application. ZFC came long after and has nothing to do with either of them. Why would you presume that it has to be based on some other theory? – DanielV Jun 13 '17 at 20:40
  • Because i thought that every theory should be built on axioms according to the axiomatic method. So i though that there should be an underlying theory for lambda-calculus – toto Jun 13 '17 at 21:05
  • Being axiomatized is not the same as requiring an underlying metatheory. Lambda calculus can be axiomatized in the same way that first order logic can be, without appeal to an underlying set theory or what not. – Malice Vidrine Jun 13 '17 at 21:11
  • @MaliceVidrine : first order logic does need an underlying set theory, were it only to mention "set of variables" or "set of formulas" – Maxime Ramzi Jun 13 '17 at 21:21
  • 1
    NO; originally, $\lambda$ calculus was developed by Alonzo Church and others explicitly as an "alternative" system with respect to set theory (based on the primitive notion of membership). The fundamental notion of $\lambda$-calculus is the application of a function to an argument; a function is a primitive notion, not defined as a set but conceived as a rule. – Mauro ALLEGRANZA Jun 14 '17 at 14:33
  • 1
    @Max, Neither of those are really essential to be able to state the lexicon or syntax of a first order language, or to conduct or recognize a proof. That it's metamathematically convenient to do so is a different matter. – Malice Vidrine Jun 14 '17 at 15:30

0 Answers0