The work of Church, Turing and Godel (and others, like Post etc.) suggests they share the same content (or subject matter), so it seems to me they are two ways of specifying the same thing. Is there a way to convert one to the other and vice-versa. How do the relations, functions, arity, of logic correspond to the start symbol, non-terminals, terminal symbols, logical axioms, non-logical axioms and production rules, etc. of a formal language (or formal system?) Automata and Turing machines also refer to the same content. Can one convert from one of these to another of these?

  • $\begingroup$ This might interest you en.wikipedia.org/wiki/Categorical_logic $\endgroup$ – user20672 2 days ago
  • $\begingroup$ The fact that proofs in every formal system can be verified using software written in just about any general-purpose programming language (e.g. C++, Basic) suggests to me that there may be something universal about classical bivalent logic which the basis for such programming languages. I would think that proofs in one formal system should be convertible to any other system using those same programming languages. $\endgroup$ – Dan Christensen 2 days ago
  • $\begingroup$ I remembered something I think is relevant: the Curry-Howard-Lambek correspondence, which, according to Wikipedia, implies either that programs are proofs, or that proofs are programs (or both?) it seems Lambek extended the correspondence (it is also called an isomorphism) to Category theory. It seems to have something to do with types, or type theory, or something like that. Sorry to be so vague, but I hope my questions and the items I referred to stimulate some thought. Civil responses to my posts are appreciated. (I get the feeling that responses to my other posts tried to shut me up.) $\endgroup$ – Joe Cash yesterday

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.