# What is the difference between 'true' and 'correct'?

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?

• In the book itself the word "true" is not written in italics and has been used several times earlier without an explicit definition (or something like that) and in an informal way. This in contrast with the word "correct" (which is written in italics). I think you must see it as a split up of sequents. There are sequents that are correct and also sequents that are not correct. In (2.2) you find the criterium for a sequent for being correct. – drhab Sep 29 '19 at 7:39
• @drhab What do you mean by a 'split up of sequents'? – Lachie Sep 29 '19 at 7:42
• That there are two sorts: sequents that are correct and sequents that are not correct. – drhab Sep 29 '19 at 7:43
• @MauroALLEGRANZA - In my opinion the question should be reopened because it is not a duplicate of that question. Of course, the two questions are related and inspired by the same textbook, but they are different. Here the OP is in trouble in understanding the difference between the meta-language (English sentences) and the object language (sequents) in a definition. There the question is more technical and about the validity of arguments. – Taroccoesbrocco Sep 29 '19 at 13:18
• It means simply that, "if it is true that there is a proof whose conclusion is ψ and whose undischarged assumptions are all in the set Γ" the sequent $(\Gamma \vdash \psi)$ is the formalization of a correct deductive inference (later called valid). – Mauro ALLEGRANZA Sep 29 '19 at 17:00

'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$$.