Correctness of the antecedent rule in sequent calculus

  • Context: Graduate 
  • Thread starter Thread starter matts0
  • Start date Start date
  • Tags Tags
    Calculus
Click For Summary
SUMMARY

The discussion centers on the correctness of the antecedent rule, also known as Weakening, in sequent calculus as presented in "Mathematical Logic" by H.-D. Ebbinghaus. The rule states that if every member of a set of formulas Γ is included in another set Γ', then the sequent Γ ⊨ Φ implies Γ' ⊨ Φ. A participant questions the validity of this rule when considering the case where Γ' is defined as Γ ∪ ¬Φ, arguing that no interpretation can satisfy both Γ' and Φ simultaneously. The conversation highlights a common misunderstanding regarding the implications of the rule and seeks clarification on its practical applications.

PREREQUISITES
  • Understanding of sequent calculus and its rules
  • Familiarity with logical formulas and interpretations
  • Knowledge of the concepts of models in mathematical logic
  • Basic grasp of the terminology used in "Mathematical Logic" by H.-D. Ebbinghaus
NEXT STEPS
  • Study the implications of the Weakening rule in sequent calculus
  • Explore examples of sequent calculus to see practical applications
  • Investigate the relationship between models and interpretations in logic
  • Read further on the concept of entailment in mathematical logic
USEFUL FOR

Students of mathematical logic, logicians, and anyone interested in the foundations of sequent calculus and its rules will benefit from this discussion.

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?
 

Similar threads

Graduate Basic Mathematical Logic - Understanding Sequents
  • · Replies 5 ·
Replies
5
Views
2K
Graduate Perihelion Precession in GR with Robertson Expansion
  • · Replies 4 ·
Replies
4
Views
2K
Equation of motion for oscillations about a stable orbit
  • · Replies 2 ·
Replies
2
Views
5K
Wave Confluence: Ship & Radiotowers (Check Needed)
  • · Replies 6 ·
Replies
6
Views
2K
Graduate What Is Conformal Mapping in Complex Analysis?
  • · Replies 6 ·
Replies
6
Views
3K
Graduate Generalized velocity addition and aberration formulas
  • · Replies 4 ·
Replies
4
Views
2K
Carnot Engine cycle on PV Diagram
  • · Replies 5 ·
Replies
5
Views
2K
Graduate Trying to understand ω-inconsistency
  • · Replies 2 ·
Replies
2
Views
3K
Graduate Issue in the electron’s infinite self-energy
  • · Replies 3 ·
Replies
3
Views
2K
Graduate Oscillator Model with Eigenfunctions
  • · Replies 2 ·
Replies
2
Views
2K