A sequent is an expression , where  and  are (possibly empty) sequences of formulas. Here,  is called the antecedent and  is called the consequent. The informal understanding of sequents is that the sequent  corresponds to . The initial sequent of all derivations is

(1)

The rules of inference for sequent calculus are divided in two categories: structural and logical. There are at least two logical rules for every propositional connective and every quantifier; one of them applies to the antecedent, whereas the other applies to the consequent. The structural rules are thinning,

(2)

contraction,

(3)

exchange,

(4)

and cut,

(5)

The logical rules are given by conjunction,

(6)

disjunction,

(7)

negation,

(8)

implication,

(9)

universal quantifier,

(10)

and existential quantifier

(11)

Here, the variable  is free in  and  is obtained from  by replacing all free occurrences of  by . The variable  occurring in the -succedent rule and the -antecedent rule is called the eigenvariable. It may not occur in the lower sequents of the respective rules.

Sequent calculus specifies classical first-order logic, and the same framework can also be used to specify intuitionistic logic. In order to limit derivations to intuitionistic ones, the additional constraint that every succedent may have not more one formula is added. The classical (multi-succedent) variant due to Gentzen is called LK, and the intuitionistic (single-succedent) variant is called LJ. LK can alternatively be defined as single-succedent calculus augmented with the law of excluded middle as yet another basic sequent. Proof theories based on sequent rules of inference are also called Gentzen-type. Many other logic formulations based on sequents have been introduced subsequently.

A sample derivation is provided by double negation, which is valid in the classical variant of the sequent calculus but not in the intuitionistic one.

A second derivation (which is a valid intuitionistic derivation) is shown above.

Sequent calculus is a very useful tool for proof theory, primarily because of the admissibility of the cut rule, which can be eliminated from derivations without affecting the set of derivable formulas.

REFERENCES

Gentzen, G. The Collected Papers of Gerhard Gentzen (Ed. M. E. Szabo). Amsterdam, Netherlands: North-Holland, 1969.

Kleene, S. C. Introduction to Metamathematics. Princeton, NJ: Van Nostrand, 1964.

اخر الاخبار

اخبار العتبة العباسية المقدسة

وفد العتبة العباسية المقدسة يهنئ الأمين العام للعتبة الكاظمية المقدسة بمناسبة تعيينه

العتبة العباسية المقدسة تنظم دورة في الإسعافات الأولية لعدد من ملاكاتها

في مستشفى الكفيل.. فريق طبي ينجح بمعالجة مسن يعاني من انسداد القناة الصفراوية

المجمع العلمي يقيم جلسةً قرآنية لتعليم أحكام التلاوة في النجف الأشرف

المزيد

الآخبار الصحية

الأطعمة الحارة.. "سر صغير" يغير صحة قلبك وعقلك

وباء صامت.. الملايين حول العالم مصابون بالسكري دون أن يعلموا !

لماذا ينصح بتناول تفاحة يوميا؟

8 فواكه طبيعية تمنحك نوما هنيئا.. وتخلصك من الأرق

المزيد

الآخبار التكنلوجية

ثلاث علامات على وجود مشاكل خطيرة في محرك السيارة ؟

ماذا نعرف عن اللقاح الروسي ضد السرطان؟

مركبة فضاء تعثر على دليل عن وجود حياة قديمة على المريخ

لتدريب الذكاء الاصطناعي.. الصين تخطط لإنشاء شبكة حوسبة موحدة

المزيد