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?
 

Thread 'Value of intuitionistic logic'

I'm taking a look at intuitionistic propositional logic (IPL). Basically it exclude Double Negation Elimination (DNE) from the set of axiom schemas replacing it with Ex falso quodlibet: ⊥ → p for any proposition p (including both atomic and composite propositions). In IPL, for instance, the Law of Excluded Middle (LEM) p ∨ ¬p is no longer a theorem. My question: aside from the logic formal perspective, is IPL supposed to model/address some specific "kind of world" ? Thanks.
View full post »

Thread 'Formal derivation of statement from Peano Arithmetic system'

I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema): $$\begin{align} & (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\ & (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\ & (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\ & (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\ & (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\ & (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber...
View full post »

Similar threads

Basic Mathematical Logic - Understanding Sequents
Replies
5
Views
2K
A Perihelion Precession in GR with Robertson Expansion
Replies
4
Views
2K
Equation of motion for oscillations about a stable orbit
Replies
2
Views
4K
Wave Confluence: Ship & Radiotowers (Check Needed)
Replies
6
Views
1K
What Is Conformal Mapping in Complex Analysis?
Replies
6
Views
3K
Generalized velocity addition and aberration formulas
Replies
4
Views
2K
Carnot Engine cycle on PV Diagram
Replies
5
Views
2K
Trying to understand ω-inconsistency
Replies
2
Views
2K
A Oscillator Model with Eigenfunctions
Replies
2
Views
2K
I Solving Mass-Speed Relation Proof Challenges
Replies
5
Views
1K

Hot Threads

Recent Insights

Back
Top