> Are these two meanings of "undecidable" related

I can't claim to answer this, but you might like to look at A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory[0] which (amongst other interesting things) does discuss the proposition "ZFC is consistent", which is independent from ZFC, in terms of a Turing Machine which enumerates all possible proofs in ZFC and halts when it finds a contradiction (e.g. a proof of 0=1).

But I don't think there's a simple equivalence here, all the same.

The logician's undecidable is always relative to a set of axioms, whereas the question of whether a property of strings can be decided by some TM doesn't place any constraints on the TM, which is to say the deciding TM is not required to, nor prohibited from, implementing any particular axiom set.

(It's tempting to try and show "provable in ZFC" to be a (CS)undecidable property by having a TM enumerate ZFC proofs and halt on finding a proof or disproof of the input string, and imagine the TM running forever when given a statement of the Continuum Hypothesis. But the TM could proceed by other means - for example [1] shows a proof of CH's independence in a theorem prover, so that a TM incorporating this construction could indeed reject CH statements as unprovable in ZFC. Which is not to say "ZFC-provable" *isn't* (CS)undecidable, just that showing this isn't as simple as constructing a ZFC-proof-enumerator and giving it the CH as input.)

0: https://arxiv.org/abs/1605.04343

1: https://arxiv.org/abs/2102.02901