Correctness of the antecedent rule in sequent calculus

  • Thread starter matts0
  • Start date
  • Tags
    Calculus
In summary, the correctness of the antecedent rule in sequent calculus is demonstrated in the book "mathematical logic" by H.-D. Ebbinghaus etc. The rule states that if every formula in the set Γ is also in the set Γ', then Γ⊂Γ' and Φ is a formula, we can infer that the sequent in the denominator is also correct. However, there may be cases where Γ' = Γ ∪ ¬Φ, in which there is no interpretation that is a model of both Γ' and Φ. This may cause confusion, but it is important to note that this rule is also known as Weakening. There may be actual cases where this rule is applicable
  • #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.
 
Last edited:
Physics news on Phys.org
  • #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.
 
  • #3
OK. Thanks a lot.
But it is still a little hard for me to understand that.
Is there any actual case for that?
 

1. What is the antecedent rule in sequent calculus?

The antecedent rule in sequent calculus is a rule that allows for the introduction of a new formula in the antecedent of a sequent, as long as it does not already appear in the antecedent or succedent of the sequent.

2. How does the antecedent rule ensure correctness?

The antecedent rule ensures correctness by maintaining the logical validity of sequents. It ensures that any new formula introduced in the antecedent does not break the logical validity of the sequent, and that all rules used in the proof are sound and consistent.

3. What happens if the antecedent rule is not followed?

If the antecedent rule is not followed, it can lead to an incorrect proof or a proof that is not logically valid. This can happen if a new formula is introduced in the antecedent that already appears in the antecedent or succedent, or if the rule used to introduce the new formula is not sound or consistent.

4. Are there any exceptions to the antecedent rule?

Yes, there are some exceptions to the antecedent rule, such as the cut rule and the contraction rule. These rules allow for the introduction of a new formula in the antecedent even if it already appears in the antecedent or succedent, but they have specific restrictions and conditions that must be met.

5. How does the antecedent rule relate to other rules in sequent calculus?

The antecedent rule is a fundamental rule in sequent calculus and is closely related to other rules, such as the succedent rule and the structural rules. Together, these rules form the basis of sequent calculus and ensure the logical validity of proofs by providing a systematic and consistent method for manipulating formulas in sequents.

Similar threads

  • Set Theory, Logic, Probability, Statistics
Replies
5
Views
2K
  • Special and General Relativity
Replies
4
Views
1K
  • Advanced Physics Homework Help
Replies
2
Views
3K
  • Introductory Physics Homework Help
Replies
6
Views
1K
  • Topology and Analysis
Replies
6
Views
2K
  • Introductory Physics Homework Help
Replies
5
Views
1K
  • Special and General Relativity
Replies
4
Views
2K
  • Engineering and Comp Sci Homework Help
Replies
1
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
2
Views
2K
  • Quantum Physics
Replies
2
Views
1K
Back
Top