2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – drhab Sep 29 '19 at 7:39
  • $\begingroup$ @drhab What do you mean by a 'split up of sequents'? $\endgroup$ – Lachie Sep 29 '19 at 7:42
  • $\begingroup$ That there are two sorts: sequents that are correct and sequents that are not correct. $\endgroup$ – drhab Sep 29 '19 at 7:43
  • $\begingroup$ @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. $\endgroup$ – Taroccoesbrocco Sep 29 '19 at 13:18
  • $\begingroup$ 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). $\endgroup$ – Mauro ALLEGRANZA Sep 29 '19 at 17:00
6
$\begingroup$

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

$\endgroup$
  • $\begingroup$ So are they only using the word 'correct' as an abbreviation for saying '(2.2) is true'? $\endgroup$ – Lachie Sep 29 '19 at 7:54
  • 1
    $\begingroup$ @Lachie - Roughly speaking, yes. But remember that only sequents can be 'correct'. A sequent is not true (unless the authors define a technical notion of truth for sequents). Here 'true' is used in the common (non-technical) sense of natural language and refers to English sentences. $\endgroup$ – Taroccoesbrocco Sep 29 '19 at 7:59
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.