- #1
matts0
- 11
- 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:
[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.
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: