I will try to clear up some confusion I see in the question and the OP's answer. Whenever I say "presentation", I mean a finite presentation (one with finitely many generators and finitely many relations), as infinite presentations do not come up.
Computational Decidability
First, every constant function is computable. So for a specific presentation $P$, we can prove that there is an algorithm that outputs whether it is trivial or not, using excluded middle:
- If $P$ presents the trivial group, the constant function that outputs "yes" computes the triviality of $P$ correctly.
- If $P$ presents a non-trivial group, the constant function that outputs "no" computes the triviality of $P$ correctly.
So we know there exists an algorithm, we just don't know which one it is. (To make a system of logic where this can't happen, a necessary, but not sufficient, criterion is to not allow the use of the principle of excluded middle. I will not comment on this further in the answer.) What people mean by "triviality is undecidable" is that the function from the set of presentations (encoded as natural numbers or finite strings from a finite alphabet) to $\{0,1\}$ that is $1$ on trivial groups and $0$ on non-trivial groups is not a computable function.
Logical Decidability
However, you also ask if there exists a presentation $P$ of a group such that there is no Turing machine that calculates the triviality of $P$ and provides a proof that it is correct. Suitably interpreted, the answer to this question is in fact yes, simply because there exists a presentation $P$ such that there exists no proof (in ZFC) that the group it presents is trivial or non-trivial, assuming ZFC is consistent.
This follows from a particular line of reasoning based on the Halting problem and Gödel's incompleteness theorem that I think I've seen on this site before, though I can't quite remember where (the closest I could find is this).
Firstly, the proof that triviality of a presentation is undecidable actually shows more. In fact, what is shown is that for each Turing machine $M$, there is a presentation $P_M$ that presents a trivial group iff $M$ halts when given an empty input, and the function $M \mapsto P_M$ is computable. For any theory $T$ where the set of axioms is recursively enumerable (e.g. Peano arithmetic, ZFC) there is a Turing machine $M_T$ that, given an empty input, searches through all formal proofs in that theory and halts if it reaches a contradiction (people have actually constructed such a thing -- see the references). If we apply the construction from the proof of the undecidability of the triviality problem, we get a presentation $P_{M_T}$ that presents a trivial group iff $M_T$ halts iff $\lnot\mathrm{Con}(T)$. So we just do this with $T = \mathrm{ZFC}$. Gödel's incompleteness theorem then gives us that ZFC cannot prove whether or not $P_{M_{\mathrm{ZFC}}}$ presents a trivial group.
In your answer, you say that since it is undecidable, $P_{M_{\mathrm{ZFC}}}$ "must be a non-trivial group". If ZFC is consistent, then, by Gödel, $\mathrm{ZFC} + \lnot \mathrm{Con}(\mathrm{ZFC})$ is consistent, and therefore has a model $X$. When $P_{M_{\mathrm{ZFC}}}$ is interpreted in $X$, it presents a trivial group. However, this is because the natural numbers of $X$ and the standard natural numbers do not agree (specifically, about whether $\mathrm{Con}(\mathrm{ZFC})$ is true).
References
The proof the undecidability of the triviality of group presentations is actually in two pieces - the first goes from the halting problem to the word problem for finitely-presented groups, and the second part from the word problem for finitely-presented groups to the triviality of finite presentations. A nice reference for the word problem is Rotman's An Introduction to the Theory of Groups, Chapter 12, which includes enough background on the semigroup version of it as well. For the second part, Rabin's original paper is perfectly good, and for the triviality problem you only need Theorem 1.2, not the more sophisticated Theorem 1.1 (that works for an arbitrary Markov property).
Here are some references for people actually going through and explicitly constructing Turing machines that have the needed property relative to ZFC. Adam Yedidia and Scott Aaronson explicitly constructed a Turing machine that halts iff $\lnot \mathrm{Con}(ZFC + SRP)$ (which implies Con(ZFC), SRP being the existence of a large cardinal with the stationary Ramsey property) using some of Harvey Friedman's work. Building on this, Stefan O'Rear explicitly constructed a Turing machine (with 5349 states) that halts iff $\lnot \mathrm{Con}(\mathrm{ZFC})$. Of course, it would be possible, given some programming effort, to produce a "compiler" from Turing machines to finitely-presented groups and thereby obtain $P_{M_{\mathrm{ZFC}}}$, but as far as I know nobody's done this yet.
