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?