1603:
13373:
120:), and then the quantifiers are reintroduced. This very much parallels the way in which mathematical proofs are carried out in practice by mathematicians. Predicate calculus proofs are generally much easier to discover with this approach, and are often shorter. Natural deduction systems are more suited to practical theorem-proving. Sequent calculus systems are more suited to theoretical analysis.
11154:
8616:
10108:
12838:, p. 336, wrote in 1967 that "it was a major logical discovery by Gentzen 1934â5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."
10985:
3247:): Every formula that can be proven in these has a reduction tree. This can be shown as follows: Every proof in propositional calculus uses only axioms and the inference rules. Each use of an axiom scheme yields a true logical formula, and can thus be proven in sequent calculus; examples for these are
11172:
These derivations also emphasize the strictly formal structure of the sequent calculus. For example, the logical rules as defined above always act on a formula immediately adjacent to the turnstile, such that the permutation rules are necessary. Note, however, that this is in part an artifact of the
3222:
It is easy to see that the steps in the tree preserve the semantic truth value of the formulas implied by them, with conjunction understood between the tree's different branches whenever there is a split. It is also obvious that an axiom is provable if and only if it is true for every assignment of
11201:
Weakening (W) allows the addition of arbitrary elements to a sequence. Intuitively, this is allowed in the antecedent because we can always restrict the scope of our proof (if all cars have wheels, then it's safe to say that all black cars have wheels); and in the succedent because we can always
3211:
Starting with any formula in propositional logic, by a series of steps, the right side of the turnstile can be processed until it includes only atomic symbols. Then, the same is done for the left side. Since every logical operator appears in one of the rules above, and is removed by the rule, the
103:
In other words, natural deduction and sequent calculus systems are particular distinct kinds of
Gentzen-style systems. Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms. Gentzen-style systems typically have very few axioms, if any, relying
1580:
in the classical natural deduction system NK is removed in the classical sequent calculus system LK. He said that the sequent calculus LJ gave more symmetry than natural deduction NJ in the case of intuitionistic logic, as also in the case of classical logic (LK versus NK). Then he said that in
3981:
Note that, contrary to the rules for proceeding along the reduction tree presented above, the following rules are for moving in the opposite directions, from axioms to theorems. Thus they are exact mirror-images of the rules above, except that here symmetry is not implicitly assumed, and rules
2373:
The items to the left of the turnstile are understood to be connected by conjunction, and those to the right by disjunction. Therefore, when both consist only of atomic symbols, the sequent is accepted axiomatically (and always true) if and only if at least one of the symbols on the right also
4913:
1288:
At first sight, this extension of the judgment form may appear to be a strange complicationâit is not motivated by an obvious shortcoming of natural deduction, and it is initially confusing that the comma seems to mean entirely different things on the two sides of the turnstile. However, in a
2377:
Following are the rules by which one proceeds along the tree. Whenever one sequent is split into two, the tree vertex has two child vertices, and the tree is branched. Additionally, one may freely change the order of the arguments in each side; Γ and Δ stand for possible additional
2896:
10537:
12709:, p. 191. "Hiermit haben wir einige Gesichtspunkte zur BegrĂŒndung der Aufstellung der folgenden KalkĂŒle angegeben. Im wesentlichen ist ihre Form jedoch durch die RĂŒcksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorlĂ€ufig nicht nĂ€her begrĂŒndet werden."
1101:
will also be true. Thus the empty sequent, having both cedents empty, is false. One way to express this is that a comma to the left of the turnstile should be thought of as an "and", and a comma to the right of the turnstile should be thought of as an (inclusive) "or". The sequents
1575:
Gentzen asserted a sharp distinction between his single-output natural deduction systems (NK and NJ) and his multiple-output sequent calculus systems (LK and LJ). He wrote that the intuitionistic natural deduction system NJ was somewhat ugly. He said that the special role of the
11177:
of formulas in the interpretation of the sequent, rather than sequences, eliminating the need for an explicit permutation rule. This corresponds to shifting commutativity of assumptions and derivations outside the sequent calculus, whereas LK embeds it within the system itself.
10829:
10683:
4168:
2592:
6268:
6129:
2697:
1548:
4792:
4685:
1563:, which manifests itself as logical negation on the semantic level, translates directly into a leftâright symmetry of sequentsâand indeed, the inference rules in sequent calculus for dealing with conjunction (â§) are mirror images of those dealing with disjunction (âš).
2990:
8473:
11560:
9927:
9788:
1412:
5010:
1558:
In these formulations, the only difference between formulae on either side of the turnstile is that one side is negated. Thus, swapping left for right in a sequent corresponds to negating all of the constituent formulae. This means that a symmetry such as
11031:
2489:
10368:
10238:
2791:
11966:
3162:
3077:
8494:
107:
Gentzen-style systems have significant practical and theoretical advantages compared to
Hilbert-style systems. For example, both natural deduction and sequent calculus systems facilitate the elimination and introduction of universal and existential
5624:
5516:
5406:
5298:
4478:
4280:
8312:
6840:
Instead of viewing the rules as descriptions for legal derivations in predicate logic, one may also consider them as instructions for the construction of a proof for a given statement. In this case the rules can be read bottom-up; for example,
4576:
4378:
5988:
5895:
1831:
5188:
5100:
9980:
7772:
Next is the proof of a simple fact involving quantifiers. Note that the converse is not true, and its falsity can be seen when attempting to derive it bottom-up, because an existing free variable cannot be used in substitution in the rules
7058:. However, there are only finitely many possibilities to be checked since the antecedent by assumption is finite. This also illustrates how proof theory can be viewed as operating on proofs in a combinatorial fashion: given proofs for both
5800:
5719:
1280:
3267:(standing for Logistische KalkĂŒl) as introduced by Gentzen in 1934. A (formal) proof in this calculus is a sequence of sequents, where each of the sequents is derivable from sequents appearing earlier in the sequence by using one of the
9642:
1713:
286:). The theorems are those formulae that appear as the concluding judgment in a valid proof. A Hilbert-style system needs no distinction between formulae and judgments; we make one here solely for comparison with the cases that follow.
12680:
nahm der Satz vom ausgeschlossenen
Dritten eine Sonderstellung unter den SchluĂweisen ein , indem er sich der EinfĂŒhrungs- und Beseitigungssystematik nicht einfĂŒgte. Bei dem im folgenden anzugebenden logistischen klassichen KalkĂŒl
10875:
12371:
1915:
12244:
8167:
4800:
1593:
makes the following comment on the translation into
English: "Gentzen says 'Sequenz', which we translate as 'sequent', because we have already used 'sequence' for any succession of objects, where the German is 'Folge'."
2799:
1566:
Many logicians feel that this symmetric presentation offers a deeper insight in the structure of the logic than other styles of proof system, where the classical duality of negation is not as apparent in the rules.
6398:. In contrast, the structural rules operate on the structure of the sequents, ignoring the exact shape of the formulae. The two exceptions to this general scheme are the axiom of identity (I) and the rule of (Cut).
1995:
10428:
7202:
The second rule that is somewhat special is the axiom of identity (I). The intuitive reading of this is obvious: every formula proves itself. Like the cut rule, the axiom of identity is somewhat redundant: the
777:
2073:
10729:
10583:
4062:
11808:, they have fewer theorems), and thus not complete with respect to the standard semantics of first-order logic. However, they have other interesting properties that have led to applications in theoretical
872:
2495:
1181:
6135:
5996:
2600:
3219:
Thus, the sequents in the leaves of the trees include only atomic symbols, which are either provable by the axiom or not, according to whether one of the symbols on the right also appears on the left.
1428:
8038:
7214:
Observe that all rules have mirror companions, except the ones for implication. This reflects the fact that the usual language of first-order logic does not include the "is not implied by" connective
11712:
4691:
289:
The price paid for the simple syntax of a
Hilbert-style system is that complete formal proofs tend to get extremely long. Concrete arguments about proofs in such a system almost always appeal to the
12874:. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, wĂ€hrend er hier durch die Sukzedensbedingung ausgedrĂŒckt wird." English translation: "The difference between
4584:
4056:
6800:
is true is not in general possible. If, however, the variable y is not mentioned elsewhere (i.e. it can still be chosen freely, without influencing the other formulae), then one may assume, that
2902:
8358:
7681:
11459:
377:
11652:
47:) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of
9834:
9695:
1301:
710:
11149:{\displaystyle \vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}
2172:
2127:
11784:
11417:
3204:
12483:, pp. 440â516. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.
4919:
12898:. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."
9418:
3388:
2401:
13292:
7586:
7507:
10284:
10154:
9508:
8611:{\displaystyle {\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}}
2703:
11865:
7754:
7272:
3083:
2998:
7925:
2274:
11309:
9336:
9257:
11205:
Contraction (C) and
Permutation (P) assure that neither the order (P) nor the multiplicity of occurrences (C) of elements of the sequences matters. Thus, one could instead of
8836:
8763:
7421:
7232:
11338:
11023:
10867:
10420:
9560:
6437:
5522:
5414:
5304:
5196:
4386:
4188:
2201:
12154:
12092:
9972:
9687:
6733:
6336:
6305:
2357:
2313:
2230:
8213:
7631:
7466:
6761:
4484:
4286:
10103:{\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}
9164:
9008:
8350:
8205:
8076:
7963:
7829:
7800:
6870:
11971:
The resulting system is called LJ. It is sound and complete with respect to intuitionistic logic and admits a similar cut-elimination proof. This can be used in proving
11857:
11451:
6554:
5901:
5808:
1747:
12123:
12007:
9374:
9091:
8935:
8728:
8690:
7386:
7348:
5106:
5018:
12036:
11367:
There is some freedom of choice regarding the technical details of how sequents and structural rules are formalized without changing what sequents the system derives.
9216:
7122:
6896:
6699:
6523:
3587:
3567:
1036:
551:
12061:
11278:
7056:
7036:
7016:
6976:
6936:
6916:
6654:
6634:
6614:
6574:
6497:
6457:
6396:
3963:
3470:
3439:
3300:
1739:
481:
453:
5725:
5644:
1192:
12495:, pp. 283â312, 331â361, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.
11735:
11595:
1099:
1069:
953:
926:
635:
608:
578:
508:
407:
10721:
10575:
10276:
10146:
9826:
9295:
9129:
8973:
8801:
7719:
7545:
3408:
1623:. It gives a series of steps that allows one to reduce the problem of proving a logical formula to simpler and simpler formulas until one arrives at trivial ones.
11422:
One may also change whether rules with more than one premise share the same context for each of those premises or split their contexts between them: For example,
11419:. Any weakening that appears in a derivation can then be moved to the beginning of the proof. This may be a convenient change when constructing proofs bottom-up.
9568:
9473:
9062:
8906:
8661:
7866:
7319:
1632:
7127:
When looking for some proof, most of the rules offer more or less direct recipes of how to do this. The rule of cut is different: it states that, when a formula
3943:
3920:
3897:
3874:
3851:
3828:
12267:
11254:
10980:{\displaystyle \left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)}
7185:
7165:
7145:
7096:
7076:
6996:
6956:
6835:
6798:
6674:
6594:
6477:
6356:
3803:
3766:
3746:
3726:
3706:
3686:
3666:
3646:
3626:
3540:
3520:
3498:
3354:
3334:
1013:
993:
973:
655:
528:
427:
268:
245:
11828:. To this end, one has to restrict to sequents with at most one formula on the right-hand side, and modify the rules to maintain this invariant. For example,
995:
are nonnegative integers, that is, the left-hand-side or the right-hand-side (or neither or both) may be empty. As in natural deduction, theorems are those
180:. Gentzen further demonstrated the power and flexibility of this technique a few years later, applying a cut-elimination argument to give a (transfinite)
59:, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical
7234:
that would be the De Morgan dual of implication. Adding such a connective with its natural rules would make the calculus completely leftâright symmetric.
12519:, pp. 184â244, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.
12275:
11216:
The extra effort of using sequences, however, is justified since part or all of the structural rules may be omitted. Doing so, one obtains the so-called
1846:
4908:{\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)}
12162:
8084:
2366:, as depicted on the right. The root of the tree is the formula we wish to prove; the leaves consist of atomic formulas only. The tree is known as a
1581:
addition to these reasons, the sequent calculus with multiple succedent formulas is intended particularly for his principal theorem ("Hauptsatz").
2891:{\displaystyle L\rightarrow {\text{rule: }}{\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}}
6401:
Although stated in a formal way, the above rules allow for a very intuitive reading in terms of classical logic. Consider, for example, the rule
116:. In a typical argument, quantifiers are eliminated, then propositional calculus is applied to unquantified expressions (which typically contain
10532:{\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A}
12094:. When multi-formula consequents are interpreted as disjunctions, all of the other inference rules of LK are derivable in LJ, while the rules
1926:
13299:
721:
10824:{\displaystyle \left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}
10678:{\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A}
4163:{\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})}
1920:
Again the right hand side includes an implication, whose premise can further be assumed so that only its conclusion needs to be proven:
12764:
2362:
This process can always be continued until there are only atomic formulas in each side. The process can be graphically described by a
2010:
7167:
can be "cut out" and the respective derivations are joined. When constructing a proof bottom-up, this creates the problem of guessing
2587:{\displaystyle R\land {\text{rule: }}{\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}}
11186:
For certain formulations (i.e. variants) of the sequent calculus, a proof in such a calculus is isomorphic to an upside-down, closed
6263:{\displaystyle {\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})}
6124:{\displaystyle {\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})}
3239:
Sequent calculus is related to other axiomatizations of classical propositional calculus, such as Frege's propositional calculus or
2692:{\displaystyle L\lor {\text{rule: }}{\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}}
796:
1543:{\displaystyle \vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})}
1108:
580:
s and the turnstile are not written down explicitly; instead a two-dimensional notation from which they can be inferred is used.)
7204:
4787:{\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma \vdash B,\Delta }{\Gamma \vdash A\land B,\Delta }}\quad ({\land }R)}
11565:
Contraction and weakening make this version of the rule interderivable with the version above, although in their absence, as in
7971:
4680:{\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}\quad ({\lor }L)}
11663:
11202:
allow for alternative conclusions (if all cars have wheels, then it's safe to say that all cars have either wheels or wings).
13224:
13202:
13180:
13131:
13109:
13087:
12961:
192:, and the general concepts relating to them, have been widely applied in the fields of proof theory, mathematical logic, and
7195:: it states that all uses of the cut rule can be eliminated from a proof, implying that any provable sequent can be given a
4002:
2985:{\displaystyle R\rightarrow {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}}
185:
13342:
12564:
Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"
11972:
8468:{\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)}
11555:{\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.}
12531:, pp. 25â150, is an introductory presentation of practical natural deduction of this kind. This became the basis of
12471:, pp. 189â244, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.
7639:
13402:
3546:
317:
12507:, pp. 101â127, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.
9922:{\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A}
9783:{\displaystyle \left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}
13153:
13061:
12939:
11611:
2082:
on the first argument on the left. Thus we may split the sequent to two, where we now have to prove each separately:
1407:{\displaystyle \vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}}
12547:
is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style
3240:
553:(with an empty left-hand side) is the conclusion of a valid proof. (In some presentations of natural deduction, the
1285:
are equivalent in the strong sense that a proof of either sequent may be extended to a proof of the other sequent.
5005:{\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)}
663:
7147:
can be concluded and this formula may also serve as a premise for concluding other statements, then the formula
2484:{\displaystyle L\land {\text{rule: }}\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}}
2133:
2088:
11740:
11384:
3171:
181:
13267:
10363:{\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A}
10233:{\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}
2786:{\displaystyle R\lor {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}}
13260:
11961:{\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,A\lor B\vdash C}}\quad ({\lor }L)}
9382:
8618:. It is straightforward to find the derivation, which exemplifies the usefulness of LK in automated proving.
3945:: These six stand for the two versions of each of three structural rules; one for use on the left ('L') of a
3361:
3157:{\displaystyle R\lnot {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}}
3072:{\displaystyle L\lnot {\text{rule: }}\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}}
293:. This leads to the idea of including the deduction theorem as a formal rule in the system, which happens in
212:
11800:
Alternatively, one may restrict or forbid the use of some of the structural rules. This yields a variety of
7553:
7474:
1718:
This is written in the following form, where the proposition that needs to be proven is to the right of the
88:
Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left.
9481:
6375:
ones. Each of the logical rules introduces a new logical formula either on the left or on the right of the
12765:
on 2 November 2015, in his
Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip
7727:
7245:
13362:
13347:
13255:
11187:
7874:
2238:
1620:
140:
sharing a certain style of inference and certain formal properties. The first sequent calculi systems,
13285:
13013:
12975:
11282:
9303:
9224:
5619:{\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)}
5511:{\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)}
5401:{\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)}
5293:{\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)}
4473:{\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})}
4275:{\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})}
3410:
are finite (possibly empty) sequences of formulae (in fact, the order of formulae does not matter; see
782:
are equivalent in the strong sense that a proof of either one may be extended to a proof of the other.
13250:
12697:, p. 191. "Die damit erreichte Symmetrie erweist sich als fĂŒr die klassische Logik angemessener."
8809:
8736:
7394:
7217:
12980:
11317:
10999:
10843:
10396:
9536:
8307:{\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)}
6404:
4571:{\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})}
4373:{\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})}
11374:. In this case, the rules for permuting and (when using sets) contracting formulae are unnecessary.
2180:
13397:
12128:
12066:
9941:
9656:
6707:
6310:
6279:
5983:{\displaystyle {\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})}
5890:{\displaystyle {\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})}
3356:
denote formulae of first-order predicate logic (one may also restrict this to propositional logic),
2324:
2280:
2206:
1826:{\displaystyle \vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}
220:, which things may appear as the conclusion of a (sub)proof. The simplest judgment form is used in
112:
so that unquantified logical expressions can be manipulated according to the much simpler rules of
7600:
7435:
6738:
5183:{\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)}
5095:{\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)}
13337:
13172:
12390:
11813:
9137:
8981:
8326:
8181:
8052:
7939:
7805:
7776:
7188:
6844:
169:
12811:
11831:
11425:
6528:
12097:
11981:
11824:
Surprisingly, some small changes in the rules of LK suffice to turn it into a proof system for
11598:
9350:
9070:
8914:
8704:
8669:
7362:
7327:
7276:
7018:, respectively. Note that, given some antecedent, it is not clear how this is to be split into
5795:{\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})}
5714:{\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})}
1577:
1275:{\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})}
113:
109:
97:
Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right.
12012:
9192:
7101:
6875:
6679:
6502:
3572:
3552:
2381:
The usual term for the horizontal line used in
Gentzen-style layouts for natural deduction is
1018:
533:
51:, giving a better approximation to the natural style of deduction used by mathematicians than
13392:
12735:
12444:, pp. 208â213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.
12041:
11263:
7041:
7021:
7001:
6961:
6921:
6901:
6639:
6619:
6599:
6559:
6482:
6442:
6381:
3948:
3455:
3424:
3285:
1724:
466:
432:
13240:
11173:
presentation, in the original style of
Gentzen. A common simplification involves the use of
9637:{\displaystyle \left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A}
1708:{\displaystyle ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}
13322:
11978:
In fact, the only rules in LK that need to be restricted to single-formula consequents are
11825:
11720:
11580:
11233:
3228:
1077:
1047:
931:
904:
613:
586:
583:
The standard semantics of a judgment in natural deduction is that it asserts that whenever
556:
486:
385:
161:
10697:
10551:
10252:
10122:
9802:
9271:
9105:
8949:
8777:
7695:
7521:
3393:
1293:
the semantics of the sequent can also (by propositional tautology) be expressed either as
8:
13119:
13097:
12752:
11801:
11795:
11217:
9452:
9041:
8885:
8640:
7845:
7298:
7192:
2363:
2079:
2001:
1837:
1616:
1590:
1560:
271:
193:
13169:
An
Introduction to Proof Theory â Normalization, Cut-Elimination, and Consistency Proofs
3925:
3902:
3879:
3856:
3833:
3810:
1836:
Now, instead of proving this from the axioms, it is enough to assume the premise of the
13033:
12997:
12395:
12252:
11657:
Or if, as described above, weakening is to be an admissible rule, then with the axiom:
11239:
7170:
7150:
7130:
7081:
7061:
6981:
6941:
6803:
6766:
6659:
6579:
6462:
6376:
6341:
3983:
3771:
3751:
3731:
3711:
3691:
3671:
3651:
3631:
3594:
3525:
3505:
3483:
3339:
3319:
3303:
1719:
998:
978:
958:
878:
640:
513:
460:
412:
279:
253:
230:
133:
20:
12909:
Proceedings Of The Third Annual Symposium On Logic In Computer Science, July 5-8, 1988
12777:
1602:
13220:
13198:
13176:
13149:
13127:
13105:
13083:
13057:
13037:
13001:
12957:
12935:
12929:
12593:
12574:
12385:
11210:
3268:
306:
294:
290:
153:
149:
91:
68:
36:
13056:. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7).
210:
One way to classify different styles of deduction systems is to look at the form of
13190:
13045:
13025:
12989:
12366:{\displaystyle {\cfrac {\Gamma \vdash A\lor C}{\Gamma \vdash (\forall xA)\lor C}}.}
11809:
11370:
First of all, as mentioned above, the sequents can be viewed to consist of sets or
1910:{\displaystyle (p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r}
13050:
12612:
For explanations of the disjunctive semantics for the right side of sequents, see
12582:
790:
Finally, sequent calculus generalizes the form of a natural deduction judgment to
13327:
13272:
13009:
12971:
11378:
11344:
6837:
holds for any value of y. The other rules should then be pretty straightforward.
1555:(it cannot be the case that all of the As are true and all of the Bs are false).
1290:
157:
44:
12239:{\displaystyle {\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}}
11737:, negation can be subsumed as a special case of implication, via the definition
1840:
and then try to prove its conclusion. Hence one moves to the following sequent:
13212:
12925:
12812:
An Introduction to the Theory and Applications of Propositional Sequent Calculi
11311:
8162:{\displaystyle \forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)}
7208:
3244:
221:
205:
82:
75:
2318:
The second sequent is done; the first sequent can be further simplified into:
13386:
13071:
12949:
12760:
12748:
1589:
The word "sequent" is taken from the word "Sequenz" in Gentzen's 1934 paper.
1570:
483:", with a single formula on the right-hand side, (though permutations of the
137:
117:
94:. Every (conditional) line has exactly one asserted proposition on the right.
52:
13332:
13317:
13164:
13075:
12400:
11566:
3252:
877:
a syntactic object called a sequent. The formulas on left-hand side of the
129:
56:
32:
9440:
9030:
8874:
8870:
8866:
8862:
8858:
8628:
8624:
8620:
7833:
7286:
3212:
process terminates when no logical operators remain: The formula has been
13352:
13141:
12578:
3476:(at least one of the formulas must hold for any assignment of variables),
283:
274:
of first-order logic (or whatever logic the deduction system applies to,
177:
148:, were introduced in 1934/1935 by Gerhard Gentzen as a tool for studying
13372:
13244:
12814:(2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.
12459:, pp. 453, gives a very brief proof of the cut-elimination theorem.
1990:{\displaystyle (p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r}
13029:
12993:
12756:
2000:
Since the arguments in the left-hand side are assumed to be related by
173:
3965:, and the other on its right ('R'). The rules are abbreviated 'W' for
1606:
A rooted tree describing a proof finding procedure by sequent calculus
11257:
11229:
3224:
48:
13277:
12928:(1998). "An introduction to proof theory". In Samuel R. Buss (ed.).
12548:
12532:
11371:
11206:
11174:
772:{\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B}
28:
2078:
This is equivalent to proving the conclusion in both cases of the
1041:
The standard semantics of a sequent is an assertion that whenever
12573:
2068:{\displaystyle (p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r}
64:
40:
6704:
For an intuition about the quantifier rules, consider the rule
1615:
Sequent calculus can be seen as a tool for proving formulas in
11859:
is reformulated as follows (where C is an arbitrary formula):
11381:
if the axiom (I) is changed to derive any sequent of the form
6358:
must not occur free anywhere in the respective lower sequents.
3628:
denotes the formula that is obtained by substituting the term
867:{\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}
164:
versions, respectively). Gentzen's so-called "Main Theorem" (
11819:
6459:
can be concluded from some sequence of formulae that contain
1419:(at least one of the As is false, or one of the Bs is true)
1176:{\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}}
60:
13044:
3251:. The only inference rule in the systems mentioned above is
7191:
is thus crucial to the applications of sequent calculus in
12778:"Gentzen's original consistency proof and the Bar Theorem"
3263:
This section introduces the rules of the sequent calculus
1571:
Distinction between natural deduction and sequent calculus
510:'s are often immaterial). The theorems are those formulae
11198:
The structural rules deserve some additional discussion.
8033:{\displaystyle \forall x\left(p(x,y)\right)\vdash p(x,y)}
6252:
6113:
5972:
5879:
5784:
5703:
4152:
4149:
12452:
12450:
11707:{\displaystyle {\cfrac {}{\Gamma ,\bot \vdash \Delta }}}
3223:
truth values to the atomic symbols. Thus this system is
459:(possibly empty) of formulae on the left-hand side of a
85:. Every line is an unconditional tautology (or theorem).
12890:
of an extremely, totally different kind to the case of
12437:
12435:
12323:
12282:
12199:
12169:
11912:
11872:
11679:
11670:
11627:
11618:
11506:
11466:
6192:
6142:
6053:
6003:
5938:
5908:
5845:
5815:
5750:
5732:
5669:
5651:
5570:
5529:
5462:
5421:
5352:
5311:
5244:
5203:
5137:
5113:
5049:
5025:
4956:
4926:
4847:
4807:
4738:
4698:
4631:
4591:
4515:
4491:
4417:
4393:
4317:
4293:
4219:
4195:
4109:
4069:
4019:
4009:
3234:
3129:
3102:
3044:
3017:
2951:
2921:
2847:
2817:
2752:
2722:
2648:
2618:
2543:
2513:
2450:
2420:
188:. Since this early work, sequent calculi, also called
13082:(Second ed.). Berlin, New York: Springer-Verlag.
12326:
12285:
12202:
12172:
11915:
11875:
11682:
11673:
11630:
11621:
11509:
11469:
6367:
The above rules can be divided into two major groups:
6195:
6145:
6056:
6006:
5941:
5911:
5848:
5818:
5753:
5735:
5672:
5654:
5573:
5532:
5465:
5424:
5355:
5314:
5247:
5206:
5140:
5116:
5052:
5028:
4959:
4929:
4850:
4810:
4741:
4701:
4634:
4594:
4518:
4494:
4420:
4396:
4320:
4296:
4222:
4198:
4112:
4072:
4051:{\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)}
4022:
4012:
3132:
3105:
3047:
3020:
2954:
2924:
2850:
2820:
2755:
2725:
2651:
2621:
2546:
2516:
2453:
2423:
12447:
12278:
12255:
12165:
12131:
12100:
12069:
12044:
12015:
11984:
11868:
11834:
11743:
11723:
11666:
11614:
11583:
11462:
11428:
11387:
11320:
11285:
11266:
11242:
11034:
11002:
10878:
10846:
10732:
10700:
10586:
10554:
10431:
10399:
10287:
10255:
10157:
10125:
9983:
9944:
9837:
9805:
9698:
9659:
9571:
9539:
9484:
9455:
9385:
9353:
9306:
9274:
9227:
9195:
9140:
9108:
9073:
9044:
8984:
8952:
8917:
8888:
8812:
8780:
8739:
8707:
8672:
8643:
8497:
8361:
8329:
8216:
8184:
8087:
8055:
7974:
7942:
7877:
7848:
7808:
7779:
7730:
7698:
7642:
7603:
7556:
7524:
7477:
7438:
7397:
7365:
7330:
7301:
7248:
7220:
7173:
7153:
7133:
7104:
7084:
7064:
7044:
7024:
7004:
6984:
6964:
6944:
6924:
6904:
6878:
6847:
6806:
6769:
6741:
6710:
6701:
holds. All the rules can be interpreted in this way.
6682:
6662:
6642:
6622:
6602:
6582:
6562:
6531:
6505:
6485:
6465:
6445:
6407:
6384:
6344:
6313:
6282:
6138:
5999:
5904:
5811:
5728:
5647:
5525:
5417:
5307:
5199:
5109:
5021:
4922:
4803:
4694:
4587:
4487:
4389:
4289:
4191:
4065:
4005:
3951:
3928:
3905:
3882:
3859:
3836:
3813:
3774:
3754:
3734:
3714:
3694:
3674:
3654:
3634:
3597:
3575:
3555:
3528:
3508:
3486:
3458:
3427:
3396:
3364:
3342:
3322:
3288:
3174:
3086:
3001:
2905:
2802:
2706:
2603:
2498:
2404:
2327:
2283:
2241:
2209:
2183:
2136:
2091:
2013:
1929:
1849:
1750:
1727:
1635:
1584:
1431:
1304:
1195:
1111:
1080:
1050:
1021:
1001:
981:
961:
934:
907:
885:, and the formulas on right-hand side are called the
799:
724:
666:
643:
616:
589:
559:
536:
516:
489:
469:
435:
415:
388:
320:
256:
233:
12432:
11236:
with respect to first-order logic, i.e. a statement
74:
Sequent calculus is one of several extant styles of
12907:M. Tiomkin, "Proving unprovability", pp.22--26. In
3549:within a formula if it is not bound by quantifiers
13049:
12365:
12261:
12238:
12148:
12117:
12086:
12055:
12030:
12001:
11960:
11851:
11778:
11729:
11706:
11646:
11589:
11554:
11445:
11411:
11332:
11303:
11272:
11248:
11148:
11017:
10979:
10861:
10823:
10715:
10677:
10569:
10531:
10414:
10362:
10270:
10232:
10140:
10102:
9966:
9921:
9820:
9782:
9681:
9636:
9554:
9502:
9467:
9412:
9368:
9330:
9289:
9251:
9210:
9158:
9123:
9085:
9056:
9002:
8967:
8929:
8900:
8830:
8795:
8757:
8722:
8684:
8655:
8610:
8467:
8344:
8306:
8199:
8161:
8070:
8032:
7957:
7919:
7860:
7823:
7794:
7748:
7713:
7676:{\displaystyle \vdash A\lor \lnot A,A\lor \lnot A}
7675:
7625:
7580:
7539:
7501:
7460:
7415:
7380:
7342:
7313:
7266:
7226:
7179:
7159:
7139:
7116:
7090:
7070:
7050:
7030:
7010:
6990:
6970:
6950:
6930:
6910:
6890:
6864:
6829:
6792:
6755:
6727:
6693:
6668:
6648:
6628:
6608:
6588:
6568:
6548:
6517:
6491:
6471:
6451:
6431:
6390:
6350:
6330:
6299:
6262:
6123:
5982:
5889:
5794:
5713:
5618:
5510:
5400:
5292:
5182:
5094:
5004:
4907:
4786:
4679:
4570:
4472:
4372:
4274:
4162:
4050:
3957:
3937:
3914:
3891:
3868:
3845:
3822:
3797:
3760:
3740:
3720:
3700:
3680:
3660:
3640:
3620:
3581:
3561:
3534:
3514:
3492:
3464:
3433:
3402:
3382:
3348:
3328:
3294:
3198:
3156:
3071:
2984:
2890:
2785:
2691:
2586:
2483:
2351:
2307:
2268:
2224:
2195:
2166:
2121:
2067:
1989:
1909:
1825:
1733:
1707:
1542:
1406:
1274:
1175:
1093:
1063:
1030:
1007:
987:
967:
947:
920:
866:
771:
704:
649:
629:
602:
572:
545:
522:
502:
475:
447:
421:
401:
371:
262:
239:
199:
13162:
12418:
12416:
11359:The above rules can be modified in various ways:
372:{\displaystyle A_{1},A_{2},\ldots ,A_{n}\vdash B}
13384:
13014:"Untersuchungen ĂŒber das logische SchlieĂen. II"
12850:, p. 194, wrote: "Der Unterschied zwischen
11362:
11181:
12976:"Untersuchungen ĂŒber das logische SchlieĂen. I"
11647:{\displaystyle {\cfrac {}{\bot \vdash \quad }}}
11347:. This result is also referred to as Gentzen's
311:In natural deduction, judgments have the shape
78:for expressing line-by-line logical arguments.
13070:
12785:Gentzen's Centenary: The Quest for Consistency
12625:
12581:; Stringer-Calvert, David W. J. (2001-11-01).
12413:
12376:These rules are not intuitionistically valid.
11223:
8491:For something more interesting we shall prove
2177:In the case of the first judgment, we rewrite
13293:
11228:This system of rules can be shown to be both
7187:(since it does not appear at all below). The
63:. In that case, sequents signify conditional
13273:Interactive tutorial of the Sequent Calculus
12731:
12729:
12727:
11804:systems. They are generally weaker than LK (
11569:, these rules define different connectives.
6439:. It says that, whenever one can prove that
300:
182:proof of the consistency of Peano arithmetic
12269:does not occur free in the bottom sequent)
6362:
1597:
785:
705:{\displaystyle A_{1},\ldots ,A_{n}\vdash B}
455:. In other words, a judgment consists of a
13300:
13286:
12801:, Cambridge University Press, 2014, p. 32.
12736:Applied Logic, Univ. of Cornell: Lecture 9
12676:, p. 191. "In dem klassischen KalkĂŒl
12567:
11820:Intuitionistic sequent calculus: System LJ
11760:
11756:
7207:states that the rule can be restricted to
3648:for every free occurrence of the variable
2167:{\displaystyle q\rightarrow r,p,q\vdash r}
2122:{\displaystyle p\rightarrow r,p,q\vdash r}
13219:. Mineola, New York: Dover Publications.
13126:. Mineola, New York: Dover Publications.
12724:
11779:{\displaystyle (\neg A)\iff (A\to \bot )}
11412:{\displaystyle \Gamma ,A\vdash A,\Delta }
10393:
9533:
9189:
3472:, the sequence of formulas is considered
3441:, the sequence of formulas is considered
3199:{\displaystyle \Gamma ,A\vdash \Delta ,A}
2004:, this can be replaced by the following:
13189:
12823:
12629:
12504:
12038:(which can be seen as a special case of
11028:
10872:
10726:
10580:
10425:
10281:
10151:
9977:
9831:
9692:
9565:
9478:
9379:
9300:
9221:
9134:
9067:
8978:
8911:
8806:
8733:
8666:
8355:
8210:
8081:
7968:
7871:
7724:
7636:
7550:
7471:
7391:
7324:
3748:(i.e., no occurrence of any variable in
3255:, which is implemented by the cut rule.
3248:
1601:
13008:
12970:
12847:
12787:. New York: Springer. pp. 213â228.
12706:
12694:
12673:
12657:
12633:
12426:
12422:
11789:
9413:{\displaystyle B\lor C,\lnot C\vdash B}
7205:completeness of atomic initial sequents
3445:(all assumed to hold at the same time),
3383:{\displaystyle \Gamma ,\Delta ,\Sigma }
13385:
13211:
13140:
13118:
13096:
12835:
12741:
12718:
12685:wird diese Sonderstellung aufgehoben."
12621:
12617:
12552:
12544:
12528:
12492:
12480:
12456:
7581:{\displaystyle \vdash A,A\lor \lnot A}
7502:{\displaystyle \vdash A\lor \lnot A,A}
7237:
13307:
13281:
12948:
12613:
12516:
12468:
12441:
11343:In the sequent calculus, the rule of
9503:{\displaystyle \lnot A\vdash \lnot A}
3411:
3279:The following notation will be used:
71:rather than conditional tautologies.
16:Style of formal logical argumentation
13343:Propositional directed acyclic graph
13048:; Paul Taylor; Yves Lafont (1990) .
12956:. New York: Dover Publications Inc.
12924:
12882:logic is in the case of the calculi
12775:
12769:
12645:
11973:disjunction and existence properties
7749:{\displaystyle \vdash A\lor \lnot A}
7267:{\displaystyle \vdash A\lor \lnot A}
6636:alone one can either still conclude
6499:from the (stronger) assumption that
3235:Relation to standard axiomatizations
2232:and split the sequent again to get:
1038:is the conclusion of a valid proof.
13268:A Brief Diversion: Sequent Calculus
13245:Stanford Encyclopedia of Philosophy
12866:Ă€uĂerlich ganz anderer Art als bei
11340:can be derived by the above rules.
11193:
7920:{\displaystyle p(x,y)\vdash p(x,y)}
3688:with the restriction that the term
3231:for classical propositional logic.
2269:{\displaystyle \lnot p,p,q\vdash r}
13:
12664:hat manche formale Unschönheiten."
12337:
12328:
12287:
12204:
12174:
12136:
12074:
12019:
11917:
11893:
11877:
11770:
11747:
11724:
11696:
11690:
11684:
11632:
11584:
11541:
11535:
11517:
11511:
11499:
11487:
11483:
11471:
11406:
11388:
11321:
11289:
11267:
11130:
11116:
11102:
10966:
10952:
10938:
10815:
10801:
10787:
10669:
10617:
10603:
10523:
10514:
10462:
10448:
10354:
10318:
10304:
10224:
10210:
10196:
10094:
10080:
10066:
10036:
10022:
9913:
9904:
9890:
9876:
9774:
9760:
9746:
9721:
9628:
9614:
9594:
9494:
9485:
9398:
9357:
8822:
8743:
8711:
8591:
8577:
8563:
8426:
8415:
8373:
8362:
8333:
8270:
8228:
8217:
8188:
8125:
8088:
8059:
7975:
7946:
7812:
7783:
7740:
7667:
7652:
7572:
7487:
7401:
7369:
7258:
7045:
7025:
7005:
6965:
6925:
6905:
6742:
6715:
6684:
6643:
6623:
6603:
6563:
6536:
6486:
6446:
6318:
6287:
6249:
6229:
6204:
6197:
6179:
6154:
6147:
6110:
6096:
6084:
6059:
6046:
6034:
6009:
5969:
5955:
5943:
5931:
5913:
5876:
5862:
5850:
5838:
5820:
5781:
5767:
5755:
5743:
5737:
5700:
5686:
5674:
5662:
5656:
5606:
5593:
5581:
5575:
5563:
5534:
5498:
5485:
5473:
5467:
5455:
5426:
5388:
5375:
5363:
5357:
5345:
5316:
5280:
5267:
5255:
5249:
5237:
5208:
5170:
5157:
5148:
5142:
5130:
5118:
5082:
5069:
5060:
5054:
5042:
5030:
4979:
4961:
4949:
4931:
4882:
4876:
4858:
4852:
4840:
4828:
4824:
4812:
4761:
4743:
4731:
4719:
4715:
4703:
4654:
4636:
4624:
4612:
4608:
4596:
4538:
4520:
4508:
4496:
4440:
4422:
4410:
4398:
4340:
4322:
4310:
4298:
4242:
4224:
4212:
4200:
4146:
4132:
4126:
4120:
4114:
4102:
4096:
4080:
4074:
3576:
3556:
3397:
3377:
3371:
3365:
3274:
3187:
3175:
3146:
3134:
3119:
3113:
3107:
3090:
3055:
3049:
3037:
3028:
3022:
3005:
2968:
2956:
2932:
2926:
2880:
2868:
2858:
2852:
2840:
2822:
2763:
2757:
2733:
2727:
2681:
2669:
2665:
2653:
2641:
2623:
2570:
2564:
2554:
2548:
2524:
2518:
2473:
2455:
2443:
2425:
2242:
2210:
1610:
1524:
1502:
1486:
1435:
1346:
1324:
1308:
136:, sequent calculus is a family of
14:
13414:
13234:
12954:Foundations of mathematical logic
12911:(1988), IEEE. ISBN 0-8186-0853-6.
11304:{\displaystyle (\Gamma \vDash A)}
9331:{\displaystyle B\lor C\vdash C,B}
9252:{\displaystyle B\lor C\vdash B,C}
7211:without any loss of provability.
657:will also be true. The judgments
13371:
13197:. New York: Dover Publications.
13163:Mancosu, Paolo; Galvan, Sergio;
12783:. In Kahle R, Rathjen M (eds.).
8831:{\displaystyle \vdash A,\lnot A}
8758:{\displaystyle \vdash \lnot A,A}
7416:{\displaystyle \vdash \lnot A,A}
7227:{\displaystyle \not \leftarrow }
7098:, one can construct a proof for
3258:
3241:Jan Ćukasiewicz's axiomatization
1626:Consider the following formula:
224:, where a judgment has the form
13102:Introduction to metamathematics
12901:
12841:
12829:
12817:
12804:
12791:
12712:
12700:
12688:
12667:
12651:
12639:
12606:
12558:
12538:
11943:
11892:
11638:
11486:
11333:{\displaystyle \Gamma \vdash A}
11018:{\displaystyle (\rightarrow R)}
10862:{\displaystyle (\rightarrow R)}
10415:{\displaystyle (\rightarrow L)}
9555:{\displaystyle (\rightarrow L)}
6432:{\displaystyle ({\land }L_{1})}
6243:
6104:
5963:
5870:
5775:
5694:
5601:
5493:
5383:
5275:
5165:
5077:
4987:
4890:
4827:
4769:
4718:
4662:
4611:
4546:
4448:
4348:
4250:
4140:
4089:
4038:
4014:
3243:(itself a part of the standard
3098:
3013:
2917:
2867:
2718:
2668:
2563:
2416:
222:Hilbert-style deduction systems
200:Hilbert-style deduction systems
186:Gödel's incompleteness theorems
13241:Proof Theory (Sequent Calculi)
12522:
12510:
12498:
12486:
12474:
12462:
12346:
12334:
12310:
12296:
12222:
12216:
12210:
12143:
12132:
12112:
12105:
12101:
12081:
12070:
12046:
12025:
12016:
11996:
11989:
11985:
11955:
11944:
11846:
11835:
11773:
11767:
11761:
11757:
11753:
11744:
11440:
11429:
11377:The rule of weakening becomes
11298:
11286:
11127:
11099:
11078:
11051:
11012:
11006:
11003:
10963:
10935:
10887:
10856:
10850:
10847:
10784:
10741:
10710:
10701:
10639:
10600:
10564:
10555:
10484:
10445:
10409:
10403:
10400:
10301:
10265:
10256:
10193:
10135:
10126:
10063:
10019:
9961:
9945:
9873:
9815:
9806:
9743:
9676:
9660:
9611:
9549:
9543:
9540:
9462:
9456:
9363:
9354:
9284:
9275:
9205:
9196:
9118:
9109:
9051:
9045:
8962:
8953:
8895:
8889:
8790:
8781:
8717:
8708:
8650:
8644:
8588:
8560:
8539:
8512:
8452:
8440:
8399:
8387:
8339:
8330:
8296:
8284:
8254:
8242:
8194:
8185:
8151:
8139:
8114:
8102:
8065:
8056:
8027:
8015:
8001:
7989:
7952:
7943:
7914:
7902:
7893:
7881:
7855:
7849:
7818:
7809:
7789:
7780:
7708:
7699:
7620:
7604:
7534:
7525:
7455:
7439:
7375:
7366:
7308:
7302:
6859:
6848:
6824:
6810:
6787:
6773:
6763:holds just from the fact that
6722:
6711:
6543:
6532:
6426:
6408:
6325:
6314:
6294:
6283:
6257:
6244:
6118:
6105:
5977:
5964:
5884:
5871:
5789:
5776:
5708:
5695:
5613:
5602:
5557:
5543:
5505:
5494:
5449:
5435:
5395:
5384:
5339:
5325:
5287:
5276:
5231:
5217:
5177:
5166:
5089:
5078:
4999:
4992:
4988:
4970:
4902:
4895:
4891:
4867:
4781:
4770:
4674:
4663:
4565:
4547:
4467:
4449:
4367:
4349:
4269:
4251:
4157:
4141:
4045:
4039:
3792:
3778:
3708:must be free for the variable
3615:
3601:
2941:
2909:
2831:
2806:
2196:{\displaystyle p\rightarrow r}
2187:
2140:
2095:
2044:
2038:
2032:
2026:
2020:
2014:
1978:
1966:
1960:
1954:
1948:
1942:
1936:
1930:
1901:
1898:
1886:
1880:
1874:
1868:
1862:
1856:
1850:
1820:
1814:
1811:
1799:
1796:
1793:
1790:
1787:
1781:
1775:
1769:
1763:
1757:
1754:
1702:
1696:
1693:
1681:
1678:
1675:
1672:
1669:
1663:
1657:
1651:
1645:
1639:
1636:
1537:
1438:
1269:
1237:
1234:
1231:
1199:
763:
760:
728:
278:, propositional calculus or a
1:
12918:
12799:Elements of Logical Reasoning
12149:{\displaystyle ({\forall }R)}
12087:{\displaystyle ({\forall }R)}
11453:may be instead formulated as
11363:Minor structural alternatives
11182:Relation to analytic tableaux
9967:{\displaystyle (\land L_{2})}
9682:{\displaystyle (\land L_{1})}
9439:
9029:
8873:
8865:
8857:
8627:
6898:follows from the assumptions
6728:{\displaystyle ({\forall }R)}
6479:, then one can also conclude
6331:{\displaystyle ({\exists }L)}
6300:{\displaystyle ({\forall }R)}
2352:{\displaystyle p,q\vdash p,r}
2308:{\displaystyle r,p,q\vdash r}
2225:{\displaystyle \lnot p\lor r}
172:, a result with far-reaching
27:is a style of formal logical
13104:. Ishi Press International.
13080:Grundlagen der Mathematik II
12747:"Remember, the way that you
12738:. Last Retrieved: 2016-06-25
11572:
7626:{\displaystyle (\lor R_{1})}
7461:{\displaystyle (\lor R_{2})}
6938:, it suffices to prove that
6756:{\displaystyle \forall {x}A}
6735:. Of course concluding that
3545:a variable is said to occur
184:, in surprising response to
7:
13363:Method of analytic tableaux
13348:Sentential decision diagram
13256:Encyclopedia of Mathematics
13010:Gentzen, Gerhard Karl Erich
12972:Gentzen, Gerhard Karl Erich
12934:. Elsevier. pp. 1â78.
12858:Logik ist bei den KalkĂŒlen
12660:, p. 188. "Der KalkĂŒl
12379:
11354:
11224:Properties of the system LK
9159:{\displaystyle C\vdash B,C}
9003:{\displaystyle B\vdash B,C}
8345:{\displaystyle (\forall R)}
8200:{\displaystyle (\exists L)}
8071:{\displaystyle (\exists R)}
7958:{\displaystyle (\forall L)}
7824:{\displaystyle (\exists L)}
7795:{\displaystyle (\forall R)}
7242:Here is the derivation of "
6865:{\displaystyle ({\land }R)}
6276:Restrictions: In the rules
1621:method of analytic tableaux
893:; together they are called
123:
10:
13419:
12626:Hilbert & Bernays 1970
12063:, as described above) and
11852:{\displaystyle ({\lor }L)}
11793:
11446:{\displaystyle ({\lor }L)}
6549:{\displaystyle ({\neg }R)}
6525:holds. Likewise, the rule
3500:denotes an arbitrary term,
304:
203:
168:) about LK and LJ was the
13403:Automated theorem proving
13369:
13313:
13191:Smullyan, Raymond Merrill
13018:Mathematische Zeitschrift
12981:Mathematische Zeitschrift
12118:{\displaystyle ({\to }R)}
12002:{\displaystyle ({\to }R)}
10996:
10840:
10694:
10548:
10249:
10119:
9938:
9799:
9653:
9449:
9369:{\displaystyle (\lnot L)}
9347:
9268:
9102:
9086:{\displaystyle C\vdash C}
9038:
8946:
8930:{\displaystyle B\vdash B}
8882:
8774:
8723:{\displaystyle (\lnot R)}
8701:
8685:{\displaystyle A\vdash A}
8637:
8323:
8178:
8049:
7936:
7842:
7692:
7597:
7518:
7432:
7381:{\displaystyle (\lnot R)}
7359:
7343:{\displaystyle A\vdash A}
7295:
6872:says that, to prove that
3167:
301:Natural deduction systems
31:in which every line of a
12931:Handbook of proof theory
12406:
12031:{\displaystyle (\neg R)}
9211:{\displaystyle (\lor L)}
7117:{\displaystyle A\land B}
6891:{\displaystyle A\land B}
6694:{\displaystyle {\neg }A}
6518:{\displaystyle A\land B}
6363:An intuitive explanation
3582:{\displaystyle \exists }
3562:{\displaystyle \forall }
1598:Proving logical formulas
1585:Origin of word "sequent"
1031:{\displaystyle \vdash B}
786:Sequent calculus systems
546:{\displaystyle \vdash B}
176:consequences, including
13338:Binary decision diagram
13213:Suppes, Patrick Colonel
13173:Oxford University Press
12632:, pp. 104â105 and
12391:Nested sequent calculus
12056:{\displaystyle {\to }R}
11814:artificial intelligence
11273:{\displaystyle \Gamma }
11260:from a set of premises
7189:cut-elimination theorem
7051:{\displaystyle \Sigma }
7031:{\displaystyle \Gamma }
7011:{\displaystyle \Sigma }
6971:{\displaystyle \Gamma }
6931:{\displaystyle \Sigma }
6911:{\displaystyle \Gamma }
6649:{\displaystyle \Delta }
6629:{\displaystyle \Gamma }
6609:{\displaystyle \Delta }
6569:{\displaystyle \Gamma }
6492:{\displaystyle \Delta }
6452:{\displaystyle \Delta }
6391:{\displaystyle \vdash }
5637:Right structural rules
3958:{\displaystyle \vdash }
3465:{\displaystyle \vdash }
3434:{\displaystyle \vdash }
3412:§ Structural rules
3295:{\displaystyle \vdash }
1734:{\displaystyle \vdash }
476:{\displaystyle \vdash }
448:{\displaystyle n\geq 0}
429:are again formulae and
170:cut-elimination theorem
104:more on sets of rules.
12367:
12263:
12240:
12150:
12119:
12088:
12057:
12032:
12003:
11962:
11853:
11780:
11731:
11708:
11648:
11591:
11556:
11447:
11413:
11334:
11305:
11274:
11250:
11150:
11019:
10981:
10863:
10825:
10717:
10679:
10571:
10533:
10416:
10364:
10272:
10234:
10142:
10104:
9968:
9923:
9822:
9784:
9683:
9638:
9556:
9504:
9469:
9414:
9370:
9332:
9291:
9253:
9212:
9160:
9125:
9087:
9058:
9004:
8969:
8931:
8902:
8832:
8797:
8759:
8724:
8686:
8657:
8612:
8469:
8346:
8308:
8201:
8163:
8072:
8034:
7959:
7921:
7862:
7825:
7796:
7750:
7715:
7677:
7627:
7582:
7541:
7503:
7462:
7417:
7382:
7344:
7315:
7277:Law of excluded middle
7268:
7228:
7181:
7161:
7141:
7118:
7092:
7072:
7052:
7032:
7012:
6998:can be concluded from
6992:
6972:
6958:can be concluded from
6952:
6932:
6912:
6892:
6866:
6831:
6794:
6757:
6729:
6695:
6670:
6650:
6630:
6610:
6590:
6570:
6550:
6519:
6493:
6473:
6453:
6433:
6392:
6352:
6332:
6301:
6264:
6125:
5984:
5891:
5796:
5715:
5634:Left structural rules
5620:
5512:
5402:
5294:
5184:
5096:
5006:
4909:
4788:
4681:
4572:
4474:
4374:
4276:
4164:
4052:
3967:Weakening (Left/Right)
3959:
3939:
3916:
3893:
3870:
3847:
3824:
3799:
3762:
3742:
3722:
3702:
3682:
3662:
3642:
3622:
3583:
3563:
3536:
3516:
3494:
3466:
3435:
3404:
3384:
3350:
3330:
3296:
3200:
3158:
3073:
2986:
2892:
2787:
2693:
2588:
2485:
2353:
2309:
2270:
2226:
2197:
2168:
2123:
2069:
1991:
1911:
1827:
1735:
1709:
1607:
1544:
1408:
1276:
1177:
1095:
1065:
1032:
1009:
989:
969:
949:
922:
868:
773:
706:
651:
637:, etc., are all true,
631:
604:
574:
547:
524:
504:
477:
449:
423:
403:
373:
264:
241:
114:propositional calculus
13217:Introduction to logic
12950:Curry, Haskell Brooks
12810:Andrzej-Indrzejczak,
12620:, pp. 290, 297,
12368:
12264:
12241:
12151:
12120:
12089:
12058:
12033:
12004:
11963:
11854:
11781:
11732:
11730:{\displaystyle \bot }
11709:
11649:
11592:
11590:{\displaystyle \bot }
11557:
11448:
11414:
11335:
11306:
11275:
11251:
11151:
11020:
10982:
10864:
10826:
10718:
10680:
10572:
10534:
10417:
10365:
10273:
10235:
10143:
10105:
9969:
9924:
9823:
9785:
9684:
9639:
9557:
9505:
9470:
9415:
9371:
9333:
9292:
9254:
9213:
9161:
9126:
9088:
9059:
9005:
8970:
8932:
8903:
8833:
8798:
8760:
8725:
8687:
8658:
8613:
8470:
8347:
8309:
8202:
8164:
8073:
8035:
7960:
7922:
7863:
7826:
7797:
7751:
7716:
7678:
7628:
7583:
7542:
7504:
7463:
7418:
7383:
7345:
7316:
7269:
7229:
7182:
7162:
7142:
7119:
7093:
7073:
7053:
7033:
7013:
6993:
6973:
6953:
6933:
6913:
6893:
6867:
6832:
6795:
6758:
6730:
6696:
6671:
6651:
6631:
6611:
6591:
6571:
6551:
6520:
6494:
6474:
6454:
6434:
6393:
6353:
6333:
6302:
6265:
6126:
5985:
5892:
5797:
5716:
5621:
5513:
5403:
5295:
5185:
5097:
5007:
4910:
4789:
4682:
4573:
4475:
4375:
4277:
4165:
4053:
3960:
3940:
3917:
3894:
3871:
3848:
3825:
3800:
3763:
3743:
3723:
3703:
3683:
3663:
3643:
3623:
3584:
3564:
3537:
3517:
3495:
3467:
3436:
3414:), called contexts,
3405:
3385:
3351:
3331:
3310:on the left from the
3297:
3201:
3159:
3074:
2987:
2893:
2788:
2694:
2589:
2486:
2374:appears on the left.
2354:
2310:
2271:
2227:
2198:
2169:
2124:
2070:
1992:
1912:
1828:
1736:
1710:
1605:
1545:
1409:
1277:
1178:
1096:
1094:{\displaystyle B_{i}}
1066:
1064:{\displaystyle A_{i}}
1033:
1010:
990:
970:
950:
948:{\displaystyle B_{i}}
923:
921:{\displaystyle A_{i}}
869:
774:
707:
652:
632:
630:{\displaystyle A_{2}}
605:
603:{\displaystyle A_{1}}
575:
573:{\displaystyle A_{i}}
548:
525:
505:
503:{\displaystyle A_{i}}
478:
450:
424:
404:
402:{\displaystyle A_{i}}
374:
265:
242:
13323:Square of opposition
13120:Kleene, Stephen Cole
13098:Kleene, Stephen Cole
12616:, pp. 189â190,
12276:
12253:
12163:
12129:
12098:
12067:
12042:
12013:
11982:
11866:
11832:
11826:intuitionistic logic
11790:Substructural logics
11741:
11721:
11664:
11612:
11581:
11460:
11426:
11385:
11318:
11283:
11264:
11240:
11218:substructural logics
11032:
11000:
10876:
10844:
10730:
10716:{\displaystyle (PL)}
10698:
10584:
10570:{\displaystyle (CR)}
10552:
10429:
10397:
10285:
10271:{\displaystyle (PL)}
10253:
10155:
10141:{\displaystyle (CL)}
10123:
9981:
9942:
9835:
9821:{\displaystyle (PL)}
9803:
9696:
9657:
9569:
9537:
9482:
9453:
9383:
9351:
9304:
9290:{\displaystyle (PR)}
9272:
9225:
9193:
9138:
9124:{\displaystyle (WR)}
9106:
9071:
9042:
8982:
8968:{\displaystyle (WR)}
8950:
8915:
8886:
8810:
8796:{\displaystyle (PR)}
8778:
8737:
8705:
8670:
8641:
8495:
8359:
8327:
8214:
8182:
8085:
8053:
7972:
7940:
7875:
7846:
7806:
7777:
7728:
7714:{\displaystyle (CR)}
7696:
7640:
7601:
7554:
7540:{\displaystyle (PR)}
7522:
7475:
7436:
7395:
7363:
7328:
7299:
7246:
7218:
7171:
7151:
7131:
7102:
7082:
7062:
7042:
7022:
7002:
6982:
6962:
6942:
6922:
6902:
6876:
6845:
6804:
6767:
6739:
6708:
6680:
6676:must be false, i.e.
6660:
6640:
6620:
6600:
6596:suffice to conclude
6580:
6560:
6529:
6503:
6483:
6463:
6443:
6405:
6382:
6342:
6311:
6280:
6136:
5997:
5902:
5809:
5726:
5645:
5523:
5415:
5305:
5197:
5107:
5019:
4920:
4801:
4692:
4585:
4485:
4387:
4287:
4189:
4181:Right logical rules
4063:
4003:
3949:
3926:
3903:
3880:
3857:
3834:
3811:
3772:
3752:
3732:
3712:
3692:
3672:
3652:
3632:
3595:
3573:
3553:
3526:
3506:
3484:
3456:
3425:
3403:{\displaystyle \Pi }
3394:
3362:
3340:
3320:
3286:
3172:
3084:
2999:
2903:
2800:
2704:
2601:
2496:
2402:
2325:
2281:
2239:
2207:
2181:
2134:
2089:
2011:
1927:
1847:
1748:
1725:
1633:
1429:
1302:
1193:
1109:
1078:
1048:
1019:
999:
979:
959:
932:
905:
797:
722:
664:
641:
614:
587:
557:
534:
514:
487:
467:
433:
413:
386:
318:
254:
231:
69:first-order language
13142:Lemmon, Edward John
12755:is by assuming the
12325:
12284:
12201:
12171:
11914:
11874:
11802:substructural logic
11796:Substructural logic
11681:
11672:
11629:
11620:
11508:
11468:
9468:{\displaystyle (I)}
9057:{\displaystyle (I)}
8901:{\displaystyle (I)}
8656:{\displaystyle (I)}
7861:{\displaystyle (I)}
7314:{\displaystyle (I)}
7238:Example derivations
7193:automated deduction
6194:
6144:
6055:
6005:
5940:
5910:
5847:
5817:
5752:
5734:
5671:
5653:
5572:
5531:
5464:
5423:
5354:
5313:
5246:
5205:
5139:
5115:
5051:
5027:
4958:
4928:
4849:
4809:
4740:
4700:
4633:
4593:
4517:
4493:
4419:
4395:
4319:
4295:
4221:
4197:
4178:Left logical rules
4111:
4071:
4021:
4011:
3131:
3104:
3046:
3019:
2953:
2923:
2849:
2819:
2754:
2724:
2650:
2620:
2545:
2515:
2452:
2422:
1617:propositional logic
194:automated deduction
13251:"Sequent calculus"
13124:Mathematical logic
13030:10.1007/bf01201363
12994:10.1007/BF01201353
12852:intuitionistischer
12583:"PVS Prover Guide"
12575:Shankar, Natarajan
12555:, pp. 25â150.
12396:Resolution (logic)
12363:
12356:
12320:
12259:
12236:
12232:
12196:
12146:
12115:
12084:
12053:
12028:
11999:
11958:
11939:
11909:
11849:
11776:
11727:
11704:
11700:
11676:
11644:
11640:
11624:
11605:, with the axiom:
11599:absurdity constant
11587:
11577:One can introduce
11552:
11545:
11503:
11443:
11409:
11351:("Main Theorem").
11330:
11301:
11270:
11246:
11146:
11015:
10977:
10859:
10821:
10713:
10675:
10567:
10529:
10412:
10360:
10268:
10230:
10138:
10100:
9964:
9919:
9818:
9780:
9679:
9634:
9552:
9500:
9465:
9410:
9366:
9328:
9287:
9249:
9208:
9156:
9121:
9083:
9054:
9000:
8965:
8927:
8898:
8828:
8793:
8755:
8720:
8682:
8653:
8608:
8465:
8342:
8304:
8197:
8159:
8068:
8030:
7955:
7917:
7858:
7821:
7792:
7746:
7711:
7673:
7623:
7578:
7537:
7499:
7458:
7413:
7378:
7340:
7311:
7264:
7224:
7177:
7157:
7137:
7114:
7088:
7068:
7048:
7028:
7008:
6988:
6968:
6948:
6928:
6908:
6888:
6862:
6827:
6790:
6753:
6725:
6691:
6666:
6646:
6626:
6606:
6586:
6566:
6546:
6515:
6489:
6469:
6449:
6429:
6388:
6348:
6328:
6297:
6260:
6239:
6189:
6121:
6100:
6050:
5980:
5959:
5935:
5887:
5866:
5842:
5792:
5771:
5747:
5711:
5690:
5666:
5616:
5597:
5567:
5508:
5489:
5459:
5398:
5379:
5349:
5290:
5271:
5241:
5180:
5161:
5134:
5092:
5073:
5046:
5002:
4983:
4953:
4905:
4886:
4844:
4784:
4765:
4735:
4677:
4658:
4628:
4568:
4542:
4512:
4470:
4444:
4414:
4370:
4344:
4314:
4272:
4246:
4216:
4160:
4136:
4106:
4048:
4034:
4016:
3955:
3938:{\displaystyle PR}
3935:
3915:{\displaystyle PL}
3912:
3892:{\displaystyle CR}
3889:
3869:{\displaystyle CL}
3866:
3846:{\displaystyle WR}
3843:
3823:{\displaystyle WL}
3820:
3795:
3758:
3738:
3718:
3698:
3678:
3658:
3638:
3618:
3579:
3559:
3532:
3512:
3490:
3462:
3431:
3400:
3380:
3346:
3326:
3292:
3196:
3154:
3150:
3126:
3069:
3065:
3041:
2982:
2978:
2948:
2888:
2884:
2844:
2783:
2779:
2749:
2689:
2685:
2645:
2584:
2580:
2540:
2481:
2477:
2447:
2349:
2305:
2266:
2222:
2193:
2164:
2119:
2065:
1987:
1907:
1823:
1731:
1705:
1608:
1540:
1404:
1272:
1173:
1091:
1061:
1028:
1005:
985:
965:
955:are formulae, and
945:
918:
864:
769:
702:
647:
627:
600:
570:
543:
520:
500:
473:
445:
419:
399:
369:
280:higher-order logic
260:
237:
134:mathematical logic
21:mathematical logic
13380:
13379:
13308:Diagrams in logic
13226:978-0-486-40687-9
13204:978-0-486-68370-6
13195:First-order logic
13182:978-0-19-289593-6
13148:. Thomas Nelson.
13133:978-0-486-42533-7
13111:978-0-923891-57-2
13089:978-3-642-86897-9
13046:Girard, Jean-Yves
12963:978-0-486-63462-3
12594:SRI International
12386:Cirquent calculus
12358:
12324:
12283:
12262:{\displaystyle y}
12234:
12200:
12170:
11941:
11913:
11873:
11702:
11680:
11671:
11642:
11628:
11619:
11547:
11507:
11467:
11345:cut is admissible
11249:{\displaystyle A}
11170:
11169:
10388:
10387:
10384:
10383:
9528:
9527:
9524:
9523:
9434:
9433:
9184:
9183:
9180:
9179:
9024:
9023:
8852:
8851:
8489:
8488:
7770:
7769:
7282:tertium non datur
7180:{\displaystyle A}
7160:{\displaystyle A}
7140:{\displaystyle A}
7091:{\displaystyle B}
7071:{\displaystyle A}
6991:{\displaystyle B}
6951:{\displaystyle A}
6830:{\displaystyle A}
6793:{\displaystyle A}
6669:{\displaystyle A}
6589:{\displaystyle A}
6472:{\displaystyle A}
6351:{\displaystyle y}
6273:
6272:
6241:
6193:
6143:
6102:
6054:
6004:
5961:
5939:
5909:
5868:
5846:
5816:
5773:
5751:
5733:
5692:
5670:
5652:
5629:
5628:
5599:
5571:
5530:
5491:
5463:
5422:
5381:
5353:
5312:
5273:
5245:
5204:
5163:
5138:
5114:
5075:
5050:
5026:
4985:
4957:
4927:
4888:
4848:
4808:
4767:
4739:
4699:
4660:
4632:
4592:
4544:
4516:
4492:
4446:
4418:
4394:
4346:
4318:
4294:
4248:
4220:
4196:
4173:
4172:
4138:
4110:
4070:
4036:
4020:
4010:
3798:{\displaystyle A}
3768:becomes bound in
3761:{\displaystyle t}
3741:{\displaystyle A}
3721:{\displaystyle x}
3701:{\displaystyle t}
3681:{\displaystyle A}
3661:{\displaystyle x}
3641:{\displaystyle t}
3621:{\displaystyle A}
3542:denote variables.
3535:{\displaystyle y}
3515:{\displaystyle x}
3493:{\displaystyle t}
3349:{\displaystyle B}
3329:{\displaystyle A}
3209:
3208:
3152:
3130:
3103:
3096:
3067:
3045:
3018:
3011:
2980:
2952:
2922:
2915:
2886:
2848:
2818:
2812:
2781:
2753:
2723:
2716:
2687:
2649:
2619:
2613:
2582:
2544:
2514:
2508:
2479:
2451:
2421:
2414:
1619:, similar to the
1291:classical context
1008:{\displaystyle B}
988:{\displaystyle k}
968:{\displaystyle n}
650:{\displaystyle B}
523:{\displaystyle B}
422:{\displaystyle B}
307:Natural deduction
295:natural deduction
291:deduction theorem
263:{\displaystyle B}
240:{\displaystyle B}
154:first-order logic
150:natural deduction
92:Natural deduction
55:earlier style of
35:is a conditional
13410:
13375:
13358:Sequent calculus
13302:
13295:
13288:
13279:
13278:
13264:
13230:
13208:
13186:
13159:
13137:
13115:
13093:
13067:
13055:
13052:Proofs and Types
13041:
13005:
12967:
12945:
12912:
12905:
12899:
12845:
12839:
12833:
12827:
12821:
12815:
12808:
12802:
12795:
12789:
12788:
12782:
12776:Tait WW (2010).
12773:
12767:
12745:
12739:
12733:
12722:
12716:
12710:
12704:
12698:
12692:
12686:
12671:
12665:
12655:
12649:
12643:
12637:
12610:
12604:
12603:
12601:
12600:
12587:
12571:
12565:
12562:
12556:
12542:
12536:
12526:
12520:
12514:
12508:
12502:
12496:
12490:
12484:
12478:
12472:
12466:
12460:
12454:
12445:
12439:
12430:
12420:
12372:
12370:
12369:
12364:
12359:
12357:
12355:
12321:
12319:
12306:
12280:
12268:
12266:
12265:
12260:
12245:
12243:
12242:
12237:
12235:
12233:
12231:
12197:
12195:
12167:
12155:
12153:
12152:
12147:
12139:
12124:
12122:
12121:
12116:
12108:
12093:
12091:
12090:
12085:
12077:
12062:
12060:
12059:
12054:
12049:
12037:
12035:
12034:
12029:
12008:
12006:
12005:
12000:
11992:
11967:
11965:
11964:
11959:
11951:
11942:
11940:
11938:
11910:
11908:
11870:
11858:
11856:
11855:
11850:
11842:
11810:computer science
11785:
11783:
11782:
11777:
11736:
11734:
11733:
11728:
11713:
11711:
11710:
11705:
11703:
11701:
11699:
11677:
11675:
11668:
11653:
11651:
11650:
11645:
11643:
11641:
11639:
11625:
11623:
11616:
11596:
11594:
11593:
11588:
11561:
11559:
11558:
11553:
11548:
11546:
11544:
11504:
11502:
11464:
11452:
11450:
11449:
11444:
11436:
11418:
11416:
11415:
11410:
11339:
11337:
11336:
11331:
11310:
11308:
11307:
11302:
11279:
11277:
11276:
11271:
11255:
11253:
11252:
11247:
11194:Structural rules
11188:analytic tableau
11155:
11153:
11152:
11147:
11145:
11141:
11140:
11136:
11126:
11122:
11112:
11108:
11077:
11073:
11072:
11068:
11024:
11022:
11021:
11016:
10986:
10984:
10983:
10978:
10976:
10972:
10962:
10958:
10948:
10944:
10913:
10909:
10908:
10904:
10868:
10866:
10865:
10860:
10830:
10828:
10827:
10822:
10811:
10807:
10797:
10793:
10767:
10763:
10762:
10758:
10722:
10720:
10719:
10714:
10684:
10682:
10681:
10676:
10665:
10661:
10660:
10656:
10627:
10623:
10613:
10609:
10576:
10574:
10573:
10568:
10538:
10536:
10535:
10530:
10510:
10506:
10505:
10501:
10472:
10468:
10458:
10454:
10421:
10419:
10418:
10413:
10369:
10367:
10366:
10361:
10350:
10346:
10328:
10324:
10314:
10310:
10277:
10275:
10274:
10269:
10239:
10237:
10236:
10231:
10220:
10216:
10206:
10202:
10176:
10172:
10147:
10145:
10144:
10139:
10109:
10107:
10106:
10101:
10090:
10086:
10076:
10072:
10046:
10042:
10032:
10028:
10002:
9998:
9973:
9971:
9970:
9965:
9960:
9959:
9928:
9926:
9925:
9920:
9900:
9896:
9886:
9882:
9856:
9852:
9827:
9825:
9824:
9819:
9789:
9787:
9786:
9781:
9770:
9766:
9756:
9752:
9717:
9713:
9688:
9686:
9685:
9680:
9675:
9674:
9643:
9641:
9640:
9635:
9624:
9620:
9590:
9586:
9561:
9559:
9558:
9553:
9509:
9507:
9506:
9501:
9474:
9472:
9471:
9466:
9441:
9419:
9417:
9416:
9411:
9375:
9373:
9372:
9367:
9337:
9335:
9334:
9329:
9296:
9294:
9293:
9288:
9258:
9256:
9255:
9250:
9217:
9215:
9214:
9209:
9165:
9163:
9162:
9157:
9130:
9128:
9127:
9122:
9092:
9090:
9089:
9084:
9063:
9061:
9060:
9055:
9031:
9009:
9007:
9006:
9001:
8974:
8972:
8971:
8966:
8936:
8934:
8933:
8928:
8907:
8905:
8904:
8899:
8875:
8871:
8867:
8863:
8859:
8837:
8835:
8834:
8829:
8802:
8800:
8799:
8794:
8764:
8762:
8761:
8756:
8729:
8727:
8726:
8721:
8691:
8689:
8688:
8683:
8662:
8660:
8659:
8654:
8629:
8625:
8621:
8617:
8615:
8614:
8609:
8607:
8606:
8602:
8601:
8597:
8587:
8583:
8573:
8569:
8538:
8534:
8533:
8529:
8474:
8472:
8471:
8466:
8464:
8460:
8459:
8455:
8411:
8407:
8406:
8402:
8351:
8349:
8348:
8343:
8313:
8311:
8310:
8305:
8303:
8299:
8266:
8262:
8261:
8257:
8206:
8204:
8203:
8198:
8168:
8166:
8165:
8160:
8158:
8154:
8121:
8117:
8077:
8075:
8074:
8069:
8039:
8037:
8036:
8031:
8008:
8004:
7964:
7962:
7961:
7956:
7926:
7924:
7923:
7918:
7867:
7865:
7864:
7859:
7834:
7830:
7828:
7827:
7822:
7801:
7799:
7798:
7793:
7755:
7753:
7752:
7747:
7720:
7718:
7717:
7712:
7682:
7680:
7679:
7674:
7632:
7630:
7629:
7624:
7619:
7618:
7587:
7585:
7584:
7579:
7546:
7544:
7543:
7538:
7508:
7506:
7505:
7500:
7467:
7465:
7464:
7459:
7454:
7453:
7422:
7420:
7419:
7414:
7387:
7385:
7384:
7379:
7349:
7347:
7346:
7341:
7320:
7318:
7317:
7312:
7287:
7274:", known as the
7273:
7271:
7270:
7265:
7233:
7231:
7230:
7225:
7186:
7184:
7183:
7178:
7166:
7164:
7163:
7158:
7146:
7144:
7143:
7138:
7123:
7121:
7120:
7115:
7097:
7095:
7094:
7089:
7077:
7075:
7074:
7069:
7057:
7055:
7054:
7049:
7037:
7035:
7034:
7029:
7017:
7015:
7014:
7009:
6997:
6995:
6994:
6989:
6977:
6975:
6974:
6969:
6957:
6955:
6954:
6949:
6937:
6935:
6934:
6929:
6917:
6915:
6914:
6909:
6897:
6895:
6894:
6889:
6871:
6869:
6868:
6863:
6855:
6836:
6834:
6833:
6828:
6820:
6799:
6797:
6796:
6791:
6783:
6762:
6760:
6759:
6754:
6749:
6734:
6732:
6731:
6726:
6718:
6700:
6698:
6697:
6692:
6687:
6675:
6673:
6672:
6667:
6655:
6653:
6652:
6647:
6635:
6633:
6632:
6627:
6615:
6613:
6612:
6607:
6595:
6593:
6592:
6587:
6575:
6573:
6572:
6567:
6556:states that, if
6555:
6553:
6552:
6547:
6539:
6524:
6522:
6521:
6516:
6498:
6496:
6495:
6490:
6478:
6476:
6475:
6470:
6458:
6456:
6455:
6450:
6438:
6436:
6435:
6430:
6425:
6424:
6415:
6397:
6395:
6394:
6389:
6357:
6355:
6354:
6349:
6337:
6335:
6334:
6329:
6321:
6306:
6304:
6303:
6298:
6290:
6269:
6267:
6266:
6261:
6256:
6255:
6242:
6240:
6238:
6237:
6236:
6212:
6211:
6190:
6188:
6187:
6186:
6162:
6161:
6140:
6130:
6128:
6127:
6122:
6117:
6116:
6103:
6101:
6099:
6092:
6091:
6067:
6066:
6051:
6049:
6042:
6041:
6017:
6016:
6001:
5989:
5987:
5986:
5981:
5976:
5975:
5962:
5960:
5958:
5936:
5934:
5906:
5896:
5894:
5893:
5888:
5883:
5882:
5869:
5867:
5865:
5843:
5841:
5813:
5801:
5799:
5798:
5793:
5788:
5787:
5774:
5772:
5770:
5748:
5746:
5730:
5720:
5718:
5717:
5712:
5707:
5706:
5693:
5691:
5689:
5667:
5665:
5649:
5631:
5630:
5625:
5623:
5622:
5617:
5609:
5600:
5598:
5596:
5568:
5566:
5553:
5527:
5517:
5515:
5514:
5509:
5501:
5492:
5490:
5488:
5460:
5458:
5445:
5419:
5407:
5405:
5404:
5399:
5391:
5382:
5380:
5378:
5350:
5348:
5335:
5309:
5299:
5297:
5296:
5291:
5283:
5274:
5272:
5270:
5242:
5240:
5227:
5201:
5189:
5187:
5186:
5181:
5173:
5164:
5162:
5160:
5135:
5133:
5111:
5101:
5099:
5098:
5093:
5085:
5076:
5074:
5072:
5047:
5045:
5023:
5011:
5009:
5008:
5003:
4995:
4986:
4984:
4982:
4954:
4952:
4924:
4914:
4912:
4911:
4906:
4898:
4889:
4887:
4885:
4845:
4843:
4805:
4793:
4791:
4790:
4785:
4777:
4768:
4766:
4764:
4736:
4734:
4696:
4686:
4684:
4683:
4678:
4670:
4661:
4659:
4657:
4629:
4627:
4589:
4577:
4575:
4574:
4569:
4564:
4563:
4554:
4545:
4543:
4541:
4513:
4511:
4489:
4479:
4477:
4476:
4471:
4466:
4465:
4456:
4447:
4445:
4443:
4415:
4413:
4391:
4379:
4377:
4376:
4371:
4366:
4365:
4356:
4347:
4345:
4343:
4315:
4313:
4291:
4281:
4279:
4278:
4273:
4268:
4267:
4258:
4249:
4247:
4245:
4217:
4215:
4193:
4175:
4174:
4169:
4167:
4166:
4161:
4156:
4155:
4139:
4137:
4135:
4107:
4105:
4067:
4057:
4055:
4054:
4049:
4037:
4035:
4033:
4017:
4015:
4007:
3989:
3988:
3964:
3962:
3961:
3956:
3944:
3942:
3941:
3936:
3921:
3919:
3918:
3913:
3898:
3896:
3895:
3890:
3875:
3873:
3872:
3867:
3852:
3850:
3849:
3844:
3829:
3827:
3826:
3821:
3804:
3802:
3801:
3796:
3788:
3767:
3765:
3764:
3759:
3747:
3745:
3744:
3739:
3727:
3725:
3724:
3719:
3707:
3705:
3704:
3699:
3687:
3685:
3684:
3679:
3667:
3665:
3664:
3659:
3647:
3645:
3644:
3639:
3627:
3625:
3624:
3619:
3611:
3588:
3586:
3585:
3580:
3568:
3566:
3565:
3560:
3541:
3539:
3538:
3533:
3521:
3519:
3518:
3513:
3499:
3497:
3496:
3491:
3471:
3469:
3468:
3463:
3440:
3438:
3437:
3432:
3409:
3407:
3406:
3401:
3389:
3387:
3386:
3381:
3355:
3353:
3352:
3347:
3335:
3333:
3332:
3327:
3306:, separates the
3301:
3299:
3298:
3293:
3205:
3203:
3202:
3197:
3163:
3161:
3160:
3155:
3153:
3151:
3149:
3127:
3125:
3100:
3097:
3094:
3078:
3076:
3075:
3070:
3068:
3066:
3064:
3042:
3040:
3015:
3012:
3009:
2991:
2989:
2988:
2983:
2981:
2979:
2977:
2949:
2947:
2919:
2916:
2913:
2897:
2895:
2894:
2889:
2887:
2885:
2883:
2845:
2843:
2815:
2813:
2810:
2792:
2790:
2789:
2784:
2782:
2780:
2778:
2750:
2748:
2720:
2717:
2714:
2698:
2696:
2695:
2690:
2688:
2686:
2684:
2646:
2644:
2616:
2614:
2611:
2593:
2591:
2590:
2585:
2583:
2581:
2579:
2541:
2539:
2511:
2509:
2506:
2490:
2488:
2487:
2482:
2480:
2478:
2476:
2448:
2446:
2418:
2415:
2412:
2388:
2387:
2358:
2356:
2355:
2350:
2314:
2312:
2311:
2306:
2275:
2273:
2272:
2267:
2231:
2229:
2228:
2223:
2202:
2200:
2199:
2194:
2173:
2171:
2170:
2165:
2128:
2126:
2125:
2120:
2074:
2072:
2071:
2066:
1996:
1994:
1993:
1988:
1916:
1914:
1913:
1908:
1832:
1830:
1829:
1824:
1740:
1738:
1737:
1732:
1720:turnstile symbol
1714:
1712:
1711:
1706:
1561:De Morgan's laws
1549:
1547:
1546:
1541:
1536:
1535:
1514:
1513:
1498:
1497:
1482:
1481:
1463:
1462:
1450:
1449:
1413:
1411:
1410:
1405:
1403:
1402:
1384:
1383:
1371:
1370:
1358:
1357:
1336:
1335:
1320:
1319:
1281:
1279:
1278:
1273:
1268:
1267:
1249:
1248:
1230:
1229:
1211:
1210:
1182:
1180:
1179:
1174:
1172:
1171:
1153:
1152:
1140:
1139:
1121:
1120:
1100:
1098:
1097:
1092:
1090:
1089:
1070:
1068:
1067:
1062:
1060:
1059:
1037:
1035:
1034:
1029:
1014:
1012:
1011:
1006:
994:
992:
991:
986:
974:
972:
971:
966:
954:
952:
951:
946:
944:
943:
927:
925:
924:
919:
917:
916:
873:
871:
870:
865:
860:
859:
841:
840:
828:
827:
809:
808:
778:
776:
775:
770:
759:
758:
740:
739:
711:
709:
708:
703:
695:
694:
676:
675:
656:
654:
653:
648:
636:
634:
633:
628:
626:
625:
609:
607:
606:
601:
599:
598:
579:
577:
576:
571:
569:
568:
552:
550:
549:
544:
529:
527:
526:
521:
509:
507:
506:
501:
499:
498:
482:
480:
479:
474:
454:
452:
451:
446:
428:
426:
425:
420:
408:
406:
405:
400:
398:
397:
378:
376:
375:
370:
362:
361:
343:
342:
330:
329:
269:
267:
266:
261:
246:
244:
243:
238:
25:sequent calculus
13418:
13417:
13413:
13412:
13411:
13409:
13408:
13407:
13398:Logical calculi
13383:
13382:
13381:
13376:
13367:
13328:Porphyrian tree
13309:
13306:
13249:
13237:
13227:
13205:
13183:
13175:. p. 431.
13156:
13146:Beginning logic
13134:
13112:
13090:
13064:
12964:
12942:
12926:Buss, Samuel R.
12921:
12916:
12915:
12906:
12902:
12846:
12842:
12834:
12830:
12822:
12818:
12809:
12805:
12797:Jan von Plato,
12796:
12792:
12780:
12774:
12770:
12746:
12742:
12734:
12725:
12717:
12713:
12705:
12701:
12693:
12689:
12672:
12668:
12656:
12652:
12644:
12640:
12628:, p. 385,
12624:, p. 441,
12611:
12607:
12598:
12596:
12585:
12579:Rushby, John M.
12572:
12568:
12563:
12559:
12543:
12539:
12527:
12523:
12515:
12511:
12503:
12499:
12491:
12487:
12479:
12475:
12467:
12463:
12455:
12448:
12440:
12433:
12421:
12414:
12409:
12382:
12327:
12322:
12302:
12286:
12281:
12279:
12277:
12274:
12273:
12254:
12251:
12250:
12203:
12198:
12173:
12168:
12166:
12164:
12161:
12160:
12135:
12130:
12127:
12126:
12104:
12099:
12096:
12095:
12073:
12068:
12065:
12064:
12045:
12043:
12040:
12039:
12014:
12011:
12010:
11988:
11983:
11980:
11979:
11947:
11916:
11911:
11876:
11871:
11869:
11867:
11864:
11863:
11838:
11833:
11830:
11829:
11822:
11798:
11792:
11742:
11739:
11738:
11722:
11719:
11718:
11683:
11678:
11674:
11669:
11667:
11665:
11662:
11661:
11631:
11626:
11622:
11617:
11615:
11613:
11610:
11609:
11582:
11579:
11578:
11575:
11510:
11505:
11470:
11465:
11463:
11461:
11458:
11457:
11432:
11427:
11424:
11423:
11386:
11383:
11382:
11365:
11357:
11319:
11316:
11315:
11284:
11281:
11280:
11265:
11262:
11261:
11241:
11238:
11237:
11226:
11196:
11184:
11095:
11091:
11090:
11086:
11085:
11081:
11058:
11054:
11047:
11043:
11042:
11038:
11033:
11030:
11029:
11001:
10998:
10997:
10931:
10927:
10926:
10922:
10921:
10917:
10894:
10890:
10883:
10879:
10877:
10874:
10873:
10845:
10842:
10841:
10780:
10776:
10775:
10771:
10748:
10744:
10737:
10733:
10731:
10728:
10727:
10699:
10696:
10695:
10646:
10642:
10635:
10631:
10596:
10592:
10591:
10587:
10585:
10582:
10581:
10553:
10550:
10549:
10491:
10487:
10480:
10476:
10441:
10437:
10436:
10432:
10430:
10427:
10426:
10398:
10395:
10394:
10336:
10332:
10297:
10293:
10292:
10288:
10286:
10283:
10282:
10254:
10251:
10250:
10189:
10185:
10184:
10180:
10162:
10158:
10156:
10153:
10152:
10124:
10121:
10120:
10059:
10055:
10054:
10050:
10015:
10011:
10010:
10006:
9988:
9984:
9982:
9979:
9978:
9955:
9951:
9943:
9940:
9939:
9869:
9865:
9864:
9860:
9842:
9838:
9836:
9833:
9832:
9804:
9801:
9800:
9739:
9735:
9734:
9730:
9703:
9699:
9697:
9694:
9693:
9670:
9666:
9658:
9655:
9654:
9607:
9603:
9576:
9572:
9570:
9567:
9566:
9538:
9535:
9534:
9483:
9480:
9479:
9454:
9451:
9450:
9384:
9381:
9380:
9352:
9349:
9348:
9305:
9302:
9301:
9273:
9270:
9269:
9226:
9223:
9222:
9194:
9191:
9190:
9139:
9136:
9135:
9107:
9104:
9103:
9072:
9069:
9068:
9043:
9040:
9039:
8983:
8980:
8979:
8951:
8948:
8947:
8916:
8913:
8912:
8887:
8884:
8883:
8811:
8808:
8807:
8779:
8776:
8775:
8738:
8735:
8734:
8706:
8703:
8702:
8671:
8668:
8667:
8642:
8639:
8638:
8556:
8552:
8551:
8547:
8546:
8542:
8519:
8515:
8508:
8504:
8503:
8499:
8498:
8496:
8493:
8492:
8436:
8432:
8425:
8421:
8383:
8379:
8372:
8368:
8360:
8357:
8356:
8328:
8325:
8324:
8280:
8276:
8238:
8234:
8227:
8223:
8215:
8212:
8211:
8183:
8180:
8179:
8135:
8131:
8098:
8094:
8086:
8083:
8082:
8054:
8051:
8050:
7985:
7981:
7973:
7970:
7969:
7941:
7938:
7937:
7876:
7873:
7872:
7847:
7844:
7843:
7807:
7804:
7803:
7778:
7775:
7774:
7729:
7726:
7725:
7697:
7694:
7693:
7641:
7638:
7637:
7614:
7610:
7602:
7599:
7598:
7555:
7552:
7551:
7523:
7520:
7519:
7476:
7473:
7472:
7449:
7445:
7437:
7434:
7433:
7396:
7393:
7392:
7364:
7361:
7360:
7329:
7326:
7325:
7300:
7297:
7296:
7247:
7244:
7243:
7240:
7219:
7216:
7215:
7209:atomic formulas
7172:
7169:
7168:
7152:
7149:
7148:
7132:
7129:
7128:
7103:
7100:
7099:
7083:
7080:
7079:
7063:
7060:
7059:
7043:
7040:
7039:
7023:
7020:
7019:
7003:
7000:
6999:
6983:
6980:
6979:
6963:
6960:
6959:
6943:
6940:
6939:
6923:
6920:
6919:
6903:
6900:
6899:
6877:
6874:
6873:
6851:
6846:
6843:
6842:
6816:
6805:
6802:
6801:
6779:
6768:
6765:
6764:
6745:
6740:
6737:
6736:
6714:
6709:
6706:
6705:
6683:
6681:
6678:
6677:
6661:
6658:
6657:
6641:
6638:
6637:
6621:
6618:
6617:
6601:
6598:
6597:
6581:
6578:
6577:
6561:
6558:
6557:
6535:
6530:
6527:
6526:
6504:
6501:
6500:
6484:
6481:
6480:
6464:
6461:
6460:
6444:
6441:
6440:
6420:
6416:
6411:
6406:
6403:
6402:
6383:
6380:
6379:
6365:
6343:
6340:
6339:
6338:, the variable
6317:
6312:
6309:
6308:
6286:
6281:
6278:
6277:
6248:
6247:
6232:
6228:
6207:
6203:
6196:
6191:
6182:
6178:
6157:
6153:
6146:
6141:
6139:
6137:
6134:
6133:
6109:
6108:
6087:
6083:
6062:
6058:
6057:
6052:
6037:
6033:
6012:
6008:
6007:
6002:
6000:
5998:
5995:
5994:
5968:
5967:
5942:
5937:
5912:
5907:
5905:
5903:
5900:
5899:
5875:
5874:
5849:
5844:
5819:
5814:
5812:
5810:
5807:
5806:
5780:
5779:
5754:
5749:
5736:
5731:
5729:
5727:
5724:
5723:
5699:
5698:
5673:
5668:
5655:
5650:
5648:
5646:
5643:
5642:
5605:
5574:
5569:
5549:
5533:
5528:
5526:
5524:
5521:
5520:
5497:
5466:
5461:
5441:
5425:
5420:
5418:
5416:
5413:
5412:
5387:
5356:
5351:
5331:
5315:
5310:
5308:
5306:
5303:
5302:
5279:
5248:
5243:
5223:
5207:
5202:
5200:
5198:
5195:
5194:
5169:
5141:
5136:
5117:
5112:
5110:
5108:
5105:
5104:
5081:
5053:
5048:
5029:
5024:
5022:
5020:
5017:
5016:
4991:
4960:
4955:
4930:
4925:
4923:
4921:
4918:
4917:
4894:
4851:
4846:
4811:
4806:
4804:
4802:
4799:
4798:
4773:
4742:
4737:
4702:
4697:
4695:
4693:
4690:
4689:
4666:
4635:
4630:
4595:
4590:
4588:
4586:
4583:
4582:
4559:
4555:
4550:
4519:
4514:
4495:
4490:
4488:
4486:
4483:
4482:
4461:
4457:
4452:
4421:
4416:
4397:
4392:
4390:
4388:
4385:
4384:
4361:
4357:
4352:
4321:
4316:
4297:
4292:
4290:
4288:
4285:
4284:
4263:
4259:
4254:
4223:
4218:
4199:
4194:
4192:
4190:
4187:
4186:
4145:
4144:
4113:
4108:
4073:
4068:
4066:
4064:
4061:
4060:
4023:
4018:
4013:
4008:
4006:
4004:
4001:
4000:
3950:
3947:
3946:
3927:
3924:
3923:
3904:
3901:
3900:
3881:
3878:
3877:
3858:
3855:
3854:
3835:
3832:
3831:
3812:
3809:
3808:
3784:
3773:
3770:
3769:
3753:
3750:
3749:
3733:
3730:
3729:
3713:
3710:
3709:
3693:
3690:
3689:
3673:
3670:
3669:
3653:
3650:
3649:
3633:
3630:
3629:
3607:
3596:
3593:
3592:
3574:
3571:
3570:
3554:
3551:
3550:
3527:
3524:
3523:
3507:
3504:
3503:
3485:
3482:
3481:
3457:
3454:
3453:
3426:
3423:
3422:
3395:
3392:
3391:
3363:
3360:
3359:
3341:
3338:
3337:
3321:
3318:
3317:
3287:
3284:
3283:
3277:
3275:Inference rules
3261:
3237:
3173:
3170:
3169:
3133:
3128:
3106:
3101:
3099:
3093:
3085:
3082:
3081:
3048:
3043:
3021:
3016:
3014:
3008:
3000:
2997:
2996:
2955:
2950:
2925:
2920:
2918:
2912:
2904:
2901:
2900:
2851:
2846:
2821:
2816:
2814:
2809:
2801:
2798:
2797:
2756:
2751:
2726:
2721:
2719:
2713:
2705:
2702:
2701:
2652:
2647:
2622:
2617:
2615:
2610:
2602:
2599:
2598:
2547:
2542:
2517:
2512:
2510:
2505:
2497:
2494:
2493:
2454:
2449:
2424:
2419:
2417:
2411:
2403:
2400:
2399:
2326:
2323:
2322:
2282:
2279:
2278:
2240:
2237:
2236:
2208:
2205:
2204:
2182:
2179:
2178:
2135:
2132:
2131:
2090:
2087:
2086:
2012:
2009:
2008:
1928:
1925:
1924:
1848:
1845:
1844:
1749:
1746:
1745:
1726:
1723:
1722:
1634:
1631:
1630:
1613:
1611:Reduction trees
1600:
1587:
1578:excluded middle
1573:
1531:
1527:
1509:
1505:
1493:
1489:
1477:
1473:
1458:
1454:
1445:
1441:
1430:
1427:
1426:
1398:
1394:
1379:
1375:
1366:
1362:
1353:
1349:
1331:
1327:
1315:
1311:
1303:
1300:
1299:
1263:
1259:
1244:
1240:
1225:
1221:
1206:
1202:
1194:
1191:
1190:
1167:
1163:
1148:
1144:
1135:
1131:
1116:
1112:
1110:
1107:
1106:
1085:
1081:
1079:
1076:
1075:
1055:
1051:
1049:
1046:
1045:
1020:
1017:
1016:
1000:
997:
996:
980:
977:
976:
960:
957:
956:
939:
935:
933:
930:
929:
912:
908:
906:
903:
902:
881:are called the
855:
851:
836:
832:
823:
819:
804:
800:
798:
795:
794:
788:
754:
750:
735:
731:
723:
720:
719:
690:
686:
671:
667:
665:
662:
661:
642:
639:
638:
621:
617:
615:
612:
611:
594:
590:
588:
585:
584:
564:
560:
558:
555:
554:
535:
532:
531:
515:
512:
511:
494:
490:
488:
485:
484:
468:
465:
464:
434:
431:
430:
414:
411:
410:
393:
389:
387:
384:
383:
357:
353:
338:
334:
325:
321:
319:
316:
315:
309:
303:
255:
252:
251:
232:
229:
228:
216:in the system,
208:
202:
190:Gentzen systems
126:
53:David Hilbert's
45:Gerhard Gentzen
17:
12:
11:
5:
13416:
13406:
13405:
13400:
13395:
13378:
13377:
13370:
13368:
13366:
13365:
13360:
13355:
13350:
13345:
13340:
13335:
13330:
13325:
13320:
13314:
13311:
13310:
13305:
13304:
13297:
13290:
13282:
13276:
13275:
13270:
13265:
13247:
13236:
13235:External links
13233:
13232:
13231:
13225:
13209:
13203:
13187:
13181:
13160:
13154:
13138:
13132:
13116:
13110:
13094:
13088:
13072:Hilbert, David
13068:
13062:
13042:
13024:(3): 405â431.
13006:
12988:(2): 176â210.
12968:
12962:
12946:
12940:
12920:
12917:
12914:
12913:
12900:
12876:intuitionistic
12840:
12828:
12816:
12803:
12790:
12768:
12740:
12723:
12721:, p. 441.
12711:
12699:
12687:
12666:
12650:
12638:
12636:, p. 180.
12605:
12566:
12557:
12537:
12521:
12509:
12497:
12485:
12473:
12461:
12446:
12431:
12411:
12410:
12408:
12405:
12404:
12403:
12398:
12393:
12388:
12381:
12378:
12374:
12373:
12362:
12354:
12351:
12348:
12345:
12342:
12339:
12336:
12333:
12330:
12318:
12315:
12312:
12309:
12305:
12301:
12298:
12295:
12292:
12289:
12258:
12247:
12246:
12230:
12227:
12224:
12221:
12218:
12215:
12212:
12209:
12206:
12194:
12191:
12188:
12185:
12182:
12179:
12176:
12145:
12142:
12138:
12134:
12114:
12111:
12107:
12103:
12083:
12080:
12076:
12072:
12052:
12048:
12027:
12024:
12021:
12018:
11998:
11995:
11991:
11987:
11969:
11968:
11957:
11954:
11950:
11946:
11937:
11934:
11931:
11928:
11925:
11922:
11919:
11907:
11904:
11901:
11898:
11895:
11891:
11888:
11885:
11882:
11879:
11848:
11845:
11841:
11837:
11821:
11818:
11794:Main article:
11791:
11788:
11775:
11772:
11769:
11766:
11763:
11759:
11755:
11752:
11749:
11746:
11726:
11715:
11714:
11698:
11695:
11692:
11689:
11686:
11655:
11654:
11637:
11634:
11586:
11574:
11571:
11563:
11562:
11551:
11543:
11540:
11537:
11534:
11531:
11528:
11525:
11522:
11519:
11516:
11513:
11501:
11498:
11495:
11492:
11489:
11485:
11482:
11479:
11476:
11473:
11442:
11439:
11435:
11431:
11408:
11405:
11402:
11399:
11396:
11393:
11390:
11364:
11361:
11356:
11353:
11329:
11326:
11323:
11312:if and only if
11300:
11297:
11294:
11291:
11288:
11269:
11245:
11225:
11222:
11209:also consider
11195:
11192:
11183:
11180:
11168:
11167:
11164:
11160:
11159:
11156:
11144:
11139:
11135:
11132:
11129:
11125:
11121:
11118:
11115:
11111:
11107:
11104:
11101:
11098:
11094:
11089:
11084:
11080:
11076:
11071:
11067:
11064:
11061:
11057:
11053:
11050:
11046:
11041:
11037:
11026:
11025:
11014:
11011:
11008:
11005:
10995:
10991:
10990:
10987:
10975:
10971:
10968:
10965:
10961:
10957:
10954:
10951:
10947:
10943:
10940:
10937:
10934:
10930:
10925:
10920:
10916:
10912:
10907:
10903:
10900:
10897:
10893:
10889:
10886:
10882:
10870:
10869:
10858:
10855:
10852:
10849:
10839:
10835:
10834:
10831:
10820:
10817:
10814:
10810:
10806:
10803:
10800:
10796:
10792:
10789:
10786:
10783:
10779:
10774:
10770:
10766:
10761:
10757:
10754:
10751:
10747:
10743:
10740:
10736:
10724:
10723:
10712:
10709:
10706:
10703:
10693:
10689:
10688:
10685:
10674:
10671:
10668:
10664:
10659:
10655:
10652:
10649:
10645:
10641:
10638:
10634:
10630:
10626:
10622:
10619:
10616:
10612:
10608:
10605:
10602:
10599:
10595:
10590:
10578:
10577:
10566:
10563:
10560:
10557:
10547:
10543:
10542:
10539:
10528:
10525:
10522:
10519:
10516:
10513:
10509:
10504:
10500:
10497:
10494:
10490:
10486:
10483:
10479:
10475:
10471:
10467:
10464:
10461:
10457:
10453:
10450:
10447:
10444:
10440:
10435:
10423:
10422:
10411:
10408:
10405:
10402:
10392:
10389:
10386:
10385:
10382:
10381:
10378:
10374:
10373:
10370:
10359:
10356:
10353:
10349:
10345:
10342:
10339:
10335:
10331:
10327:
10323:
10320:
10317:
10313:
10309:
10306:
10303:
10300:
10296:
10291:
10279:
10278:
10267:
10264:
10261:
10258:
10248:
10244:
10243:
10240:
10229:
10226:
10223:
10219:
10215:
10212:
10209:
10205:
10201:
10198:
10195:
10192:
10188:
10183:
10179:
10175:
10171:
10168:
10165:
10161:
10149:
10148:
10137:
10134:
10131:
10128:
10118:
10114:
10113:
10110:
10099:
10096:
10093:
10089:
10085:
10082:
10079:
10075:
10071:
10068:
10065:
10062:
10058:
10053:
10049:
10045:
10041:
10038:
10035:
10031:
10027:
10024:
10021:
10018:
10014:
10009:
10005:
10001:
9997:
9994:
9991:
9987:
9975:
9974:
9963:
9958:
9954:
9950:
9947:
9937:
9933:
9932:
9929:
9918:
9915:
9912:
9909:
9906:
9903:
9899:
9895:
9892:
9889:
9885:
9881:
9878:
9875:
9872:
9868:
9863:
9859:
9855:
9851:
9848:
9845:
9841:
9829:
9828:
9817:
9814:
9811:
9808:
9798:
9794:
9793:
9790:
9779:
9776:
9773:
9769:
9765:
9762:
9759:
9755:
9751:
9748:
9745:
9742:
9738:
9733:
9729:
9726:
9723:
9720:
9716:
9712:
9709:
9706:
9702:
9690:
9689:
9678:
9673:
9669:
9665:
9662:
9652:
9648:
9647:
9644:
9633:
9630:
9627:
9623:
9619:
9616:
9613:
9610:
9606:
9602:
9599:
9596:
9593:
9589:
9585:
9582:
9579:
9575:
9563:
9562:
9551:
9548:
9545:
9542:
9532:
9529:
9526:
9525:
9522:
9521:
9518:
9514:
9513:
9510:
9499:
9496:
9493:
9490:
9487:
9476:
9475:
9464:
9461:
9458:
9448:
9445:
9438:
9435:
9432:
9431:
9428:
9424:
9423:
9420:
9409:
9406:
9403:
9400:
9397:
9394:
9391:
9388:
9377:
9376:
9365:
9362:
9359:
9356:
9346:
9342:
9341:
9338:
9327:
9324:
9321:
9318:
9315:
9312:
9309:
9298:
9297:
9286:
9283:
9280:
9277:
9267:
9263:
9262:
9259:
9248:
9245:
9242:
9239:
9236:
9233:
9230:
9219:
9218:
9207:
9204:
9201:
9198:
9188:
9185:
9182:
9181:
9178:
9177:
9174:
9170:
9169:
9166:
9155:
9152:
9149:
9146:
9143:
9132:
9131:
9120:
9117:
9114:
9111:
9101:
9097:
9096:
9093:
9082:
9079:
9076:
9065:
9064:
9053:
9050:
9047:
9037:
9034:
9028:
9025:
9022:
9021:
9018:
9014:
9013:
9010:
8999:
8996:
8993:
8990:
8987:
8976:
8975:
8964:
8961:
8958:
8955:
8945:
8941:
8940:
8937:
8926:
8923:
8920:
8909:
8908:
8897:
8894:
8891:
8881:
8878:
8856:
8853:
8850:
8849:
8846:
8842:
8841:
8838:
8827:
8824:
8821:
8818:
8815:
8804:
8803:
8792:
8789:
8786:
8783:
8773:
8769:
8768:
8765:
8754:
8751:
8748:
8745:
8742:
8731:
8730:
8719:
8716:
8713:
8710:
8700:
8696:
8695:
8692:
8681:
8678:
8675:
8664:
8663:
8652:
8649:
8646:
8636:
8633:
8605:
8600:
8596:
8593:
8590:
8586:
8582:
8579:
8576:
8572:
8568:
8565:
8562:
8559:
8555:
8550:
8545:
8541:
8537:
8532:
8528:
8525:
8522:
8518:
8514:
8511:
8507:
8502:
8487:
8486:
8483:
8479:
8478:
8475:
8463:
8458:
8454:
8451:
8448:
8445:
8442:
8439:
8435:
8431:
8428:
8424:
8420:
8417:
8414:
8410:
8405:
8401:
8398:
8395:
8392:
8389:
8386:
8382:
8378:
8375:
8371:
8367:
8364:
8353:
8352:
8341:
8338:
8335:
8332:
8322:
8318:
8317:
8314:
8302:
8298:
8295:
8292:
8289:
8286:
8283:
8279:
8275:
8272:
8269:
8265:
8260:
8256:
8253:
8250:
8247:
8244:
8241:
8237:
8233:
8230:
8226:
8222:
8219:
8208:
8207:
8196:
8193:
8190:
8187:
8177:
8173:
8172:
8169:
8157:
8153:
8150:
8147:
8144:
8141:
8138:
8134:
8130:
8127:
8124:
8120:
8116:
8113:
8110:
8107:
8104:
8101:
8097:
8093:
8090:
8079:
8078:
8067:
8064:
8061:
8058:
8048:
8044:
8043:
8040:
8029:
8026:
8023:
8020:
8017:
8014:
8011:
8007:
8003:
8000:
7997:
7994:
7991:
7988:
7984:
7980:
7977:
7966:
7965:
7954:
7951:
7948:
7945:
7935:
7931:
7930:
7927:
7916:
7913:
7910:
7907:
7904:
7901:
7898:
7895:
7892:
7889:
7886:
7883:
7880:
7869:
7868:
7857:
7854:
7851:
7841:
7838:
7820:
7817:
7814:
7811:
7791:
7788:
7785:
7782:
7768:
7767:
7764:
7760:
7759:
7756:
7745:
7742:
7739:
7736:
7733:
7722:
7721:
7710:
7707:
7704:
7701:
7691:
7687:
7686:
7683:
7672:
7669:
7666:
7663:
7660:
7657:
7654:
7651:
7648:
7645:
7634:
7633:
7622:
7617:
7613:
7609:
7606:
7596:
7592:
7591:
7588:
7577:
7574:
7571:
7568:
7565:
7562:
7559:
7548:
7547:
7536:
7533:
7530:
7527:
7517:
7513:
7512:
7509:
7498:
7495:
7492:
7489:
7486:
7483:
7480:
7469:
7468:
7457:
7452:
7448:
7444:
7441:
7431:
7427:
7426:
7423:
7412:
7409:
7406:
7403:
7400:
7389:
7388:
7377:
7374:
7371:
7368:
7358:
7354:
7353:
7350:
7339:
7336:
7333:
7322:
7321:
7310:
7307:
7304:
7294:
7291:
7263:
7260:
7257:
7254:
7251:
7239:
7236:
7223:
7176:
7156:
7136:
7113:
7110:
7107:
7087:
7067:
7047:
7027:
7007:
6987:
6967:
6947:
6927:
6907:
6887:
6884:
6881:
6861:
6858:
6854:
6850:
6826:
6823:
6819:
6815:
6812:
6809:
6789:
6786:
6782:
6778:
6775:
6772:
6752:
6748:
6744:
6724:
6721:
6717:
6713:
6690:
6686:
6665:
6645:
6625:
6605:
6585:
6565:
6545:
6542:
6538:
6534:
6514:
6511:
6508:
6488:
6468:
6448:
6428:
6423:
6419:
6414:
6410:
6387:
6364:
6361:
6347:
6327:
6324:
6320:
6316:
6296:
6293:
6289:
6285:
6271:
6270:
6259:
6254:
6251:
6246:
6235:
6231:
6227:
6224:
6221:
6218:
6215:
6210:
6206:
6202:
6199:
6185:
6181:
6177:
6174:
6171:
6168:
6165:
6160:
6156:
6152:
6149:
6131:
6120:
6115:
6112:
6107:
6098:
6095:
6090:
6086:
6082:
6079:
6076:
6073:
6070:
6065:
6061:
6048:
6045:
6040:
6036:
6032:
6029:
6026:
6023:
6020:
6015:
6011:
5991:
5990:
5979:
5974:
5971:
5966:
5957:
5954:
5951:
5948:
5945:
5933:
5930:
5927:
5924:
5921:
5918:
5915:
5897:
5886:
5881:
5878:
5873:
5864:
5861:
5858:
5855:
5852:
5840:
5837:
5834:
5831:
5828:
5825:
5822:
5803:
5802:
5791:
5786:
5783:
5778:
5769:
5766:
5763:
5760:
5757:
5745:
5742:
5739:
5721:
5710:
5705:
5702:
5697:
5688:
5685:
5682:
5679:
5676:
5664:
5661:
5658:
5639:
5638:
5635:
5627:
5626:
5615:
5612:
5608:
5604:
5595:
5592:
5589:
5586:
5583:
5580:
5577:
5565:
5562:
5559:
5556:
5552:
5548:
5545:
5542:
5539:
5536:
5518:
5507:
5504:
5500:
5496:
5487:
5484:
5481:
5478:
5475:
5472:
5469:
5457:
5454:
5451:
5448:
5444:
5440:
5437:
5434:
5431:
5428:
5409:
5408:
5397:
5394:
5390:
5386:
5377:
5374:
5371:
5368:
5365:
5362:
5359:
5347:
5344:
5341:
5338:
5334:
5330:
5327:
5324:
5321:
5318:
5300:
5289:
5286:
5282:
5278:
5269:
5266:
5263:
5260:
5257:
5254:
5251:
5239:
5236:
5233:
5230:
5226:
5222:
5219:
5216:
5213:
5210:
5191:
5190:
5179:
5176:
5172:
5168:
5159:
5156:
5153:
5150:
5147:
5144:
5132:
5129:
5126:
5123:
5120:
5102:
5091:
5088:
5084:
5080:
5071:
5068:
5065:
5062:
5059:
5056:
5044:
5041:
5038:
5035:
5032:
5013:
5012:
5001:
4998:
4994:
4990:
4981:
4978:
4975:
4972:
4969:
4966:
4963:
4951:
4948:
4945:
4942:
4939:
4936:
4933:
4915:
4904:
4901:
4897:
4893:
4884:
4881:
4878:
4875:
4872:
4869:
4866:
4863:
4860:
4857:
4854:
4842:
4839:
4836:
4833:
4830:
4826:
4823:
4820:
4817:
4814:
4795:
4794:
4783:
4780:
4776:
4772:
4763:
4760:
4757:
4754:
4751:
4748:
4745:
4733:
4730:
4727:
4724:
4721:
4717:
4714:
4711:
4708:
4705:
4687:
4676:
4673:
4669:
4665:
4656:
4653:
4650:
4647:
4644:
4641:
4638:
4626:
4623:
4620:
4617:
4614:
4610:
4607:
4604:
4601:
4598:
4579:
4578:
4567:
4562:
4558:
4553:
4549:
4540:
4537:
4534:
4531:
4528:
4525:
4522:
4510:
4507:
4504:
4501:
4498:
4480:
4469:
4464:
4460:
4455:
4451:
4442:
4439:
4436:
4433:
4430:
4427:
4424:
4412:
4409:
4406:
4403:
4400:
4381:
4380:
4369:
4364:
4360:
4355:
4351:
4342:
4339:
4336:
4333:
4330:
4327:
4324:
4312:
4309:
4306:
4303:
4300:
4282:
4271:
4266:
4262:
4257:
4253:
4244:
4241:
4238:
4235:
4232:
4229:
4226:
4214:
4211:
4208:
4205:
4202:
4183:
4182:
4179:
4171:
4170:
4159:
4154:
4151:
4148:
4143:
4134:
4131:
4128:
4125:
4122:
4119:
4116:
4104:
4101:
4098:
4095:
4092:
4088:
4085:
4082:
4079:
4076:
4058:
4047:
4044:
4041:
4032:
4029:
4026:
3997:
3996:
3993:
3984:quantification
3979:
3978:
3973:, and 'P' for
3954:
3934:
3931:
3911:
3908:
3888:
3885:
3865:
3862:
3842:
3839:
3819:
3816:
3806:
3794:
3791:
3787:
3783:
3780:
3777:
3757:
3737:
3717:
3697:
3677:
3657:
3637:
3617:
3614:
3610:
3606:
3603:
3600:
3590:
3578:
3558:
3543:
3531:
3511:
3501:
3489:
3479:
3478:
3477:
3461:
3446:
3430:
3399:
3379:
3376:
3373:
3370:
3367:
3357:
3345:
3325:
3315:
3291:
3276:
3273:
3260:
3257:
3245:Hilbert system
3236:
3233:
3207:
3206:
3195:
3192:
3189:
3186:
3183:
3180:
3177:
3165:
3164:
3148:
3145:
3142:
3139:
3136:
3124:
3121:
3118:
3115:
3112:
3109:
3092:
3089:
3079:
3063:
3060:
3057:
3054:
3051:
3039:
3036:
3033:
3030:
3027:
3024:
3007:
3004:
2993:
2992:
2976:
2973:
2970:
2967:
2964:
2961:
2958:
2946:
2943:
2940:
2937:
2934:
2931:
2928:
2911:
2908:
2898:
2882:
2879:
2876:
2873:
2870:
2866:
2863:
2860:
2857:
2854:
2842:
2839:
2836:
2833:
2830:
2827:
2824:
2808:
2805:
2794:
2793:
2777:
2774:
2771:
2768:
2765:
2762:
2759:
2747:
2744:
2741:
2738:
2735:
2732:
2729:
2712:
2709:
2699:
2683:
2680:
2677:
2674:
2671:
2667:
2664:
2661:
2658:
2655:
2643:
2640:
2637:
2634:
2631:
2628:
2625:
2609:
2606:
2595:
2594:
2578:
2575:
2572:
2569:
2566:
2562:
2559:
2556:
2553:
2550:
2538:
2535:
2532:
2529:
2526:
2523:
2520:
2504:
2501:
2491:
2475:
2472:
2469:
2466:
2463:
2460:
2457:
2445:
2442:
2439:
2436:
2433:
2430:
2427:
2410:
2407:
2396:
2395:
2392:
2383:inference line
2368:reduction tree
2360:
2359:
2348:
2345:
2342:
2339:
2336:
2333:
2330:
2316:
2315:
2304:
2301:
2298:
2295:
2292:
2289:
2286:
2276:
2265:
2262:
2259:
2256:
2253:
2250:
2247:
2244:
2221:
2218:
2215:
2212:
2192:
2189:
2186:
2175:
2174:
2163:
2160:
2157:
2154:
2151:
2148:
2145:
2142:
2139:
2129:
2118:
2115:
2112:
2109:
2106:
2103:
2100:
2097:
2094:
2076:
2075:
2064:
2061:
2058:
2055:
2052:
2049:
2046:
2043:
2040:
2037:
2034:
2031:
2028:
2025:
2022:
2019:
2016:
1998:
1997:
1986:
1983:
1980:
1977:
1974:
1971:
1968:
1965:
1962:
1959:
1956:
1953:
1950:
1947:
1944:
1941:
1938:
1935:
1932:
1918:
1917:
1906:
1903:
1900:
1897:
1894:
1891:
1888:
1885:
1882:
1879:
1876:
1873:
1870:
1867:
1864:
1861:
1858:
1855:
1852:
1834:
1833:
1822:
1819:
1816:
1813:
1810:
1807:
1804:
1801:
1798:
1795:
1792:
1789:
1786:
1783:
1780:
1777:
1774:
1771:
1768:
1765:
1762:
1759:
1756:
1753:
1730:
1716:
1715:
1704:
1701:
1698:
1695:
1692:
1689:
1686:
1683:
1680:
1677:
1674:
1671:
1668:
1665:
1662:
1659:
1656:
1653:
1650:
1647:
1644:
1641:
1638:
1612:
1609:
1599:
1596:
1586:
1583:
1572:
1569:
1553:
1552:
1551:
1550:
1539:
1534:
1530:
1526:
1523:
1520:
1517:
1512:
1508:
1504:
1501:
1496:
1492:
1488:
1485:
1480:
1476:
1472:
1469:
1466:
1461:
1457:
1453:
1448:
1444:
1440:
1437:
1434:
1417:
1416:
1415:
1414:
1401:
1397:
1393:
1390:
1387:
1382:
1378:
1374:
1369:
1365:
1361:
1356:
1352:
1348:
1345:
1342:
1339:
1334:
1330:
1326:
1323:
1318:
1314:
1310:
1307:
1283:
1282:
1271:
1266:
1262:
1258:
1255:
1252:
1247:
1243:
1239:
1236:
1233:
1228:
1224:
1220:
1217:
1214:
1209:
1205:
1201:
1198:
1184:
1183:
1170:
1166:
1162:
1159:
1156:
1151:
1147:
1143:
1138:
1134:
1130:
1127:
1124:
1119:
1115:
1088:
1084:
1058:
1054:
1027:
1024:
1004:
984:
964:
942:
938:
915:
911:
875:
874:
863:
858:
854:
850:
847:
844:
839:
835:
831:
826:
822:
818:
815:
812:
807:
803:
787:
784:
780:
779:
768:
765:
762:
757:
753:
749:
746:
743:
738:
734:
730:
727:
713:
712:
701:
698:
693:
689:
685:
682:
679:
674:
670:
646:
624:
620:
597:
593:
567:
563:
542:
539:
519:
497:
493:
472:
444:
441:
438:
418:
396:
392:
380:
379:
368:
365:
360:
356:
352:
349:
346:
341:
337:
333:
328:
324:
305:Main article:
302:
299:
259:
248:
247:
236:
206:Hilbert system
204:Main article:
201:
198:
174:meta-theoretic
162:intuitionistic
138:formal systems
125:
122:
118:free variables
101:
100:
99:
98:
95:
86:
76:proof calculus
15:
9:
6:
4:
3:
2:
13415:
13404:
13401:
13399:
13396:
13394:
13391:
13390:
13388:
13374:
13364:
13361:
13359:
13356:
13354:
13351:
13349:
13346:
13344:
13341:
13339:
13336:
13334:
13331:
13329:
13326:
13324:
13321:
13319:
13316:
13315:
13312:
13303:
13298:
13296:
13291:
13289:
13284:
13283:
13280:
13274:
13271:
13269:
13266:
13262:
13258:
13257:
13252:
13248:
13246:
13242:
13239:
13238:
13228:
13222:
13218:
13214:
13210:
13206:
13200:
13196:
13192:
13188:
13184:
13178:
13174:
13170:
13166:
13165:Zach, Richard
13161:
13157:
13155:0-17-712040-1
13151:
13147:
13143:
13139:
13135:
13129:
13125:
13121:
13117:
13113:
13107:
13103:
13099:
13095:
13091:
13085:
13081:
13077:
13076:Bernays, Paul
13073:
13069:
13065:
13063:0-521-37181-3
13059:
13054:
13053:
13047:
13043:
13039:
13035:
13031:
13027:
13023:
13019:
13015:
13011:
13007:
13003:
12999:
12995:
12991:
12987:
12983:
12982:
12977:
12973:
12969:
12965:
12959:
12955:
12951:
12947:
12943:
12941:0-444-89840-9
12937:
12933:
12932:
12927:
12923:
12922:
12910:
12904:
12897:
12893:
12889:
12885:
12881:
12877:
12873:
12869:
12865:
12861:
12857:
12853:
12849:
12844:
12837:
12832:
12826:, p. 107
12825:
12824:Smullyan 1995
12820:
12813:
12807:
12800:
12794:
12786:
12779:
12772:
12766:
12762:
12761:Philip Wadler
12758:
12754:
12750:
12744:
12737:
12732:
12730:
12728:
12720:
12715:
12708:
12703:
12696:
12691:
12684:
12679:
12675:
12670:
12663:
12659:
12654:
12647:
12642:
12635:
12631:
12630:Smullyan 1995
12627:
12623:
12619:
12615:
12609:
12595:
12591:
12584:
12580:
12577:; Owre, Sam;
12576:
12570:
12561:
12554:
12550:
12546:
12541:
12534:
12530:
12525:
12518:
12513:
12506:
12505:Smullyan 1995
12501:
12494:
12489:
12482:
12477:
12470:
12465:
12458:
12453:
12451:
12443:
12438:
12436:
12428:
12424:
12419:
12417:
12412:
12402:
12399:
12397:
12394:
12392:
12389:
12387:
12384:
12383:
12377:
12360:
12352:
12349:
12343:
12340:
12331:
12316:
12313:
12307:
12303:
12299:
12293:
12290:
12272:
12271:
12270:
12256:
12228:
12225:
12219:
12213:
12207:
12192:
12189:
12186:
12183:
12180:
12177:
12159:
12158:
12157:
12140:
12109:
12078:
12050:
12022:
11993:
11976:
11974:
11952:
11948:
11935:
11932:
11929:
11926:
11923:
11920:
11905:
11902:
11899:
11896:
11889:
11886:
11883:
11880:
11862:
11861:
11860:
11843:
11839:
11827:
11817:
11815:
11811:
11807:
11803:
11797:
11787:
11764:
11750:
11693:
11687:
11660:
11659:
11658:
11635:
11608:
11607:
11606:
11604:
11601:representing
11600:
11570:
11568:
11549:
11538:
11532:
11529:
11526:
11523:
11520:
11514:
11496:
11493:
11490:
11480:
11477:
11474:
11456:
11455:
11454:
11437:
11433:
11420:
11403:
11400:
11397:
11394:
11391:
11380:
11375:
11373:
11368:
11360:
11352:
11350:
11346:
11341:
11327:
11324:
11313:
11295:
11292:
11259:
11243:
11235:
11231:
11221:
11219:
11214:
11212:
11208:
11203:
11199:
11191:
11189:
11179:
11176:
11165:
11162:
11161:
11157:
11142:
11137:
11133:
11123:
11119:
11113:
11109:
11105:
11096:
11092:
11087:
11082:
11074:
11069:
11065:
11062:
11059:
11055:
11048:
11044:
11039:
11035:
11027:
11009:
10993:
10992:
10988:
10973:
10969:
10959:
10955:
10949:
10945:
10941:
10932:
10928:
10923:
10918:
10914:
10910:
10905:
10901:
10898:
10895:
10891:
10884:
10880:
10871:
10853:
10837:
10836:
10832:
10818:
10812:
10808:
10804:
10798:
10794:
10790:
10781:
10777:
10772:
10768:
10764:
10759:
10755:
10752:
10749:
10745:
10738:
10734:
10725:
10707:
10704:
10691:
10690:
10686:
10672:
10666:
10662:
10657:
10653:
10650:
10647:
10643:
10636:
10632:
10628:
10624:
10620:
10614:
10610:
10606:
10597:
10593:
10588:
10579:
10561:
10558:
10545:
10544:
10540:
10526:
10520:
10517:
10511:
10507:
10502:
10498:
10495:
10492:
10488:
10481:
10477:
10473:
10469:
10465:
10459:
10455:
10451:
10442:
10438:
10433:
10424:
10406:
10390:
10379:
10376:
10375:
10371:
10357:
10351:
10347:
10343:
10340:
10337:
10333:
10329:
10325:
10321:
10315:
10311:
10307:
10298:
10294:
10289:
10280:
10262:
10259:
10246:
10245:
10241:
10227:
10221:
10217:
10213:
10207:
10203:
10199:
10190:
10186:
10181:
10177:
10173:
10169:
10166:
10163:
10159:
10150:
10132:
10129:
10116:
10115:
10111:
10097:
10091:
10087:
10083:
10077:
10073:
10069:
10060:
10056:
10051:
10047:
10043:
10039:
10033:
10029:
10025:
10016:
10012:
10007:
10003:
9999:
9995:
9992:
9989:
9985:
9976:
9956:
9952:
9948:
9935:
9934:
9930:
9916:
9910:
9907:
9901:
9897:
9893:
9887:
9883:
9879:
9870:
9866:
9861:
9857:
9853:
9849:
9846:
9843:
9839:
9830:
9812:
9809:
9796:
9795:
9791:
9777:
9771:
9767:
9763:
9757:
9753:
9749:
9740:
9736:
9731:
9727:
9724:
9718:
9714:
9710:
9707:
9704:
9700:
9691:
9671:
9667:
9663:
9650:
9649:
9645:
9631:
9625:
9621:
9617:
9608:
9604:
9600:
9597:
9591:
9587:
9583:
9580:
9577:
9573:
9564:
9546:
9530:
9519:
9516:
9515:
9511:
9497:
9491:
9488:
9477:
9459:
9446:
9443:
9442:
9437:
9436:
9429:
9426:
9425:
9421:
9407:
9404:
9401:
9395:
9392:
9389:
9386:
9378:
9360:
9344:
9343:
9339:
9325:
9322:
9319:
9316:
9313:
9310:
9307:
9299:
9281:
9278:
9265:
9264:
9260:
9246:
9243:
9240:
9237:
9234:
9231:
9228:
9220:
9202:
9199:
9186:
9175:
9172:
9171:
9167:
9153:
9150:
9147:
9144:
9141:
9133:
9115:
9112:
9099:
9098:
9094:
9080:
9077:
9074:
9066:
9048:
9035:
9033:
9032:
9027:
9026:
9019:
9016:
9015:
9011:
8997:
8994:
8991:
8988:
8985:
8977:
8959:
8956:
8943:
8942:
8938:
8924:
8921:
8918:
8910:
8892:
8879:
8877:
8876:
8872:
8869:
8868:
8864:
8861:
8860:
8855:
8854:
8847:
8844:
8843:
8839:
8825:
8819:
8816:
8813:
8805:
8787:
8784:
8771:
8770:
8766:
8752:
8749:
8746:
8740:
8732:
8714:
8698:
8697:
8693:
8679:
8676:
8673:
8665:
8647:
8634:
8631:
8630:
8626:
8623:
8622:
8619:
8603:
8598:
8594:
8584:
8580:
8574:
8570:
8566:
8557:
8553:
8548:
8543:
8535:
8530:
8526:
8523:
8520:
8516:
8509:
8505:
8500:
8484:
8481:
8480:
8476:
8461:
8456:
8449:
8446:
8443:
8437:
8433:
8429:
8422:
8418:
8412:
8408:
8403:
8396:
8393:
8390:
8384:
8380:
8376:
8369:
8365:
8354:
8336:
8320:
8319:
8315:
8300:
8293:
8290:
8287:
8281:
8277:
8273:
8267:
8263:
8258:
8251:
8248:
8245:
8239:
8235:
8231:
8224:
8220:
8209:
8191:
8175:
8174:
8170:
8155:
8148:
8145:
8142:
8136:
8132:
8128:
8122:
8118:
8111:
8108:
8105:
8099:
8095:
8091:
8080:
8062:
8046:
8045:
8041:
8024:
8021:
8018:
8012:
8009:
8005:
7998:
7995:
7992:
7986:
7982:
7978:
7967:
7949:
7933:
7932:
7928:
7911:
7908:
7905:
7899:
7896:
7890:
7887:
7884:
7878:
7870:
7852:
7839:
7836:
7835:
7832:
7815:
7786:
7765:
7762:
7761:
7757:
7743:
7737:
7734:
7731:
7723:
7705:
7702:
7689:
7688:
7684:
7670:
7664:
7661:
7658:
7655:
7649:
7646:
7643:
7635:
7615:
7611:
7607:
7594:
7593:
7589:
7575:
7569:
7566:
7563:
7560:
7557:
7549:
7531:
7528:
7515:
7514:
7510:
7496:
7493:
7490:
7484:
7481:
7478:
7470:
7450:
7446:
7442:
7429:
7428:
7424:
7410:
7407:
7404:
7398:
7390:
7372:
7356:
7355:
7351:
7337:
7334:
7331:
7323:
7305:
7292:
7289:
7288:
7285:
7283:
7279:
7278:
7261:
7255:
7252:
7249:
7235:
7221:
7212:
7210:
7206:
7200:
7198:
7194:
7190:
7174:
7154:
7134:
7125:
7111:
7108:
7105:
7085:
7065:
6985:
6945:
6885:
6882:
6879:
6856:
6852:
6838:
6821:
6817:
6813:
6807:
6784:
6780:
6776:
6770:
6750:
6746:
6719:
6702:
6688:
6663:
6583:
6540:
6512:
6509:
6506:
6466:
6421:
6417:
6412:
6399:
6385:
6378:
6374:
6370:
6360:
6359:
6345:
6322:
6291:
6233:
6225:
6222:
6219:
6216:
6213:
6208:
6200:
6183:
6175:
6172:
6169:
6166:
6163:
6158:
6150:
6132:
6093:
6088:
6080:
6077:
6074:
6071:
6068:
6063:
6043:
6038:
6030:
6027:
6024:
6021:
6018:
6013:
5993:
5992:
5952:
5949:
5946:
5928:
5925:
5922:
5919:
5916:
5898:
5859:
5856:
5853:
5835:
5832:
5829:
5826:
5823:
5805:
5804:
5764:
5761:
5758:
5740:
5722:
5683:
5680:
5677:
5659:
5641:
5640:
5636:
5633:
5632:
5610:
5590:
5587:
5584:
5578:
5560:
5554:
5550:
5546:
5540:
5537:
5519:
5502:
5482:
5479:
5476:
5470:
5452:
5446:
5442:
5438:
5432:
5429:
5411:
5410:
5392:
5372:
5369:
5366:
5360:
5342:
5336:
5332:
5328:
5322:
5319:
5301:
5284:
5264:
5261:
5258:
5252:
5234:
5228:
5224:
5220:
5214:
5211:
5193:
5192:
5174:
5154:
5151:
5145:
5127:
5124:
5121:
5103:
5086:
5066:
5063:
5057:
5039:
5036:
5033:
5015:
5014:
4996:
4976:
4973:
4967:
4964:
4946:
4943:
4940:
4937:
4934:
4916:
4899:
4879:
4873:
4870:
4864:
4861:
4855:
4837:
4834:
4831:
4821:
4818:
4815:
4797:
4796:
4778:
4774:
4758:
4755:
4752:
4749:
4746:
4728:
4725:
4722:
4712:
4709:
4706:
4688:
4671:
4667:
4651:
4648:
4645:
4642:
4639:
4621:
4618:
4615:
4605:
4602:
4599:
4581:
4580:
4560:
4556:
4551:
4535:
4532:
4529:
4526:
4523:
4505:
4502:
4499:
4481:
4462:
4458:
4453:
4437:
4434:
4431:
4428:
4425:
4407:
4404:
4401:
4383:
4382:
4362:
4358:
4353:
4337:
4334:
4331:
4328:
4325:
4307:
4304:
4301:
4283:
4264:
4260:
4255:
4239:
4236:
4233:
4230:
4227:
4209:
4206:
4203:
4185:
4184:
4180:
4177:
4176:
4129:
4123:
4117:
4099:
4093:
4090:
4086:
4083:
4077:
4059:
4042:
4030:
4027:
4024:
3999:
3998:
3994:
3991:
3990:
3987:
3985:
3976:
3972:
3968:
3952:
3932:
3929:
3909:
3906:
3886:
3883:
3863:
3860:
3840:
3837:
3817:
3814:
3807:
3789:
3785:
3781:
3775:
3755:
3735:
3715:
3695:
3675:
3655:
3635:
3612:
3608:
3604:
3598:
3591:
3548:
3544:
3529:
3509:
3502:
3487:
3480:
3475:
3474:disjunctively
3459:
3451:
3448:while on the
3447:
3444:
3443:conjunctively
3428:
3420:
3416:
3415:
3413:
3374:
3368:
3358:
3343:
3323:
3316:
3313:
3309:
3305:
3302:known as the
3289:
3282:
3281:
3280:
3272:
3270:
3266:
3259:The system LK
3256:
3254:
3250:
3246:
3242:
3232:
3230:
3226:
3220:
3217:
3215:
3193:
3190:
3184:
3181:
3178:
3166:
3143:
3140:
3137:
3122:
3116:
3110:
3087:
3080:
3061:
3058:
3052:
3034:
3031:
3025:
3002:
2995:
2994:
2974:
2971:
2965:
2962:
2959:
2944:
2938:
2935:
2929:
2906:
2899:
2877:
2874:
2871:
2864:
2861:
2855:
2837:
2834:
2828:
2825:
2803:
2796:
2795:
2775:
2772:
2769:
2766:
2760:
2745:
2742:
2739:
2736:
2730:
2710:
2707:
2700:
2678:
2675:
2672:
2662:
2659:
2656:
2638:
2635:
2632:
2629:
2626:
2607:
2604:
2597:
2596:
2576:
2573:
2567:
2560:
2557:
2551:
2536:
2533:
2530:
2527:
2521:
2502:
2499:
2492:
2470:
2467:
2464:
2461:
2458:
2440:
2437:
2434:
2431:
2428:
2408:
2405:
2398:
2397:
2393:
2390:
2389:
2386:
2384:
2379:
2375:
2371:
2369:
2365:
2346:
2343:
2340:
2337:
2334:
2331:
2328:
2321:
2320:
2319:
2302:
2299:
2296:
2293:
2290:
2287:
2284:
2277:
2263:
2260:
2257:
2254:
2251:
2248:
2245:
2235:
2234:
2233:
2219:
2216:
2213:
2190:
2184:
2161:
2158:
2155:
2152:
2149:
2146:
2143:
2137:
2130:
2116:
2113:
2110:
2107:
2104:
2101:
2098:
2092:
2085:
2084:
2083:
2081:
2062:
2059:
2056:
2053:
2050:
2047:
2041:
2035:
2029:
2023:
2017:
2007:
2006:
2005:
2003:
1984:
1981:
1975:
1972:
1969:
1963:
1957:
1951:
1945:
1939:
1933:
1923:
1922:
1921:
1904:
1895:
1892:
1889:
1883:
1877:
1871:
1865:
1859:
1853:
1843:
1842:
1841:
1839:
1817:
1808:
1805:
1802:
1784:
1778:
1772:
1766:
1760:
1751:
1744:
1743:
1742:
1728:
1721:
1699:
1690:
1687:
1684:
1666:
1660:
1654:
1648:
1642:
1629:
1628:
1627:
1624:
1622:
1618:
1604:
1595:
1592:
1582:
1579:
1568:
1564:
1562:
1556:
1532:
1528:
1521:
1518:
1515:
1510:
1506:
1499:
1494:
1490:
1483:
1478:
1474:
1470:
1467:
1464:
1459:
1455:
1451:
1446:
1442:
1432:
1425:
1424:
1422:
1421:
1420:
1399:
1395:
1391:
1388:
1385:
1380:
1376:
1372:
1367:
1363:
1359:
1354:
1350:
1343:
1340:
1337:
1332:
1328:
1321:
1316:
1312:
1305:
1298:
1297:
1296:
1295:
1294:
1292:
1286:
1264:
1260:
1256:
1253:
1250:
1245:
1241:
1226:
1222:
1218:
1215:
1212:
1207:
1203:
1196:
1189:
1188:
1187:
1168:
1164:
1160:
1157:
1154:
1149:
1145:
1141:
1136:
1132:
1128:
1125:
1122:
1117:
1113:
1105:
1104:
1103:
1086:
1082:
1074:
1056:
1052:
1044:
1039:
1025:
1022:
1002:
982:
962:
940:
936:
913:
909:
900:
896:
892:
888:
884:
880:
861:
856:
852:
848:
845:
842:
837:
833:
829:
824:
820:
816:
813:
810:
805:
801:
793:
792:
791:
783:
766:
755:
751:
747:
744:
741:
736:
732:
725:
718:
717:
716:
699:
696:
691:
687:
683:
680:
677:
672:
668:
660:
659:
658:
644:
622:
618:
595:
591:
581:
565:
561:
540:
537:
517:
495:
491:
470:
462:
458:
442:
439:
436:
416:
394:
390:
366:
363:
358:
354:
350:
347:
344:
339:
335:
331:
326:
322:
314:
313:
312:
308:
298:
296:
292:
287:
285:
281:
277:
273:
257:
234:
227:
226:
225:
223:
219:
215:
214:
207:
197:
195:
191:
187:
183:
179:
175:
171:
167:
163:
159:
155:
151:
147:
143:
139:
135:
131:
121:
119:
115:
111:
105:
96:
93:
90:
89:
87:
84:
83:Hilbert style
81:
80:
79:
77:
72:
70:
66:
62:
58:
54:
50:
46:
42:
38:
34:
30:
29:argumentation
26:
22:
13393:Proof theory
13357:
13333:Karnaugh map
13318:Venn diagram
13254:
13216:
13194:
13168:
13145:
13123:
13101:
13079:
13051:
13021:
13017:
12985:
12979:
12953:
12930:
12908:
12903:
12895:
12891:
12887:
12883:
12879:
12875:
12871:
12867:
12863:
12859:
12855:
12851:
12848:Gentzen 1934
12843:
12831:
12819:
12806:
12798:
12793:
12784:
12771:
12743:
12714:
12707:Gentzen 1934
12702:
12695:Gentzen 1934
12690:
12682:
12677:
12674:Gentzen 1934
12669:
12661:
12658:Gentzen 1934
12653:
12648:, p. 10
12641:
12634:Gentzen 1934
12608:
12597:. Retrieved
12589:
12569:
12560:
12540:
12524:
12512:
12500:
12488:
12476:
12464:
12427:Gentzen 1935
12423:Gentzen 1934
12401:Proof theory
12375:
12248:
11977:
11970:
11823:
11805:
11799:
11716:
11656:
11602:
11576:
11567:linear logic
11564:
11421:
11376:
11369:
11366:
11358:
11348:
11342:
11314:the sequent
11258:semantically
11227:
11215:
11204:
11200:
11197:
11185:
11171:
8490:
7771:
7281:
7275:
7241:
7213:
7201:
7196:
7126:
6839:
6703:
6616:, then from
6400:
6372:
6368:
6366:
6275:
6274:
3980:
3974:
3970:
3966:
3473:
3449:
3442:
3418:
3417:when on the
3314:on the right
3312:propositions
3311:
3307:
3278:
3264:
3262:
3253:modus ponens
3238:
3221:
3218:
3213:
3210:
2382:
2380:
2376:
2372:
2367:
2361:
2317:
2176:
2077:
1999:
1919:
1835:
1717:
1625:
1614:
1588:
1574:
1565:
1557:
1554:
1418:
1287:
1284:
1185:
1073:at least one
1072:
1042:
1040:
898:
894:
890:
886:
882:
876:
789:
781:
714:
582:
456:
381:
310:
288:
275:
249:
217:
211:
209:
189:
165:
145:
141:
130:proof theory
127:
106:
102:
73:
57:formal logic
24:
18:
13353:Truth table
12856:klassischer
12836:Kleene 2002
12753:implication
12719:Kleene 2002
12622:Kleene 2009
12618:Kleene 2002
12553:Suppes 1999
12545:Lemmon 1965
12529:Suppes 1999
12493:Kleene 2002
12481:Kleene 2009
12457:Kleene 2009
7284:in Latin).
3986:are added.
3975:Permutation
3971:Contraction
3668:in formula
3308:assumptions
3249:shown below
3095:rule:
3010:rule:
2914:rule:
2811:rule:
2715:rule:
2612:rule:
2507:rule:
2413:rule:
2378:arguments.
2364:rooted tree
2080:disjunction
2002:conjunction
1838:implication
284:modal logic
178:consistency
110:quantifiers
13387:Categories
12919:References
12757:hypothesis
12614:Curry 1977
12599:2015-05-29
12590:User guide
12517:Curry 1977
12469:Curry 1977
12442:Curry 1977
12249:and (when
11379:admissible
6373:structural
3982:regarding
3969:, 'C' for
3214:decomposed
891:consequent
883:antecedent
530:such that
382:where the
39:(called a
13261:EMS Press
13215:(1999) .
13193:(1995) .
13122:(2002) .
13100:(2009) .
13078:(1970) .
13038:186239837
13002:121546341
12952:(1977) .
12880:classical
12646:Buss 1998
12551:based on
12350:∨
12338:∀
12332:⊢
12329:Γ
12314:∨
12291:⊢
12288:Γ
12226:∨
12217:→
12208:⊢
12205:Γ
12190:∨
12184:⊢
12175:Γ
12137:∀
12106:→
12075:∀
12047:→
12020:¬
11990:→
11949:∨
11933:⊢
11927:∨
11918:Γ
11903:⊢
11894:Γ
11887:⊢
11878:Γ
11840:∨
11771:⊥
11768:→
11758:⟺
11748:¬
11725:⊥
11697:Δ
11694:⊢
11691:⊥
11685:Γ
11636:⊢
11633:⊥
11585:⊥
11573:Absurdity
11542:Π
11536:Δ
11533:⊢
11527:∨
11518:Σ
11512:Γ
11500:Π
11497:⊢
11488:Σ
11484:Δ
11481:⊢
11472:Γ
11434:∨
11407:Δ
11398:⊢
11389:Γ
11372:multisets
11349:Hauptsatz
11325:⊢
11322:Γ
11293:⊨
11290:Γ
11268:Γ
11207:sequences
11175:multisets
11131:¬
11128:→
11117:¬
11114:∧
11103:¬
11100:→
11079:→
11063:∨
11052:→
11036:⊢
11007:→
10967:¬
10964:→
10953:¬
10950:∧
10939:¬
10936:→
10915:⊢
10899:∨
10888:→
10851:→
10816:¬
10813:⊢
10802:¬
10799:∧
10788:¬
10785:→
10753:∨
10742:→
10670:¬
10667:⊢
10651:∨
10640:→
10618:¬
10615:∧
10604:¬
10601:→
10524:¬
10515:¬
10512:⊢
10496:∨
10485:→
10463:¬
10460:∧
10449:¬
10446:→
10404:→
10355:¬
10352:⊢
10341:∨
10319:¬
10316:∧
10305:¬
10302:→
10225:¬
10222:⊢
10211:¬
10208:∧
10197:¬
10194:→
10167:∨
10095:¬
10092:⊢
10081:¬
10078:∧
10067:¬
10064:→
10037:¬
10034:∧
10023:¬
10020:→
9993:∨
9949:∧
9914:¬
9911:⊢
9905:¬
9891:¬
9888:∧
9877:¬
9874:→
9847:∨
9775:¬
9772:⊢
9761:¬
9758:∧
9747:¬
9744:→
9722:¬
9708:∨
9664:∧
9629:¬
9626:⊢
9615:¬
9612:→
9595:¬
9581:∨
9544:→
9495:¬
9492:⊢
9486:¬
9405:⊢
9399:¬
9390:∨
9358:¬
9317:⊢
9311:∨
9238:⊢
9232:∨
9200:∨
9145:⊢
9078:⊢
8989:⊢
8922:⊢
8823:¬
8814:⊢
8744:¬
8741:⊢
8712:¬
8677:⊢
8592:¬
8589:→
8578:¬
8575:∧
8564:¬
8561:→
8540:→
8524:∨
8513:→
8427:∃
8416:∀
8413:⊢
8374:∀
8363:∃
8334:∀
8271:∃
8268:⊢
8229:∀
8218:∃
8189:∃
8126:∃
8123:⊢
8089:∀
8060:∃
8010:⊢
7976:∀
7947:∀
7897:⊢
7813:∃
7784:∀
7741:¬
7738:∨
7732:⊢
7668:¬
7665:∨
7653:¬
7650:∨
7644:⊢
7608:∨
7573:¬
7570:∨
7558:⊢
7488:¬
7485:∨
7479:⊢
7443:∨
7402:¬
7399:⊢
7370:¬
7335:⊢
7259:¬
7256:∨
7250:⊢
7109:∧
7046:Σ
7026:Γ
7006:Σ
6966:Γ
6926:Σ
6906:Γ
6883:∧
6853:∧
6743:∀
6716:∀
6685:¬
6644:Δ
6624:Γ
6604:Δ
6564:Γ
6537:¬
6510:∧
6487:Δ
6447:Δ
6413:∧
6386:⊢
6377:turnstile
6319:∃
6288:∀
6230:Δ
6205:Δ
6201:⊢
6198:Γ
6180:Δ
6155:Δ
6151:⊢
6148:Γ
6097:Δ
6094:⊢
6085:Γ
6060:Γ
6047:Δ
6044:⊢
6035:Γ
6010:Γ
5956:Δ
5947:⊢
5944:Γ
5932:Δ
5917:⊢
5914:Γ
5863:Δ
5860:⊢
5851:Γ
5839:Δ
5836:⊢
5821:Γ
5768:Δ
5759:⊢
5756:Γ
5744:Δ
5741:⊢
5738:Γ
5687:Δ
5684:⊢
5675:Γ
5663:Δ
5660:⊢
5657:Γ
5607:∃
5594:Δ
5582:∃
5579:⊢
5576:Γ
5564:Δ
5538:⊢
5535:Γ
5499:∃
5486:Δ
5483:⊢
5474:∃
5468:Γ
5456:Δ
5453:⊢
5427:Γ
5389:∀
5376:Δ
5364:∀
5361:⊢
5358:Γ
5346:Δ
5320:⊢
5317:Γ
5281:∀
5268:Δ
5265:⊢
5256:∀
5250:Γ
5238:Δ
5235:⊢
5209:Γ
5171:¬
5158:Δ
5149:¬
5146:⊢
5143:Γ
5131:Δ
5128:⊢
5119:Γ
5083:¬
5070:Δ
5067:⊢
5061:¬
5055:Γ
5043:Δ
5034:⊢
5031:Γ
4993:→
4980:Δ
4971:→
4965:⊢
4962:Γ
4950:Δ
4941:⊢
4932:Γ
4896:→
4883:Π
4877:Δ
4874:⊢
4868:→
4859:Σ
4853:Γ
4841:Π
4838:⊢
4829:Σ
4825:Δ
4816:⊢
4813:Γ
4775:∧
4762:Δ
4753:∧
4747:⊢
4744:Γ
4732:Δ
4723:⊢
4720:Γ
4716:Δ
4707:⊢
4704:Γ
4668:∨
4655:Δ
4652:⊢
4646:∨
4637:Γ
4625:Δ
4622:⊢
4613:Γ
4609:Δ
4606:⊢
4597:Γ
4552:∨
4539:Δ
4530:∨
4524:⊢
4521:Γ
4509:Δ
4500:⊢
4497:Γ
4454:∧
4441:Δ
4438:⊢
4432:∧
4423:Γ
4411:Δ
4408:⊢
4399:Γ
4354:∨
4341:Δ
4332:∨
4326:⊢
4323:Γ
4311:Δ
4302:⊢
4299:Γ
4256:∧
4243:Δ
4240:⊢
4234:∧
4225:Γ
4213:Δ
4210:⊢
4201:Γ
4133:Π
4127:Δ
4124:⊢
4121:Σ
4115:Γ
4103:Π
4100:⊢
4097:Σ
4081:Δ
4078:⊢
4075:Γ
4028:⊢
3953:⊢
3577:∃
3557:∀
3460:⊢
3429:⊢
3398:Π
3378:Σ
3372:Δ
3366:Γ
3304:turnstile
3290:⊢
3188:Δ
3185:⊢
3176:Γ
3147:Δ
3144:⊢
3135:Γ
3120:¬
3114:Δ
3111:⊢
3108:Γ
3091:¬
3056:Δ
3053:⊢
3050:Γ
3038:Δ
3035:⊢
3029:¬
3023:Γ
3006:¬
2969:Δ
2966:⊢
2957:Γ
2942:→
2933:Δ
2930:⊢
2927:Γ
2910:→
2881:Δ
2878:⊢
2869:Γ
2859:Δ
2856:⊢
2853:Γ
2841:Δ
2838:⊢
2832:→
2823:Γ
2807:→
2764:Δ
2761:⊢
2758:Γ
2743:∨
2734:Δ
2731:⊢
2728:Γ
2711:∨
2682:Δ
2679:⊢
2670:Γ
2666:Δ
2663:⊢
2654:Γ
2642:Δ
2639:⊢
2633:∨
2624:Γ
2608:∨
2571:Δ
2568:⊢
2565:Γ
2555:Δ
2552:⊢
2549:Γ
2534:∧
2525:Δ
2522:⊢
2519:Γ
2503:∧
2474:Δ
2471:⊢
2456:Γ
2444:Δ
2441:⊢
2435:∧
2426:Γ
2409:∧
2338:⊢
2300:⊢
2261:⊢
2243:¬
2217:∨
2211:¬
2188:→
2159:⊢
2141:→
2114:⊢
2096:→
2060:⊢
2039:→
2030:∨
2021:→
1982:⊢
1973:∧
1955:→
1946:∨
1937:→
1902:→
1893:∧
1884:⊢
1875:→
1866:∨
1857:→
1815:→
1806:∧
1794:→
1782:→
1773:∨
1764:→
1752:⊢
1729:⊢
1697:→
1688:∧
1676:→
1664:→
1655:∨
1646:→
1525:¬
1522:∧
1519:⋯
1516:∧
1503:¬
1500:∧
1487:¬
1484:∧
1471:∧
1468:⋯
1465:∧
1452:∧
1436:¬
1433:⊢
1392:∨
1389:⋯
1386:∨
1373:∨
1360:∨
1347:¬
1344:∨
1341:⋯
1338:∨
1325:¬
1322:∨
1309:¬
1306:⊢
1257:∨
1254:⋯
1251:∨
1235:→
1219:∧
1216:⋯
1213:∧
1197:⊢
1158:…
1142:⊢
1126:…
1071:is true,
1023:⊢
901:. Again,
887:succedent
879:turnstile
846:…
830:⊢
814:…
764:→
748:∧
745:⋯
742:∧
726:⊢
697:⊢
681:…
538:⊢
471:⊢
461:turnstile
440:≥
364:⊢
348:…
213:judgments
166:Hauptsatz
158:classical
49:inference
37:tautology
13167:(2021).
13144:(1965).
13012:(1935).
12974:(1934).
12549:System L
12533:System L
12380:See also
11355:Variants
11256:follows
11234:complete
7222:↚
7197:cut-free
3229:complete
3168:Axiom:
899:sequents
463:symbol "
124:Overview
65:theorems
13263:, 2001
13243:in the
12156:become
11166:
11163:
11158:
10994:
10989:
10838:
10833:
10692:
10687:
10546:
10541:
10391:
10380:
10377:
10372:
10247:
10242:
10117:
10112:
9936:
9931:
9797:
9792:
9651:
9646:
9531:
9520:
9517:
9512:
9447:
9444:
9430:
9427:
9422:
9345:
9340:
9266:
9261:
9187:
9176:
9173:
9168:
9100:
9095:
9036:
9020:
9017:
9012:
8944:
8939:
8880:
8848:
8845:
8840:
8772:
8767:
8699:
8694:
8635:
8632:
8485:
8482:
8477:
8321:
8316:
8176:
8171:
8047:
8042:
7934:
7929:
7840:
7837:
7766:
7763:
7758:
7690:
7685:
7595:
7590:
7516:
7511:
7430:
7425:
7357:
7352:
7293:
7290:
7199:proof.
6369:logical
3452:of the
3421:of the
3271:below.
895:cedents
409:'s and
272:formula
270:is any
41:sequent
13223:
13201:
13179:
13152:
13130:
13108:
13086:
13060:
13036:
13000:
12960:
12938:
11597:, the
3992:Axiom
3390:, and
2394:Right
1591:Kleene
1423:or as
1015:where
250:where
61:axioms
13034:S2CID
12998:S2CID
12781:(PDF)
12749:prove
12586:(PDF)
12407:Notes
11717:With
11603:false
11230:sound
3450:right
3269:rules
3225:sound
2391:Left
1043:every
282:or a
67:in a
33:proof
13221:ISBN
13199:ISBN
13177:ISBN
13150:ISBN
13128:ISBN
13106:ISBN
13084:ISBN
13058:ISBN
12958:ISBN
12936:ISBN
12894:and
12886:and
12878:and
12870:und
12862:und
12854:und
12125:and
11812:and
11806:i.e.
11232:and
11211:sets
7802:and
7078:and
7038:and
6978:and
6918:and
6576:and
6371:and
6307:and
3995:Cut
3547:free
3522:and
3419:left
3336:and
3227:and
1186:and
975:and
928:and
715:and
457:list
276:e.g.
218:i.e.
160:and
156:(in
144:and
132:and
13026:doi
12990:doi
12759:."â
12751:an
6656:or
3728:in
3569:or
2203:as
897:or
889:or
152:in
128:In
43:by
19:In
13389::
13259:,
13253:,
13171:.
13074:;
13032:.
13022:39
13020:.
13016:.
12996:.
12986:39
12984:.
12978:.
12896:NK
12892:NJ
12888:LK
12884:LJ
12872:NK
12868:NJ
12864:LK
12860:LJ
12763:,
12726:^
12683:LK
12678:NK
12662:NJ
12592:.
12588:.
12449:^
12434:^
12425:,
12415:^
12009:,
11975:.
11816:.
11786:.
11220:.
11213:.
11190:.
7831:.
7124:.
3922:,
3899:,
3876:,
3853:,
3830:,
3805:).
3265:LK
3216:.
2385:.
2370:.
1741::
610:,
297:.
196:.
146:LJ
142:LK
23:,
13301:e
13294:t
13287:v
13229:.
13207:.
13185:.
13158:.
13136:.
13114:.
13092:.
13066:.
13040:.
13028::
13004:.
12992::
12966:.
12944:.
12602:.
12535:.
12429:.
12361:.
12353:C
12347:)
12344:A
12341:x
12335:(
12317:C
12311:]
12308:x
12304:/
12300:y
12297:[
12294:A
12257:y
12229:C
12223:)
12220:B
12214:A
12211:(
12193:C
12187:B
12181:A
12178:,
12144:)
12141:R
12133:(
12113:)
12110:R
12102:(
12082:)
12079:R
12071:(
12051:R
12026:)
12023:R
12017:(
11997:)
11994:R
11986:(
11956:)
11953:L
11945:(
11936:C
11930:B
11924:A
11921:,
11906:C
11900:B
11897:,
11890:C
11884:A
11881:,
11847:)
11844:L
11836:(
11774:)
11765:A
11762:(
11754:)
11751:A
11745:(
11688:,
11550:.
11539:,
11530:B
11524:A
11521:,
11515:,
11494:B
11491:,
11478:A
11475:,
11441:)
11438:L
11430:(
11404:,
11401:A
11395:A
11392:,
11328:A
11299:)
11296:A
11287:(
11244:A
11143:)
11138:)
11134:A
11124:)
11120:C
11110:)
11106:A
11097:B
11093:(
11088:(
11083:(
11075:)
11070:)
11066:C
11060:B
11056:(
11049:A
11045:(
11040:(
11013:)
11010:R
11004:(
10974:)
10970:A
10960:)
10956:C
10946:)
10942:A
10933:B
10929:(
10924:(
10919:(
10911:)
10906:)
10902:C
10896:B
10892:(
10885:A
10881:(
10857:)
10854:R
10848:(
10819:A
10809:)
10805:C
10795:)
10791:A
10782:B
10778:(
10773:(
10769:,
10765:)
10760:)
10756:C
10750:B
10746:(
10739:A
10735:(
10711:)
10708:L
10705:P
10702:(
10673:A
10663:)
10658:)
10654:C
10648:B
10644:(
10637:A
10633:(
10629:,
10625:)
10621:C
10611:)
10607:A
10598:B
10594:(
10589:(
10565:)
10562:R
10559:C
10556:(
10527:A
10521:,
10518:A
10508:)
10503:)
10499:C
10493:B
10489:(
10482:A
10478:(
10474:,
10470:)
10466:C
10456:)
10452:A
10443:B
10439:(
10434:(
10410:)
10407:L
10401:(
10358:A
10348:)
10344:C
10338:B
10334:(
10330:,
10326:)
10322:C
10312:)
10308:A
10299:B
10295:(
10290:(
10266:)
10263:L
10260:P
10257:(
10228:A
10218:)
10214:C
10204:)
10200:A
10191:B
10187:(
10182:(
10178:,
10174:)
10170:C
10164:B
10160:(
10136:)
10133:L
10130:C
10127:(
10098:A
10088:)
10084:C
10074:)
10070:A
10061:B
10057:(
10052:(
10048:,
10044:)
10040:C
10030:)
10026:A
10017:B
10013:(
10008:(
10004:,
10000:)
9996:C
9990:B
9986:(
9962:)
9957:2
9953:L
9946:(
9917:A
9908:C
9902:,
9898:)
9894:C
9884:)
9880:A
9871:B
9867:(
9862:(
9858:,
9854:)
9850:C
9844:B
9840:(
9816:)
9813:L
9810:P
9807:(
9778:A
9768:)
9764:C
9754:)
9750:A
9741:B
9737:(
9732:(
9728:,
9725:C
9719:,
9715:)
9711:C
9705:B
9701:(
9677:)
9672:1
9668:L
9661:(
9632:A
9622:)
9618:A
9609:B
9605:(
9601:,
9598:C
9592:,
9588:)
9584:C
9578:B
9574:(
9550:)
9547:L
9541:(
9498:A
9489:A
9463:)
9460:I
9457:(
9408:B
9402:C
9396:,
9393:C
9387:B
9364:)
9361:L
9355:(
9326:B
9323:,
9320:C
9314:C
9308:B
9285:)
9282:R
9279:P
9276:(
9247:C
9244:,
9241:B
9235:C
9229:B
9206:)
9203:L
9197:(
9154:C
9151:,
9148:B
9142:C
9119:)
9116:R
9113:W
9110:(
9081:C
9075:C
9052:)
9049:I
9046:(
8998:C
8995:,
8992:B
8986:B
8963:)
8960:R
8957:W
8954:(
8925:B
8919:B
8896:)
8893:I
8890:(
8826:A
8820:,
8817:A
8791:)
8788:R
8785:P
8782:(
8753:A
8750:,
8747:A
8718:)
8715:R
8709:(
8680:A
8674:A
8651:)
8648:I
8645:(
8604:)
8599:)
8595:A
8585:)
8581:C
8571:)
8567:A
8558:B
8554:(
8549:(
8544:(
8536:)
8531:)
8527:C
8521:B
8517:(
8510:A
8506:(
8501:(
8462:)
8457:)
8453:)
8450:y
8447:,
8444:x
8441:(
8438:p
8434:(
8430:y
8423:(
8419:x
8409:)
8404:)
8400:)
8397:y
8394:,
8391:x
8388:(
8385:p
8381:(
8377:x
8370:(
8366:y
8340:)
8337:R
8331:(
8301:)
8297:)
8294:y
8291:,
8288:x
8285:(
8282:p
8278:(
8274:y
8264:)
8259:)
8255:)
8252:y
8249:,
8246:x
8243:(
8240:p
8236:(
8232:x
8225:(
8221:y
8195:)
8192:L
8186:(
8156:)
8152:)
8149:y
8146:,
8143:x
8140:(
8137:p
8133:(
8129:y
8119:)
8115:)
8112:y
8109:,
8106:x
8103:(
8100:p
8096:(
8092:x
8066:)
8063:R
8057:(
8028:)
8025:y
8022:,
8019:x
8016:(
8013:p
8006:)
8002:)
7999:y
7996:,
7993:x
7990:(
7987:p
7983:(
7979:x
7953:)
7950:L
7944:(
7915:)
7912:y
7909:,
7906:x
7903:(
7900:p
7894:)
7891:y
7888:,
7885:x
7882:(
7879:p
7856:)
7853:I
7850:(
7819:)
7816:L
7810:(
7790:)
7787:R
7781:(
7744:A
7735:A
7709:)
7706:R
7703:C
7700:(
7671:A
7662:A
7659:,
7656:A
7647:A
7621:)
7616:1
7612:R
7605:(
7576:A
7567:A
7564:,
7561:A
7535:)
7532:R
7529:P
7526:(
7497:A
7494:,
7491:A
7482:A
7456:)
7451:2
7447:R
7440:(
7411:A
7408:,
7405:A
7376:)
7373:R
7367:(
7338:A
7332:A
7309:)
7306:I
7303:(
7280:(
7262:A
7253:A
7175:A
7155:A
7135:A
7112:B
7106:A
7086:B
7066:A
6986:B
6946:A
6886:B
6880:A
6860:)
6857:R
6849:(
6825:]
6822:x
6818:/
6814:y
6811:[
6808:A
6788:]
6785:x
6781:/
6777:y
6774:[
6771:A
6751:A
6747:x
6723:)
6720:R
6712:(
6689:A
6664:A
6584:A
6544:)
6541:R
6533:(
6513:B
6507:A
6467:A
6427:)
6422:1
6418:L
6409:(
6346:y
6326:)
6323:L
6315:(
6295:)
6292:R
6284:(
6258:)
6253:R
6250:P
6245:(
6234:2
6226:,
6223:A
6220:,
6217:B
6214:,
6209:1
6184:2
6176:,
6173:B
6170:,
6167:A
6164:,
6159:1
6119:)
6114:L
6111:P
6106:(
6089:2
6081:,
6078:A
6075:,
6072:B
6069:,
6064:1
6039:2
6031:,
6028:B
6025:,
6022:A
6019:,
6014:1
5978:)
5973:R
5970:C
5965:(
5953:,
5950:A
5929:,
5926:A
5923:,
5920:A
5885:)
5880:L
5877:C
5872:(
5857:A
5854:,
5833:A
5830:,
5827:A
5824:,
5790:)
5785:R
5782:W
5777:(
5765:,
5762:A
5709:)
5704:L
5701:W
5696:(
5681:A
5678:,
5614:)
5611:R
5603:(
5591:,
5588:A
5585:x
5561:,
5558:]
5555:x
5551:/
5547:t
5544:[
5541:A
5506:)
5503:L
5495:(
5480:A
5477:x
5471:,
5450:]
5447:x
5443:/
5439:y
5436:[
5433:A
5430:,
5396:)
5393:R
5385:(
5373:,
5370:A
5367:x
5343:,
5340:]
5337:x
5333:/
5329:y
5326:[
5323:A
5288:)
5285:L
5277:(
5262:A
5259:x
5253:,
5232:]
5229:x
5225:/
5221:t
5218:[
5215:A
5212:,
5178:)
5175:R
5167:(
5155:,
5152:A
5125:A
5122:,
5090:)
5087:L
5079:(
5064:A
5058:,
5040:,
5037:A
5000:)
4997:R
4989:(
4977:,
4974:B
4968:A
4947:,
4944:B
4938:A
4935:,
4903:)
4900:L
4892:(
4880:,
4871:B
4865:A
4862:,
4856:,
4835:B
4832:,
4822:,
4819:A
4782:)
4779:R
4771:(
4759:,
4756:B
4750:A
4729:,
4726:B
4713:,
4710:A
4675:)
4672:L
4664:(
4649:B
4643:A
4640:,
4619:B
4616:,
4603:A
4600:,
4566:)
4561:2
4557:R
4548:(
4536:,
4533:B
4527:A
4506:,
4503:B
4468:)
4463:2
4459:L
4450:(
4435:B
4429:A
4426:,
4405:B
4402:,
4368:)
4363:1
4359:R
4350:(
4338:,
4335:B
4329:A
4308:,
4305:A
4270:)
4265:1
4261:L
4252:(
4237:B
4231:A
4228:,
4207:A
4204:,
4158:)
4153:t
4150:u
4147:C
4142:(
4130:,
4118:,
4094:,
4091:A
4087:A
4084:,
4046:)
4043:I
4040:(
4031:A
4025:A
3977:.
3933:R
3930:P
3910:L
3907:P
3887:R
3884:C
3864:L
3861:C
3841:R
3838:W
3818:L
3815:W
3793:]
3790:x
3786:/
3782:t
3779:[
3776:A
3756:t
3736:A
3716:x
3696:t
3676:A
3656:x
3636:t
3616:]
3613:x
3609:/
3605:t
3602:[
3599:A
3589:.
3530:y
3510:x
3488:t
3375:,
3369:,
3344:B
3324:A
3194:A
3191:,
3182:A
3179:,
3141:A
3138:,
3123:A
3117:,
3088:R
3062:A
3059:,
3032:A
3026:,
3003:L
2975:B
2972:,
2963:A
2960:,
2945:B
2939:A
2936:,
2907:R
2875:B
2872:,
2865:A
2862:,
2835:B
2829:A
2826:,
2804:L
2776:B
2773:,
2770:A
2767:,
2746:B
2740:A
2737:,
2708:R
2676:B
2673:,
2660:A
2657:,
2636:B
2630:A
2627:,
2605:L
2577:B
2574:,
2561:A
2558:,
2537:B
2531:A
2528:,
2500:R
2468:B
2465:,
2462:A
2459:,
2438:B
2432:A
2429:,
2406:L
2347:r
2344:,
2341:p
2335:q
2332:,
2329:p
2303:r
2297:q
2294:,
2291:p
2288:,
2285:r
2264:r
2258:q
2255:,
2252:p
2249:,
2246:p
2220:r
2214:p
2191:r
2185:p
2162:r
2156:q
2153:,
2150:p
2147:,
2144:r
2138:q
2117:r
2111:q
2108:,
2105:p
2102:,
2099:r
2093:p
2063:r
2057:q
2054:,
2051:p
2048:,
2045:)
2042:r
2036:q
2033:(
2027:)
2024:r
2018:p
2015:(
1985:r
1979:)
1976:q
1970:p
1967:(
1964:,
1961:)
1958:r
1952:q
1949:(
1943:)
1940:r
1934:p
1931:(
1905:r
1899:)
1896:q
1890:p
1887:(
1881:)
1878:r
1872:q
1869:(
1863:)
1860:r
1854:p
1851:(
1821:)
1818:r
1812:)
1809:q
1803:p
1800:(
1797:(
1791:)
1788:)
1785:r
1779:q
1776:(
1770:)
1767:r
1761:p
1758:(
1755:(
1703:)
1700:r
1694:)
1691:q
1685:p
1682:(
1679:(
1673:)
1670:)
1667:r
1661:q
1658:(
1652:)
1649:r
1643:p
1640:(
1637:(
1538:)
1533:k
1529:B
1511:2
1507:B
1495:1
1491:B
1479:n
1475:A
1460:2
1456:A
1447:1
1443:A
1439:(
1400:k
1396:B
1381:2
1377:B
1368:1
1364:B
1355:n
1351:A
1333:2
1329:A
1317:1
1313:A
1270:)
1265:k
1261:B
1246:1
1242:B
1238:(
1232:)
1227:n
1223:A
1208:1
1204:A
1200:(
1169:k
1165:B
1161:,
1155:,
1150:1
1146:B
1137:n
1133:A
1129:,
1123:,
1118:1
1114:A
1087:i
1083:B
1057:i
1053:A
1026:B
1003:B
983:k
963:n
941:i
937:B
914:i
910:A
862:,
857:k
853:B
849:,
843:,
838:1
834:B
825:n
821:A
817:,
811:,
806:1
802:A
767:B
761:)
756:n
752:A
737:1
733:A
729:(
700:B
692:n
688:A
684:,
678:,
673:1
669:A
645:B
623:2
619:A
596:1
592:A
566:i
562:A
541:B
518:B
496:i
492:A
443:0
437:n
417:B
395:i
391:A
367:B
359:n
355:A
351:,
345:,
340:2
336:A
332:,
327:1
323:A
258:B
235:B
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.