I am reading Chriswell & Hodges which says (p. 7)
A sequent is an expression
$(Γ \vdash ψ)$
where $ψ$ is a statement and $Γ$ is a set of statements. The sequent $(Γ \vdash ψ)$ means
(2.2) There is a proof whose conclusion is $ψ$ and whose undischarged assumptions are all in the set $Γ$.
When (2.2) is true, we say that the sequent is correct.
Why are the authors using 'true' and 'correct' instead of just 'true'? Is there some difference between the meaning of the two words?
On
I think the authors just want to make a difference between the theory of sequents and the meta level. The meta level here is talking about the theory of sequents.
I previously had a paragraph in this answer elaborating on possible differences in connotations, but I've come to the conclusion that I cannot separate those terms in a clear-cut fashion and thus deleted the paragraph.
'True' refers to the English statement (2.2), 'correct' refers to the sequent $\Gamma \vdash \Psi$. The authors aim to define when a sequent is correct in a technical sense, and they use the common sense of 'true' in natural language (the meta-level).
In other words, the meaning of the paragraph is that if the situation described by (2.2) holds (i.e. the statement $\Psi$ is provable from the undischarged assumptions $\Gamma$) then we say that the sequent $\Gamma \vdash \Psi$ is correct.
Note that it is not true that all sequents are correct: for instance, $X \vdash \lnot X$ is not correct (if your system is consistent) because there is no proof of $\lnot X$ from $X$.