33:
384:(17). Adding these groups in order allows one to build a propositional calculus, then a predicate calculus, then a predicate calculus with equality, then a predicate calculus with equality allowing for the derivation of new rules. Some of the propositional calculus rules, like MTT, are superfluous and can be derived as rules from other rules.
1320:. A derived rule with no assumptions is a theorem, and can be introduced at any time with no assumptions. Some cite that as "TI(S)", for "theorem" instead of "sequent". Additionally, some cite only "SI" or "TI" in either case when a substitution instance isn't needed, as their propositions match the ones of the referenced proof exactly.
2021:, pp. 241–255) demonstrated a method of using one or more asterisks to the left of each line of proof to indicate dependencies. This is equivalent to Kleene's vertical bars. (It is not totally clear if Quine's asterisk notation appeared in the original 1950 edition or was added in a later edition.)
161:
of the table to indicate dependencies. However, Kleene's version has the advantage that it is presented, although only very sketchily, within a rigorous framework of metamathematical theory, whereas the books by Suppes and Lemmon are applications of the tabular layout for teaching introductory logic.
160:
A similar tabular layout is presented by Kleene. The main difference is that Kleene does not abbreviate the left-hand sides of assertions to line numbers, preferring instead to either give full lists of precedent propositions or alternatively indicate the left-hand sides by bars running down the left
361:
The second column holds line numbers. The third holds a wff, which is justified by the rule held in the fourth along with auxiliary information about other wffs, possibly in other proofs. The first column represents the line numbers of the assumptions the wff rests on, determined by the application
379:
The above proof is a valid one, but proofs don't need to be to conform to the general syntax of the proof system. To guarantee a sequent's validity, however, we must conform to carefully specified rules. The rules can be divided into four groups: the propositional rules (1-10), the predicate rules
156:
1934/1935 natural deduction system, in which proofs were presented in tree-diagram form rather than in the tabular form of Suppes and Lemmon. Although the tree-diagram layout has advantages for philosophical and educational purposes, the tabular layout is much more convenient for practical
2049:, pp. 50–58, 128–130) briefly demonstrated two kinds of practical logic proofs, one system using explicit quotations of antecedent propositions on the left of each line, the other system using vertical bar-lines on the left to indicate dependencies.
2009:
The historical development of tabular-layout natural deduction systems, which are rule-based, and which indicate antecedent propositions by line numbers (and related methods such as vertical bars or asterisks) includes the following publications.
366:
by listing the wffs at the cited lines as the premises and the wff at the line as the conclusion. Analogously, they can be converted into conditionals where the antecedent is a conjunction. These sequents are often listed above the proof, as
2226:
A particular advantage of Kleene's tabular natural deduction systems is that he proves the validity of the inference rules for both propositional calculus and predicate calculus. See
2035:, pp. 183–190, 215–219) uses sets of line numbers to indicate antecedent dependencies of the lines of sequential logical arguments based on natural deduction inference rules.
520:
The Rule of ∨-elimination (∨E): For a disjunction P∨Q, if one assumes P and Q and separately comes to the conclusion R from each, then one can conclude R. The rule is cited as "
1045:
912:
870:
766:
700:
1234:
1135:
1106:
1010:
939:
827:
797:
657:
1310:
1274:
1254:
1191:
1171:
1065:
979:
724:
50:
1579:
using monotonicity of entailment. Some have called the following technique, demonstrated in lines 3-6, the Rule of (Finite) Augmentation of
Premises:
2014:
1940: In a textbook, Quine indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
2424:
2402:
2383:
2361:
2317:
97:
69:
560:
conclude R with P and Q in their respective assumption pools. The assumptions are the collective pools of the two lines concluding R,
76:
2339:
116:
169:
Suppes–Lemmon notation is a notation for predicate calculus with equality, so its description can be separated into two parts: the
83:
2466:
54:
65:
2028:, pp. 25–150). This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line.
499:
43:
2371:
2349:
464:
previously in the proof, making this rule a biconditional. The assumption pool is the one of the line cited.
133:
90:
1576:
2090:
803:. UE is a duality with UI in that one can switch between quantified and free variables using these rules.
2281:
2248:
579:
502:, as when a proposition P is joined with Q with ∧I and separated with ∧E, it retains Q's assumptions.
391:
381:
170:
2305:
1015:
882:
840:
736:
670:
196:
185:
A proof is a table with 4 columns and unlimited ordered rows. From left to right the columns hold:
1207:
2420:
2398:
2379:
2357:
2335:
2313:
2197:
2059:
388:
The Rule of
Assumption (A): "A" justifies any wff. The only assumption is its own line number.
174:
149:
145:
2293:
2260:
2217:. See particularly pages 91–93 for Quine's line-number notation for antecedent dependencies.
2187:
2069:
2064:
2450:
2277:
2244:
153:
1114:
1085:
483:∧I" justifies P∧Q. The assumptions are the collective pool of the conjoined propositions.
2136:, pp. 25–150, for an introductory presentation of Suppes' natural deduction system.
2089:
Pelletier, Francis Jeffry; Hazen, Allen (2024), Zalta, Edward N.; Nodelman, Uri (eds.),
992:
921:
809:
779:
639:
2412:
1295:
1259:
1239:
1176:
1156:
1050:
964:
709:
141:
2460:
368:
2175:
202:
A set of numbers, possibly empty; a rule; and possibly a reference to another proof
362:
of the cited rule in context. Any line of any valid proof can be converted into a
2327:
460:
DN" justifies adding or subtracting two negation symbols from the wff at a line
137:
32:
2192:
2201:
2042:
is an introduction to logic proofs using a method based on that of Suppes.
2024:
1957: An introduction to practical logic theorem proving in a textbook by
981:
cannot appear in the conclusion P, any of its assumptions aside from line
2356:(Revised ed.). Cambridge, Massachusetts: Harvard University Press.
879:
Existential
Elimination (EE): For an existentially quantified predicate
17:
2378:(Fourth ed.). Cambridge, Massachusetts: Harvard University Press.
2297:
2264:
363:
2120:
for an introductory presentation of Lemmon's natural deduction system.
467:
The Rule of ∧-introduction (∧I): If propositions P and Q are at lines
2097:(Spring 2024 ed.), Metaphysics Research Lab, Stanford University
733:
Universal
Elimination (UE): For a universally quantified predicate
418:
MPP" justifies Q. The assumptions are the collective pool of lines
1332:
An example of the proof of a sequent (a theorem in this case):
2451:
A History of
Natural Deduction and Elementary Logic Textbooks.
989:. For this reason EE and EI are in duality, as one can assume
26:
490:
is a conjunction P∧Q, one can conclude either P or Q using "
1292:
SI(S) X" to justify introducing a substitution instance of
1082:
1997:
1774:
1762:
1584:
1568:
1337:
609:
Modus
Tollens (MTT): For propositions P→Q and ¬Q on lines
354:
211:
148:
proofs as sequences of justified steps. Both methods use
380:(11-14), the rules of equality (15-16), and the rule of
625:
MTT" to derive ¬P. The assumptions are those of lines
1298:
1262:
1242:
1210:
1179:
1159:
1117:
1088:
1053:
1018:
995:
967:
924:
885:
843:
812:
782:
739:
712:
673:
642:
57:. Unsourced material may be challenged and removed.
1304:
1268:
1248:
1228:
1185:
1165:
1129:
1100:
1059:
1039:
1004:
973:
933:
906:
864:
821:
791:
760:
718:
694:
651:
509:with proposition P one can introduce P∨Q citing "
2282:"Untersuchungen über das logische Schließen. II"
1236:proved in proof X and substitution instances of
1047:, as the EI will rid the conclusion of the term
598:RAA" and derive ¬Q from the assumptions of line
2249:"Untersuchungen über das logische Schließen. I"
806:Existential Introduction (EI): For a predicate
726:in anywhere. The assumptions are those of line
1067:. The assumptions are the assumptions on line
837:EI" to justify an existential quantification,
429:The Rule of Conditional Proof (CP): If a line
2174:Coburn, Barry; Miller, David (October 1977).
1204:Substitution Instance (SI(S)): For a sequent
636:Universal Introduction (UI): For a predicate
8:
2128:
2126:
2112:
2110:
2005:History of tabular natural deduction systems
1111:Equality Elimination (=E): For propositions
505:The Rule of ∨-introduction (∨I): For a line
702:, provided none of the assumptions on line
667:UI" to justify a universal quantification,
2176:"Two comments on Lemmon's Beginning logic"
433:with proposition P has an assumption line
189:A set of positive integers, possibly empty
2419:. Mineola, New York: Dover Publications.
2397:. Mineola, New York: Dover Publications.
2312:. Mineola, New York: Dover Publications.
2191:
1297:
1261:
1241:
1209:
1178:
1158:
1116:
1087:
1052:
1017:
994:
966:
923:
884:
842:
811:
781:
738:
711:
672:
641:
375:Rules of Predicate Calculus with Equality
117:Learn how and when to remove this message
1771:
1581:
1334:
1193:. The assumptions are the pool of lines
633:. This is proven from other rules above.
486:The Rule of ∧-elimination (∧E): If line
208:
2436:The collected papers of Gerhard Gentzen
2149:
2145:
2095:The Stanford Encyclopedia of Philosophy
2081:
552:assume P and Q respectively, and lines
544:has the initial disjunction P∨Q, lines
2227:
2161:
2133:
2117:
2046:
2039:
2025:
1012:and use EI to reach a conclusion from
582:(RAA): For a proposition P∧¬P on line
2271:Investigations into Logical Deduction
2214:
2032:
2018:
1312:. The assumptions are those of lines
7:
2091:"Natural Deduction Systems in Logic"
872:. The assumptions are those of line
799:. The assumptions are those of line
568:, minus the lines assuming P and Q,
55:adding citations to reliable sources
1769:An example of substitution and ∨E:
456:The Rule of Double Negation (DN): "
402:previously in the proof containing
165:Description of the deductive system
2180:Notre Dame Journal of Formal Logic
1153:=E" to justify changing any terms
1022:
889:
847:
743:
677:
25:
1108:citing "=I" with no assumptions.
31:
1992:
1987:
1984:
1981:
1976:
1971:
1968:
1965:
1960:
1954:
1951:
1948:
1943:
1938:
1935:
1932:
1927:
1918:
1915:
1912:
1907:
1902:
1899:
1896:
1891:
1885:
1882:
1879:
1874:
1869:
1866:
1863:
1858:
1849:
1846:
1843:
1838:
1819:
1816:
1813:
1809:Lines in-use and Justification
1757:
1752:
1749:
1746:
1741:
1735:
1732:
1729:
1724:
1715:
1712:
1709:
1704:
1690:
1687:
1684:
1679:
1673:
1670:
1667:
1662:
1653:
1650:
1647:
1642:
1636:
1633:
1630:
1625:
1620:
1617:
1614:
1610:Lines in-use and Justification
1563:
1552:
1549:
1547:
1542:
1531:
1528:
1526:
1521:
1502:
1499:
1496:
1491:
1480:
1477:
1474:
1469:
1463:
1460:
1457:
1452:
1433:
1430:
1427:
1422:
1411:
1408:
1405:
1400:
1395:
1392:
1389:
1384:
1373:
1370:
1367:
1363:Lines in-use and Justification
586:citing an assumption Q on line
349:
343:
340:
337:
332:
323:
320:
317:
312:
307:
304:
301:
296:
291:
288:
285:
280:
274:
271:
268:
263:
254:
251:
248:
244:Lines in-use and Justification
42:needs additional citations for
1028:
1019:
895:
886:
853:
844:
749:
740:
683:
674:
494:∧E". The assumptions are line
1:
2038:1965: The entire textbook by
1040:{\displaystyle (\exists x)Rx}
945:and derive P with it on line
907:{\displaystyle (\exists x)Rx}
865:{\displaystyle (\exists x)Rx}
761:{\displaystyle (\forall x)Rx}
695:{\displaystyle (\forall x)Rx}
206:The following is an example:
136:notation system developed by
2393:Stoll, Robert Roth (1979) .
2438:. Amsterdam: North-Holland.
2278:Gentzen, Gerhard Karl Erich
2245:Gentzen, Gerhard Karl Erich
1977:7, 8 SI(S) see above proof
1908:3, 4 SI(S) see above proof
1229:{\displaystyle P,Q\vdash R}
961:EE" to justify P. The term
2483:
2230:, pp. 44–45, 118–119.
2164:, pp. 50–56, 128–130.
500:monotonicity of entailment
445:CP" justifies Q→P. All of
394:(MPP): If there are lines
2286:Mathematische Zeitschrift
2253:Mathematische Zeitschrift
513:∨I". The assumptions are
173:and the context specific
2372:Quine, Willard Van Orman
2350:Quine, Willard Van Orman
2193:10.1305/ndjfl/1093888128
498:'s. ∧I and ∧E allow for
144:' method, it represents
66:"Suppes–Lemmon notation"
2413:Suppes, Patrick Colonel
134:natural deductive logic
2467:Propositional calculus
1577:principle of explosion
1306:
1270:
1250:
1230:
1187:
1167:
1131:
1102:
1061:
1041:
1006:
975:
935:
908:
866:
823:
793:
762:
720:
696:
653:
130:Suppes–Lemmon notation
2417:Introduction to logic
2269:(English translation
2045:1967: In a textbook,
2017:1950: In a textbook,
1307:
1271:
1251:
1231:
1188:
1168:
1132:
1103:
1062:
1042:
1007:
976:
936:
909:
867:
824:
794:
763:
721:
697:
654:
449:'s assumptions aside
437:with proposition Q, "
2434:Szabo, M.E. (1969).
2395:Set Theory and Logic
2306:Kleene, Stephen Cole
1296:
1260:
1240:
1208:
1177:
1157:
1115:
1086:
1051:
1016:
993:
965:
922:
883:
841:
810:
780:
737:
710:
671:
640:
580:Reductio Ad Absurdum
392:Modus Ponendo Ponens
181:General Proof Syntax
171:general proof syntax
51:improve this article
2328:Lemmon, Edward John
1130:{\displaystyle a=b}
1101:{\displaystyle a=a}
941:to be true on line
197:well-formed formula
2449:Pelletier, Jeff, "
2354:Mathematical logic
2310:Mathematical logic
2298:10.1007/bf01201363
2265:10.1007/BF01201353
1993:1, 2, 5, 6, 9, ∨E
1796:Assumption number
1597:Assumption number
1350:Assumption number
1302:
1266:
1246:
1226:
1183:
1163:
1127:
1098:
1057:
1037:
1005:{\displaystyle Ra}
1002:
971:
934:{\displaystyle Ra}
931:
904:
862:
822:{\displaystyle Ra}
819:
792:{\displaystyle Ra}
789:
758:
716:
692:
652:{\displaystyle Ra}
649:
231:Assumption number
192:A positive integer
2426:978-0-486-40687-9
2404:978-0-486-63829-4
2385:978-0-674-57176-1
2363:978-0-674-55451-1
2334:. Thomas Nelson.
2319:978-0-486-42533-7
2070:Deductive systems
2060:Natural deduction
2002:
2001:
1767:
1766:
1573:
1572:
1305:{\displaystyle R}
1269:{\displaystyle Q}
1249:{\displaystyle P}
1186:{\displaystyle b}
1166:{\displaystyle a}
1060:{\displaystyle a}
974:{\displaystyle a}
719:{\displaystyle a}
359:
358:
146:natural deduction
127:
126:
119:
101:
16:(Redirected from
2474:
2439:
2430:
2408:
2389:
2376:Methods of logic
2367:
2345:
2323:
2301:
2268:
2231:
2224:
2218:
2212:
2206:
2205:
2195:
2171:
2165:
2159:
2153:
2143:
2137:
2130:
2121:
2114:
2105:
2104:
2103:
2102:
2086:
2065:Sequent calculus
1772:
1582:
1335:
1311:
1309:
1308:
1303:
1284:, one can cite "
1275:
1273:
1272:
1267:
1255:
1253:
1252:
1247:
1235:
1233:
1232:
1227:
1192:
1190:
1189:
1184:
1172:
1170:
1169:
1164:
1145:, one can cite "
1136:
1134:
1133:
1128:
1107:
1105:
1104:
1099:
1071:and any on line
1066:
1064:
1063:
1058:
1046:
1044:
1043:
1038:
1011:
1009:
1008:
1003:
980:
978:
977:
972:
940:
938:
937:
932:
913:
911:
910:
905:
871:
869:
868:
863:
828:
826:
825:
820:
798:
796:
795:
790:
772:, one can cite "
767:
765:
764:
759:
725:
723:
722:
717:
701:
699:
698:
693:
663:, one can cite "
658:
656:
655:
650:
590:, one can cite "
540:∨E", where line
409:
405:
209:
122:
115:
111:
108:
102:
100:
59:
35:
27:
21:
2482:
2481:
2477:
2476:
2475:
2473:
2472:
2471:
2457:
2456:
2446:
2433:
2427:
2411:
2405:
2392:
2386:
2370:
2364:
2348:
2342:
2332:Beginning logic
2326:
2320:
2304:
2276:
2243:
2240:
2235:
2234:
2225:
2221:
2213:
2209:
2173:
2172:
2168:
2160:
2156:
2144:
2140:
2131:
2124:
2115:
2108:
2100:
2098:
2088:
2087:
2083:
2078:
2056:
2007:
1575:A proof of the
1330:
1324:
1294:
1293:
1258:
1257:
1238:
1237:
1206:
1205:
1175:
1174:
1155:
1154:
1137:and P on lines
1113:
1112:
1084:
1083:
1049:
1048:
1014:
1013:
991:
990:
963:
962:
949:, we can cite "
920:
919:
918:, if we assume
881:
880:
839:
838:
808:
807:
778:
777:
776:UE" to justify
735:
734:
708:
707:
669:
668:
638:
637:
410:respectively, "
407:
403:
377:
183:
167:
150:inference rules
140:. Derived from
123:
112:
106:
103:
60:
58:
48:
36:
23:
22:
15:
12:
11:
5:
2480:
2478:
2470:
2469:
2459:
2458:
2455:
2454:
2445:
2444:External links
2442:
2441:
2440:
2431:
2425:
2409:
2403:
2390:
2384:
2368:
2362:
2346:
2340:
2324:
2318:
2302:
2292:(3): 405–431.
2274:
2259:(2): 176–210.
2239:
2236:
2233:
2232:
2219:
2207:
2186:(4): 607–610.
2166:
2154:
2138:
2122:
2106:
2080:
2079:
2077:
2074:
2073:
2072:
2067:
2062:
2055:
2052:
2051:
2050:
2043:
2036:
2029:
2022:
2015:
2006:
2003:
2000:
1999:
1995:
1994:
1991:
1986:
1983:
1979:
1978:
1975:
1970:
1967:
1963:
1962:
1959:
1953:
1950:
1946:
1945:
1942:
1937:
1934:
1930:
1929:
1926:
1917:
1914:
1910:
1909:
1906:
1901:
1898:
1894:
1893:
1890:
1884:
1881:
1877:
1876:
1873:
1868:
1865:
1861:
1860:
1857:
1848:
1845:
1841:
1840:
1837:
1818:
1815:
1811:
1810:
1807:
1800:
1797:
1793:
1792:
1765:
1764:
1760:
1759:
1756:
1751:
1748:
1744:
1743:
1740:
1734:
1731:
1727:
1726:
1723:
1714:
1711:
1707:
1706:
1703:
1689:
1686:
1682:
1681:
1678:
1672:
1669:
1665:
1664:
1661:
1652:
1649:
1645:
1644:
1641:
1635:
1632:
1628:
1627:
1624:
1619:
1616:
1612:
1611:
1608:
1601:
1598:
1594:
1593:
1571:
1570:
1566:
1565:
1562:
1551:
1548:
1545:
1544:
1541:
1530:
1527:
1524:
1523:
1520:
1501:
1498:
1494:
1493:
1490:
1479:
1476:
1472:
1471:
1468:
1462:
1459:
1455:
1454:
1451:
1432:
1429:
1425:
1424:
1421:
1410:
1407:
1403:
1402:
1399:
1394:
1391:
1387:
1386:
1383:
1372:
1369:
1365:
1364:
1361:
1354:
1351:
1347:
1346:
1329:
1326:
1322:
1321:
1301:
1265:
1245:
1225:
1222:
1219:
1216:
1213:
1202:
1182:
1173:terms in P to
1162:
1126:
1123:
1120:
1109:
1097:
1094:
1091:
1080:
1056:
1036:
1033:
1030:
1027:
1024:
1021:
1001:
998:
970:
930:
927:
903:
900:
897:
894:
891:
888:
877:
861:
858:
855:
852:
849:
846:
833:one can cite "
818:
815:
804:
788:
785:
757:
754:
751:
748:
745:
742:
731:
715:
706:have the term
691:
688:
685:
682:
679:
676:
648:
645:
634:
617:one can cite "
607:
577:
518:
503:
484:
465:
454:
427:
389:
376:
373:
357:
356:
352:
351:
348:
342:
339:
335:
334:
331:
322:
319:
315:
314:
311:
306:
303:
299:
298:
295:
290:
287:
283:
282:
279:
273:
270:
266:
265:
262:
253:
250:
246:
245:
242:
235:
232:
228:
227:
204:
203:
200:
193:
190:
182:
179:
166:
163:
157:applications.
125:
124:
39:
37:
30:
24:
14:
13:
10:
9:
6:
4:
3:
2:
2479:
2468:
2465:
2464:
2462:
2452:
2448:
2447:
2443:
2437:
2432:
2428:
2422:
2418:
2414:
2410:
2406:
2400:
2396:
2391:
2387:
2381:
2377:
2373:
2369:
2365:
2359:
2355:
2351:
2347:
2343:
2341:0-17-712040-1
2337:
2333:
2329:
2325:
2321:
2315:
2311:
2307:
2303:
2299:
2295:
2291:
2287:
2283:
2279:
2275:
2272:
2266:
2262:
2258:
2254:
2250:
2246:
2242:
2241:
2237:
2229:
2223:
2220:
2216:
2211:
2208:
2203:
2199:
2194:
2189:
2185:
2181:
2177:
2170:
2167:
2163:
2158:
2155:
2151:
2147:
2142:
2139:
2135:
2129:
2127:
2123:
2119:
2113:
2111:
2107:
2096:
2092:
2085:
2082:
2075:
2071:
2068:
2066:
2063:
2061:
2058:
2057:
2053:
2048:
2044:
2041:
2040:Lemmon (1965)
2037:
2034:
2030:
2027:
2023:
2020:
2016:
2013:
2012:
2011:
2004:
1996:
1990:
1980:
1974:
1964:
1958:
1947:
1941:
1931:
1925:
1921:
1911:
1905:
1895:
1889:
1878:
1872:
1862:
1856:
1852:
1842:
1835:
1831:
1827:
1823:
1812:
1808:
1805:
1801:
1798:
1795:
1794:
1790:
1786:
1782:
1778:
1773:
1770:
1761:
1755:
1745:
1739:
1728:
1722:
1718:
1708:
1702:
1698:
1694:
1683:
1677:
1666:
1660:
1656:
1646:
1640:
1629:
1623:
1613:
1609:
1606:
1602:
1599:
1596:
1595:
1591:
1587:
1583:
1580:
1578:
1567:
1560:
1556:
1546:
1539:
1535:
1525:
1518:
1514:
1510:
1506:
1495:
1488:
1484:
1473:
1467:
1456:
1449:
1445:
1441:
1437:
1426:
1419:
1415:
1404:
1398:
1388:
1381:
1377:
1366:
1362:
1359:
1355:
1352:
1349:
1348:
1345:
1341:
1336:
1333:
1327:
1325:
1319:
1315:
1299:
1291:
1287:
1283:
1279:
1263:
1243:
1223:
1220:
1217:
1214:
1211:
1203:
1200:
1196:
1180:
1160:
1152:
1148:
1144:
1140:
1124:
1121:
1118:
1110:
1095:
1092:
1089:
1081:
1078:
1074:
1070:
1054:
1034:
1031:
1025:
999:
996:
988:
985:, or on line
984:
968:
960:
956:
952:
948:
944:
928:
925:
917:
901:
898:
892:
878:
875:
859:
856:
850:
836:
832:
816:
813:
805:
802:
786:
783:
775:
771:
755:
752:
746:
732:
729:
713:
705:
689:
686:
680:
666:
662:
646:
643:
635:
632:
628:
624:
620:
616:
612:
608:
605:
601:
597:
593:
589:
585:
581:
578:
575:
571:
567:
563:
559:
555:
551:
547:
543:
539:
535:
531:
527:
523:
519:
516:
512:
508:
504:
501:
497:
493:
489:
485:
482:
478:
474:
470:
466:
463:
459:
455:
452:
448:
444:
440:
436:
432:
428:
425:
421:
417:
413:
401:
397:
393:
390:
387:
386:
385:
383:
374:
372:
370:
369:Modus Tollens
365:
353:
347:
336:
330:
326:
316:
310:
300:
294:
284:
278:
267:
261:
257:
247:
243:
240:
236:
233:
230:
229:
226:
222:
218:
214:
210:
207:
201:
198:
194:
191:
188:
187:
186:
180:
178:
176:
172:
164:
162:
158:
155:
152:derived from
151:
147:
143:
139:
135:
131:
121:
118:
110:
99:
96:
92:
89:
85:
82:
78:
75:
71:
68: –
67:
63:
62:Find sources:
56:
52:
46:
45:
40:This article
38:
34:
29:
28:
19:
2435:
2416:
2394:
2375:
2353:
2331:
2309:
2289:
2285:
2270:
2256:
2252:
2222:
2215:Quine (1981)
2210:
2183:
2179:
2169:
2157:
2150:Gentzen 1935
2146:Gentzen 1934
2141:
2099:, retrieved
2094:
2084:
2047:Kleene (2002
2026:Suppes (1999
2008:
1988:
1972:
1956:
1939:
1923:
1919:
1903:
1887:
1870:
1854:
1850:
1833:
1829:
1825:
1821:
1803:
1799:Line number
1788:
1784:
1780:
1776:
1768:
1753:
1737:
1720:
1716:
1700:
1696:
1692:
1675:
1658:
1654:
1643:A (for RAA)
1638:
1626:A (for RAA)
1621:
1604:
1600:Line number
1589:
1585:
1574:
1558:
1554:
1537:
1533:
1516:
1512:
1508:
1504:
1486:
1482:
1465:
1447:
1443:
1439:
1435:
1417:
1413:
1401:A (for RAA)
1396:
1385:A (for RAA)
1379:
1375:
1357:
1353:Line number
1343:
1339:
1331:
1323:
1317:
1313:
1289:
1285:
1281:
1277:
1198:
1194:
1150:
1146:
1142:
1138:
1076:
1072:
1068:
986:
982:
958:
954:
950:
946:
942:
915:
873:
834:
830:
800:
773:
769:
727:
703:
664:
660:
630:
626:
622:
618:
614:
610:
603:
599:
595:
591:
587:
583:
573:
569:
565:
561:
557:
553:
549:
545:
541:
537:
533:
529:
525:
521:
514:
510:
506:
495:
491:
487:
480:
476:
472:
468:
461:
457:
450:
446:
442:
438:
434:
430:
423:
419:
415:
411:
399:
395:
382:substitution
378:
360:
345:
328:
324:
308:
297:A (for RAA)
292:
276:
259:
255:
238:
234:Line number
224:
220:
216:
212:
205:
184:
168:
159:
129:
128:
113:
104:
94:
87:
80:
73:
61:
49:Please help
44:verification
41:
2228:Kleene 2002
2162:Kleene 2002
2134:Suppes 1999
2118:Lemmon 1965
2033:Stoll (1979
2019:Quine (1982
1928:A (for ∨E)
1859:A (for ∨E)
1680:A (for DN)
1075:aside from
602:aside from
138:E.J. Lemmon
2273:in Szabo.)
2238:References
2101:2024-05-01
1742:4, 6, RAA
1543:1, 7, RAA
1470:2, 4, RAA
371:is above.
350:3, 5, RAA
313:1, 3, MPP
107:April 2010
77:newspapers
2415:(1999) .
2374:(1982) .
2352:(1981) .
2308:(2002) .
2202:0029-4527
1802:Formula (
1705:3, 4, ∧I
1663:1, 2, ∧I
1603:Formula (
1522:1, 6, ∧I
1453:3, 1, ∧I
1356:Formula (
1276:on lines
1221:⊢
1023:∃
890:∃
848:∃
744:∀
678:∀
453:are kept.
333:2, 4, ∧I
237:Formula (
154:Gentzen's
2461:Category
2330:(1965).
2280:(1935).
2247:(1934).
2054:See also
1710:1, 2, 4
1685:1, 2, 4
1328:Examples
914:on line
829:on line
768:on line
659:on line
318:1, 2, 3
199:(or wff)
18:System L
1725:5, ∧E
364:sequent
91:scholar
2423:
2401:
2382:
2360:
2338:
2316:
2200:
2031:1963:
1998:Q.E.D
1791:) ⊢ r
1763:Q.E.D
1758:7, DN
1569:Q.E.D
1564:8, DN
1511:) ∧ ¬(
1492:5, ∨I
1442:) ∧ ¬(
1423:2, ∨I
355:Q.E.D
142:Suppes
93:
86:
79:
72:
64:
2076:Notes
1985:(10)
1961:2 ∧E
1944:6 ∧E
1892:2 ∧E
1875:2 ∧E
1828:) ∨ (
1783:) ∨ (
1747:1, 2
1730:1, 2
1699:) ∧ ¬
1648:1, 2
1428:1, 2
404:P → Q
338:1, 2
302:1, 3
175:rules
132:is a
98:JSTOR
84:books
2421:ISBN
2399:ISBN
2380:ISBN
2358:ISBN
2336:ISBN
2314:ISBN
2198:ISSN
2132:See
2116:See
1969:(9)
1952:(8)
1936:(7)
1916:(6)
1900:(5)
1883:(4)
1867:(3)
1847:(2)
1817:(1)
1750:(8)
1733:(7)
1713:(6)
1688:(5)
1671:(4)
1651:(3)
1634:(2)
1618:(1)
1592:⊢ q
1557:∨ ¬
1550:(9)
1536:∨ ¬
1529:(8)
1515:∨ ¬
1507:∨ ¬
1500:(7)
1485:∨ ¬
1478:(6)
1461:(5)
1446:∨ ¬
1438:∨ ¬
1431:(4)
1416:∨ ¬
1409:(3)
1393:(2)
1378:∨ ¬
1371:(1)
1342:∨ ¬
1316:and
1280:and
1256:and
1197:and
1141:and
629:and
613:and
572:and
564:and
556:and
548:and
471:and
422:and
406:and
398:and
341:(6)
321:(5)
305:(4)
289:(3)
272:(2)
252:(1)
70:news
2294:doi
2261:doi
2188:doi
1922:∧ ¬
1853:∧ ¬
1832:∧ ¬
1824:∧ ¬
1804:wff
1787:∧ ¬
1779:∧ ¬
1719:∧ ¬
1695:∧ ¬
1657:∧ ¬
1605:wff
1588:, ¬
1532:¬¬(
1358:wff
517:'s.
475:, "
327:∧ ¬
239:wff
223:⊢ ¬
219:, ¬
53:by
2463::
2290:39
2288:.
2284:.
2257:39
2255:.
2251:.
2196:.
2184:18
2182:.
2178:.
2148:,
2125:^
2109:^
2093:,
1982:1
1966:6
1949:6
1933:6
1913:6
1897:2
1880:2
1864:2
1844:2
1839:A
1836:)
1814:1
1806:)
1736:¬¬
1668:4
1631:2
1615:1
1607:)
1561:)
1540:)
1519:)
1497:1
1489:)
1475:1
1458:1
1450:)
1420:)
1406:2
1390:2
1382:)
1374:¬(
1368:1
1360:)
286:3
281:A
269:2
264:A
258:→
249:1
241:)
215:→
195:A
177:.
2453:"
2429:.
2407:.
2388:.
2366:.
2344:.
2322:.
2300:.
2296::
2267:.
2263::
2204:.
2190::
2152:.
1989:r
1973:r
1957:q
1955:¬
1940:q
1924:q
1920:q
1904:r
1888:p
1886:¬
1871:p
1855:p
1851:p
1834:q
1830:q
1826:p
1822:p
1820:(
1789:q
1785:q
1781:p
1777:p
1775:(
1754:q
1738:q
1721:p
1717:p
1701:q
1697:p
1693:p
1691:(
1676:q
1674:¬
1659:p
1655:p
1639:p
1637:¬
1622:p
1590:p
1586:p
1559:p
1555:p
1553:(
1538:p
1534:p
1517:p
1513:p
1509:p
1505:p
1503:(
1487:p
1483:p
1481:(
1466:p
1464:¬
1448:p
1444:p
1440:p
1436:p
1434:(
1418:p
1414:p
1412:(
1397:p
1380:p
1376:p
1344:p
1340:p
1338:⊢
1318:b
1314:a
1300:R
1290:b
1288:,
1286:a
1282:b
1278:a
1264:Q
1244:P
1224:R
1218:Q
1215:,
1212:P
1201:.
1199:b
1195:a
1181:b
1161:a
1151:b
1149:,
1147:a
1143:b
1139:a
1125:b
1122:=
1119:a
1096:a
1093:=
1090:a
1079:.
1077:b
1073:c
1069:a
1055:a
1035:x
1032:R
1029:)
1026:x
1020:(
1000:a
997:R
987:a
983:b
969:a
959:c
957:,
955:b
953:,
951:a
947:c
943:b
929:a
926:R
916:a
902:x
899:R
896:)
893:x
887:(
876:.
874:a
860:x
857:R
854:)
851:x
845:(
835:a
831:a
817:a
814:R
801:a
787:a
784:R
774:a
770:a
756:x
753:R
750:)
747:x
741:(
730:.
728:a
714:a
704:a
690:x
687:R
684:)
681:x
675:(
665:a
661:a
647:a
644:R
631:b
627:a
623:b
621:,
619:a
615:b
611:a
606:.
604:b
600:a
596:a
594:,
592:b
588:b
584:a
576:.
574:d
570:b
566:e
562:c
558:e
554:c
550:d
546:b
542:a
538:e
536:,
534:d
532:,
530:c
528:,
526:b
524:,
522:a
515:a
511:a
507:a
496:a
492:a
488:a
481:b
479:,
477:a
473:b
469:a
462:a
458:a
451:b
447:a
443:a
441:,
439:b
435:b
431:a
426:.
424:b
420:a
416:b
414:,
412:a
408:P
400:b
396:a
346:p
344:¬
329:q
325:q
309:q
293:p
277:q
275:¬
260:q
256:p
225:p
221:q
217:q
213:p
120:)
114:(
109:)
105:(
95:·
88:·
81:·
74:·
47:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
