Oscar Cunningham on Nostr: If a word problem is decidable, can we always prove it's decidable? Or could there be ...

If a word problem is decidable, can we always prove it's decidable? Or could there be a monoid where there's an algorithm which seems to work, but we can't prove that it works?