Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Correctness of the antecedent rule in sequent calculus

  1. Oct 24, 2012 #1
    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:
    [itex]\frac{\Gamma \phi}{\Gamma^' \phi}[/itex] 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: Oct 24, 2012
  2. jcsd
  3. Oct 24, 2012 #2
    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.
  4. Oct 24, 2012 #3
    OK. Thanks a lot.
    But it is still a little hard for me to understand that.
    Is there any actual case for that?
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook