Introduction, Elimination Rules for — and D: A Study from Graded Context (Pattern Recognition and Machine Learning)


This paper is aimed to study the algebraic background of some proof theoretic rules in a set up where distinct levels of logic activity have been maintained carefully. In this regard, Introduction, Elimination rules for -i, and D have been considered as specific cases whose necessary and sufficient conditions from the perspective of graded consequence will reveal a new analysis.

Keywords: Graded consequence, Object level algebra, Meta level algebra, Introduction and Elimination rules, Proof theory.


Natural deduction system was introduced [5] to bring into notice the prototypes of human reasoning in the form of some rules of inference. Sentences (wffs) i.e. elements of F, the set of all wffs are object level entities; whereas, the notion of inference is a meta level concept. Rules of inference lie at meta meta level to talk about the interrelation between two or more than two inferences. This distinction between levels is generally missing in the existing approaches. Gentzen’s own interpretation totmp1411-1138_thumbIntroduction [5] is a clear evidence of mixing up meta level implication namely ‘provability’ with object level implication ‘follows’. Later on, when Sequent calculus was introduced [5], a sequent viz.,tmp1411-1139_thumb tmp1411-1140_thumbis assumed to represent the truth of the object level sentence

tmp1411-1141_thumbIn [7], it has been clearly mentioned that in LJ and LK (the sequent calculus presentations for Intuitionistic logic and Classical logic respectively) the presence of contraction left, weakening left, cut, &-left and &-right jointly claim the propositiontmp1411-1142_thumbif and only iftmp1411-1143_thumb

This indicates that usual practice in LJ and LK is to see meta level symbol ‘,’ and object level conjunction ‘&’ equivalently. Apart from LJ, LK, it has been a convenient practice in many other logical systems [6] also. In substructural logics [7] where some of the structural rules remain absent, the rules for & are modified in such a way that in absence of any one of the above mentioned structural rules tmp1411-1144_thumbif and only iftmp1411-1145_thumbremains unaltered. Thus in all these approaches a lack of clarity in distinction between levels of logic activity is envisaged.

Theory of graded consequence which was introduced by Chakraborty [1] in order to generalize two-valued notion of consequence relation in many-valued context, throws light on this issue. Suppose L is a set of truth values assigned  to the sentences of F endowed with some operators, say,tmp1411-1154_thumbin correspondence to each connectivetmp1411-1155_thumbof the object language. Now with respect totmp1411-1156_thumba set of fuzzy subsets any formula a gets a truth value in L. Thus tmp1411-1157_thumbdetermines the value of the meta-linguistic sentence ‘X semantically entails a’ or in symboltmp1411-1158_thumbIn two-valued context,tmp1411-1159_thumbi.e. ‘for all Tj, if tmp1411-1160_thumbthentmp1411-1161_thumbwhere eachtmp1411-1162_thumbis identified with the valuation under which all formulae of T get the value 1, involves a meta-level ‘if-then’ and quantifier ‘for all’. So, a complete lattice along with an implication ^m is needed for meta level algebra.

Now, let us consider the following form of Deduction Theorem (D-Introduction).


where X is a set of formulas andtmp1411-1173_thumbare single formulas. In algebraic term this can be restated as – ‘truth valuetmp1411-1174_thumbtruth valuetmp1411-1175_thumbOr more formally abbreviating ‘grade’ by ‘gr’ one can write –


So, to obtain Deduction Theorem (DT) as a rule of inference demands should be made to thetmp1411-1180_thumbin such a way that as a result (A) gets satisfied.

This clarifies that the algebras of different levels of logic give rise to different rules of inference. Having this as the main theme of the paper, in Section 2, the basic concept of the notion of graded consequence will be introduced and then as a specific case of study the necessary and sufficient conditions for graded Introduction, Elimination rules for D and — will be discussed. In Section 3 we will try to show that this study of proof theoretic results from the perspective of graded consequence gives a different analysis in comparison to the existing approaches.

In the Context of Graded Consequence

In graded context depending on a collection of fuzzy setstmp1411-1181_thumbover well-formed formulas the sentence ‘a is a consequence of X’ may get values other than the top (1) and least (0). That is, the notion of derivation of a formula from a set of formulae is in general a graded concept. Usually logics dealing with uncertainties do not feel the necessity to address many-valuedness in the concept of derivation. In this regard, an overlapping standpoint with ours can be found in [6] in the concept of degree of soundness of a rule. A graded consequence relation [3] is assumed to be a fuzzy relation satisfying the following conditions.


Given a context i.e a collectiontmp1411-1185_thumbof fuzzy subsets over formulae and a meta-level algebratmp1411-1186_thumb, consisting of operators for meta-level implication and conjunction, a sentence ‘a is a consequence of X’ gets a truth value, denoted bytmp1411-1189_thumbin L. In two-valued context, Shoesmith and Smiley [8], generalized the definition of semantic consequence with respect to a set oftmp1411-1190_thumb valuationstmp1411-1191_thumbAccording to this definitiontmp1411-1192_thumbbasically means’for all T in

tmp1411-1193_thumbif for alltmp1411-1194_thumbGeneralizing this idea in graded context the value oftmp1411-1195_thumbis calculated by thetmp1411-1196_thumb


In [2], it had been proved that given a contexttmp1411-1198_thumband a complete residuated latticetmp1411-1199_thumbfor meta level algebra,tmp1411-1200_thumbis a graded consequence relation. On the other hand, it also had been proved [2] that given any graded consequence relationtmp1411-1201_thumbthere existstmp1411-1202_thumba collection of fuzzy subsets over formulas, such that the fuzzy relation ‘tmp1411-1203_thumbcoincides withtmp1411-1204_thumbThese two results together constitutes the representation theorem. Now let us come to the context of graded rule DT i.e.tmp1411-1205_thumb


Theorem 1. A necessary and sufficient condition for gradedtmp1411-1207_thumb introduction rule)

For anytmp1411-1208_thumbdefined over a complete residuated lattice L, a necessary and sufficient condition fortmp1411-1209_thumbis that for anytmp1411-1210_thumb


Theorem 2. A necessary condition for graded MPtmp1411-1212_thumb

For anytmp1411-1213_thumbdefined over a complete residuated lattice L, the necessary condition for

Theorem 3. A sufficient condition for graded MP

tmp1411-1218_thumbdefined over a complete residuated lattice L, satisfy the conditions viz., tmp1411-1219_thumbfor anytmp1411-1220_thumb


From this study on the necessary and sufficient condition of the graded rule DT and MP we can see that an interrelation between the two levels of implication is needed for the viability of the rules. In two valued context (both classical and intuitionistic)tmp1411-1222_thumbare the same. Also fortmp1411-1223_thumb

tmp1411-1224_thumbholds. So, both DT and MP are valid in classical as well as intuitionistic cases. As a non-trivial example, let us consider [0, 1] endowed with Godel adjoint pair as the meta-level algebra for and Lukasiweciz implication for computingtmp1411-1225_thumbThen these structures for object and meta level satisfytmp1411-1226_thumb

tmp1411-1227_thumband hence DT holds in this case. On the other hand, with Godel algebra as meta structure and computingtmp1411-1228_thumbby Godel implication, one can find a model for graded rule MP.

Let us now consider the rule -Introduction viz., [a]

This presentation is due to Gentzen [5]. In a language where A, the falsum constant is not present the above form is equivalent to [a]


As in this present study we are considering sequents of the formtmp1411-1271_thumb, the

respective translation will betmp1411-1272_thumbfor alltmp1411-1273_thumb


Theorem 4. A necessary condition for graded —-Introduction

For anytmp1411-1277_thumb, defined over a complete residuated lattice L, the necessary condition

for intmp1411-1278_thumbis thattmp1411-1279_thumb

Theorem 5. A sufficient condition for graded —-Introduction

Lettmp1411-1280_thumb, defined over a complete residuated lattice L, satisfy the conditions viz.,

(i) there is an elementtmp1411-1281_thumbsuch thattmp1411-1282_thumbfor anytmp1411-1283_thumb

(ii) for anytmp1411-1284_thumbimpliestmp1411-1285_thumb Then intmp1411-1286_thumbholds.


—-Elimination presented in [5] is of the form


In graded context —-Elimination is generalized as – ‘There is sometmp1411-1299_thumbsuch that intmp1411-1300_thumbThe necessary and sufficient conditions for graded —-Elimination are as follows.

Theorem 6. A necessary condition for graded —-Elimination For any arbitrarily chosen complete residuated lattice L if graded —-Elimination holds for anytmp1411-1301_thumbthen for any non-zerotmp1411-1302_thumbthere exists some non-zero z in L such thattmp1411-1303_thumb

Theorem 7. A sufficient condition for graded —-Elimination

Lettmp1411-1309_thumbbe a complete residuated lattice determining a graded consequence relationtmp1411-1310_thumbbe the operator for object language negation — with the conditions – (i) there is sometmp1411-1311_thumb, such thattmp1411-1312_thumbfor any b in L andtmp1411-1313_thumbthen there existstmp1411-1314_thumbsuch thattmp1411-1315_thumb

Then graded —-Elimination holds.

In two-valued contexttmp1411-1316_thumbis always 0 and hence —-Elimination holds for k

= 1. Also, the conditions suffice to have —-Introduction are true in two-valued context and hence we get —-Introduction in two-valued case. To have a non-trivial example let us considertmp1411-1317_thumbwith Lukasiewicz adjoint pair at meta level algebra. — is defined bytmp1411-1318_thumbfor a =1 and 1 otherwise. Then for

c =1/2 one can verify the sufficient conditions for graded —-Introduction. The same structure also suffices to have graded —-Elimination; but in this case value of k will be 1. On the other hand, instead of the above definition of —o if we considertmp1411-1319_thumbthen the value of k will be 1/2.

3 An Analysis of Proof Theoretic Rules of Inference: Existing Approaches versus the Theory of Graded Consequence

In the introduction, it has already been discussed that the existing approaches of looking at the notion of inference are so designed that the distinction between object level and meta level connectives gets mingled up. DT statestmp1411-1320_thumb impliestmp1411-1321_thumbBut this turns out to betmp1411-1322_thumbimpliestmp1411-1323_thumb due to the equivalent treatment given to ‘,’ and ‘&’. On the other hand,tmp1411-1324_thumb [7] along with reflexivity and cut gives rise totmp1411-1325_thumbimpliestmp1411-1326_thumb

The algebraic counterpart oftmp1411-1327_thumbif and only iftmp1411-1328_thumbis given by

tmp1411-1329_thumbresiduation in object level operatorstmp1411-1330_thumbIn

this regard, the study of the background of DT from the perspective of graded consequence reveals a different analysis. In graded context, the summary of the semantic background of DT is – (i) the notion of consequencetmp1411-1331_thumbdepends on a meta-linguistic residuation pairtmp1411-1332_thumband (ii) the object leveltmp1411-1333_thumbcomputing


This seems more close to the understanding of the rule viz.,tmp1411-1335_thumb tmp1411-1363_thumb

as the rule asserts an object level implication viz.,tmp1411-1364_thumbprovidedtmp1411-1365_thumbis provable from a’.

In Section 2, we have discussed the necessary and sufficient condition for graded —-Introduction. The necessary condition for graded —-Introduction is tmp1411-1366_thumbOn the other hand, the sufficient condition demandstmp1411-1367_thumb tmp1411-1368_thumbfor sometmp1411-1369_thumbwhich in two-valued scenario will reduce totmp1411-1370_thumb

In algebraic termtmp1411-1378_thumb, the special case of —-Introduction can be translated as

tmp1411-1379_thumbwhere algebraic interpretation oftmp1411-1380_thumband the bold line between the upper and lower sequents are represented bytmp1411-1381_thumbrespectively.

Then algebraic translation oftmp1411-1382_thumbwould betmp1411-1383_thumbwould be

tmp1411-1384_thumb.This translation of —- Introduction becomes transparent due to the study of graded consequence.


Logic generally consists of three distinct levels viz, object, meta and meta-meta level. Each of these levels has a set of vocabulary which need not be the same. So, one can think of to have different algebraic structures for different levels of language, in general. Existing approaches have not paid much attention to this. As a result, the prevalent understanding for proof theoretic rules lacks a certain degree of clarity in maintaining the distinction of levels. In this paper we tried to provide an alternative analysis taking care of the distinction between levels. In this connection, exploring an alternative semantic background for classical and intuitionistic logic from the perspective of graded proof theoretic rules can be a new direction of study.

Next post:

Previous post: