I assume that’s the answer they’re looking for, yes. But this assumes the word “lie” means “to make a statement that is false according to the rules of first-order propositional logic,” but that is not specified in the problem and is definitely not the only or obvious choice of definition for that word.
If Pinocchio is the one choosing to lie, then his is the definition that counts, and he’s not a logician. If the lying is some sort of externally enforced compulsion, then the relevant definition is that of whatever entity or force compels him.
We have extensive philosophical and literary traditions exploring this kind of thing, from Gettier problems (would it be a lie to say you don’t know something, if you have a justified true belief that is only true for unknown reasons unrelated to your justification?) to the Aes Sedai in the Wheel of Time being known as prolific liars despite a magical oath to speak no word that is not true.
@Neil_Austin Vacuous truth in formal logic is much older than Godel and doesn’t help there, at all. It is a way to force all well-formed statements to fit into a model with only two possible truth values, though. I’m curious about this, though. I often see people argue that vacuously true statements should be regarded as false, and sometimes as neither, which I agree with in everyday life generally. But are there formal systems of logic that represent this without giving up all the results that come from use of vacuously true statements in math?