Correctness of the antecedent rule in sequent calculus

  • Thread starter Thread starter matts0
  • Start date Start date
  • Tags Tags
    Calculus
AI Thread Summary
The discussion centers on the correctness of the antecedent rule, or Weakening, in sequent calculus as described in H.-D. Ebbinghaus's "Mathematical Logic." The rule states that if a sequent with a set of formulas Γ is correct, then a sequent with a superset Γ' is also correct, provided every member of Γ is included in Γ'. A participant questions the validity of this when Γ' includes the negation of a formula Φ, suggesting there would be no interpretation that satisfies both Γ' and Φ simultaneously. Clarification is sought on how the rule holds in such cases, indicating a potential misunderstanding of the implications of the rule. The conversation highlights the complexity of interpreting the rule in specific scenarios.
matts0
Messages
11
Reaction score
0
Hi. I have a question on the correctness of the antecedent rule in sequent calculus when I read the book "mathematical logic" written by H.-D. Ebbinghaus etc.
The rule says:
\frac{\Gamma \phi}{\Gamma^' \phi} if every member of Γ is also a member of Γ' ( Γ⊂ Γ' ,where Γ and Γ' are formula sets and Φ is a formula)
and the correctness has been showed in the book (Γ'⊨Φ). So basically it means if the sequent in the numerator is correct, then we have sequent in the denominator being correct.

But since Γ'⊨Φ means that every interpretation which is a model of Γ' is also a model of Φ, what if we have Γ' = Γ ∪ ¬ Φ, then there shall be no interpertation that is a model of Γ' and Φ at the same time. Then how is it correct?
I think I have misunderstandings in some part, but I still don't know where it is.

Thanks in advance.
 
Last edited:
Physics news on Phys.org
If there is no model of Γ, ¬Φ, then trivially each model of Γ, ¬Φ is also a model of Φ.

Note that what you call "the antecedent rule" is normally called Weakening.
 
OK. Thanks a lot.
But it is still a little hard for me to understand that.
Is there any actual case for that?
 
I was reading documentation about the soundness and completeness of logic formal systems. Consider the following $$\vdash_S \phi$$ where ##S## is the proof-system making part the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the turnstile symbol ##\vdash_S##, as far as I can tell it actually represents the empty set. So what does it mean ? I guess it actually means ##\phi## is a theorem of the formal system, i.e. there is a...

Similar threads

Back
Top