Caroll's paradox => Rice theorem? To me (but I might be wrong) Rice's theorem asserts that it's not possible to formalise the demonstration of a non-trivial property of a recursively enumerable language within the same given language. The modus ponens being the basis for demonstrating, Rice therefore says in substance that you will necessarily need a metalanguage to define it.

What I call Carroll's paradox is referred in Wikipedia under What the Tortoise Said to Achilles.

Wikipedia explains the following:


  The Wittgensteinian philosopher Peter Winch discussed the paradox in The Idea 
  of a Social Science and its Relation to Philosophy (1958), where he argued that the paradox showed that "the actual process of drawing an inference, which is after all at the heart of logic, is something which cannot be represented as a logical formula ... Learning to infer is not just a matter of being taught about explicit logical relations between propositions; it is learning to do something" (p. 57). Winch goes on to suggest that the moral of the dialogue is a particular case of a general lesson, to the effect that the proper application of rules governing a form of human activity cannot itself be summed up with a set of further rules, and so that "a form of human activity can never be summed up in a set of explicit precepts" (p. 53).


In other words, Carroll's paradox shows that it's not formally possible to prove a property of a language purely with propositions of this language. You will need to admit a rule (or a principle) that "the modus ponens means X" with X using everyday words. I.e. you will need a meta language.

I will concede that it is a philosophical way to ask the question. But Carroll's paradox can be described in a formal (mathematical) way (done here).

Hence am I mistaken in principle to say that Caroll's paradox implies Rice's theorem?
Well, any true statement implies every other true statement, so in that vacuous sense, I suppose one implies the other.

But no, I wouldn't say that Carroll's paradox implies Rice's theorem in any interesting or meaningful way.  Carroll's Paradox is an explanation of why we need modus ponens as an inference rule in propositional logic and can't replace it with a finite list of axioms.  It's nothing fancier than that.  As such, it refers to what is true in a logical theory.  It refers to what inference rules or axioms we need.

Rice's theorem is different.  It talks about what is decidable, not what is true.   It talks about what can be computed on a Turing machine, not about the inference rules or axioms we need.

Rice's theorem doesn't say "it's not possible to formalise the demonstration of a non-trivial property of a recursively enumerable language within the same given language".  It has nothing to do with "within the same given language" (it's not even clear what that would mean; a language is a subset of $\{0,1\}^*$ and doesn't demonstrate anything), but rather with that can be computed with a Turing machine.  Rice's theorem talks about what a Turing machine can decide.

Rice's theorem doesn't say "you will necessarily need a metalanguage to define modus ponens".  (I don't even know what a metalanguage would mean in this context.)  It has nothing to do with what you can define.  Rather, it has to do with what a Turing machine can decide.

In general, I warn you against trying to reason about mathematical statements using English language and analogies.  That is notoriously error-prone.  Rice's theorem is a mathematical statement with a precise mathematical meaning.  At a suitable level of imprecision and vagueness, I suspect everything can seem similar and connected -- but when you look at the specifics, the situation often becomes richer and more interesting than that.