2
$\begingroup$

In Chiswell and Hodges Mathematical Logic the authors define a sequent as such

"A sequent is an expression (Γ ⊢ ψ) (or Γ ⊢ ψ when there is no ambiguity) where ψ is a statement (the conclusion of the sequent) and Γ is a set of statements (the assumptions of the sequent) ...There is a proof whose conclusion is ψ and whose undischarged assumptions are all in the set Γ.".

They then go on to provide the axiom as follows:

Sequent Rule (Axiom Rule) If ψ ∈ Γ then the sequent (Γ ⊢ ψ) is correct.

Upon further reading about what exactly it means to be a sequent wikipedia I understand that for $\psi$ to be satisfied or "correct", every element of $\Gamma$ must be true as their all linked by AND conjunctions.

What confuses me is that suppose that there is an element in $\Gamma$ which is false then the whole antecedent is false according to the wikipedia definition by conjunction and then even though $\psi$ exists and is true in $\Gamma$ ultimately $\psi$ would be false. Could someone please explain to me and help clarify how the axiom and the definition can both be true. Thank you for all of your help.

$\endgroup$
2
$\begingroup$

The authors are introducing the basic elements of the proof system.

As you said, the definition of correct sequent $(\Gamma \vdash \psi)$ is :

There is a proof [according to the rules of the system to be specified] whose conclusion is $\psi$ and whose undischarged assumptions [premises] are all in the set $Γ$.

When the semantics of the language will be defined [see para 3.5] the authors will intorduce the concept of semantic sequent : $\Gamma \vDash \psi$, defined as :

for every $σ$-structure $A$, if $A$ is a model of $Γ$ then $A$ is a model of $ψ$.

The definition formalizes the informal concept of valid argument.

Then, they will prove the basic result [see page 87 : the Soundness Theorem of Natural Deduction for Propositional Logic] :

$\Gamma \vdash \psi \text { iff } \Gamma \vDash \psi$.


Having said that, the rules of the proof system are the "rules of the game" that allows us to derive conclusion from premises.

It is obvious that if $\psi \in \Gamma$, we can derive it from $\Gamma$ and this is formalized with the (Axiom Rule) above.

What if $\psi$ is false ? No problem: the move is "formally" correct but the argument is still valid because the case $\psi$ false does not contradict the definition of valid argument :

the conclusion must be true whenever all the premsies are true.

In geenral, the reasoning applies if some elements of $\Gamma$ is false; the (Axioom Rule) applies (because a premise can always be derived as conclusion) without contradiction.

$\endgroup$
  • $\begingroup$ Thank you for taking the time to respond and for your thorough answer. I suppose where my confusion lies is in the other elements of $\Gamma$ which are not $\psi$ if one of those elements were to be false wouldn’t that be enough to give us a result of false despite having $\psi$ in $\Gamma$. $\endgroup$ – user372382 Jan 10 at 8:40
  • $\begingroup$ Thank you for your revision, so in essence if I am understanding this correct if we have $\psi$ in $\Gamma$ we can ignore all other elements of $\Gamma$ despite them being true or false removing them from the conjunction and take only those elements in this case just $\psi$ which results in $\psi$ $\endgroup$ – user372382 Jan 10 at 8:44
  • $\begingroup$ @user372382 - as said, the rule is sound, i.e. derives true conclusion from true premises (i.e. we can "safely" use it in our formal arguments). What if we apply it to a set of premises that contains a false assumption ? This is not a problem of the rule; simply, the rule does not guarantee us that the conclusion will be true. $\endgroup$ – Mauro ALLEGRANZA Jan 10 at 8:45
  • $\begingroup$ If $\psi$ were true and were in the set of $\Gamma$ containing other elements which were false wouldn’t the conclusion $\psi$ be false contradicting our original assumption. $\endgroup$ – user372382 Jan 10 at 8:48
  • 1
    $\begingroup$ @user372382 - NO; if $\psi$ is true it is true "forever". The rule is applied "correctly", because $\psi$ was in the initial set of premises. Why this case does not contradict the def of valid argument ? Because the negation of the def is : there is a model where all premises are true and the conclusion is false, and thi is not your case. $\endgroup$ – Mauro ALLEGRANZA Jan 10 at 12:05

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.