Definition: A sequent is an expression (A ⊢ C) where C is a statement called the conclusion of the sequent and A is a set of statements called the assumptions of the sequent. (A ⊢ C) is read 'A entals C' and means that there is a proof whose conclusion is C and whose undischarged assumptions are all in the set A. (⊢ C) means there is a proof of C relying on no undischarged assumptions.
Sequent Rule (∧I): If (A ⊢ C) and (B ⊢ D), then [(A ⋃ B) ⊢ (C ∧ D)].
Sequent Rule (∧E): If [A ⊢ (B ∧ C)], then (A ⊢ B) and (A ⊢ C).
Sequent Rule (⇒I): If [A ⋃ {b} ⊢ C], then [A ⊢ (b ⇒ C)].
Sequent Rule (⇒E): If (A ⊢ C) and [B ⊢ (C ⇒ D)], then [(A ⋃ B) ⊢ D]
No comments:
Post a Comment