2988:(US), we can change each of these axiom schemas into a single axiom, replacing each schematic variable by some propositional variable that isn't mentioned in any axiom to get what we call the substitutional axiomatisation. Both formalisations have variables, but where the one-rule axiomatisation has schematic variables that are outside the logic's language, the substitutional axiomatisation uses propositional variables that do the same work by expressing the idea of a variable ranging over formulae with a rule that uses substitution.
6903:
340:
5093:
necessary elements of his
Formalist "proof theory"—e.g. induction axioms, recursion axioms, etc; he also offers up a spirited defense against L.E.J. Brouwer's Intuitionism. Also see Hermann Weyl's (1927) comments and rebuttal (pp. 480–484), Paul Bernay's (1927) appendix to Hilbert's lecture (pp. 485–489) and Luitzen Egbertus Jan Brouwer's (1927) response (pp. 490–495)
4094:
3529:
2205:
279:
264:
of a rather simple form. The same cannot be done with the other two deductions systems: as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided – not even if we want to use them just for proving derivability
5092:
Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367–392), presents his 17 axioms—axioms of implication #1-4, axioms about & and V #5-10, axioms of negation #11-12, his logical ε-axiom #13, axioms of equality #14-15, and axioms of number #16-17—along with the other
2265:
There is an unlimited amount of axiomatisations of predicate logic, since for any logic there is freedom in choosing axioms and rules that characterise that logic. We describe here a
Hilbert system with nine axioms and just the rule modus ponens, which we call the one-rule axiomatisation and which
5117:
See in particular
Chapter IV Formal System (pp. 69–85) wherein Kleene presents subchapters §16 Formal symbols, §17 Formation rules, §18 Free and bound variables (including substitution), §19 Transformation rules (e.g. modus ponens) -- and from these he presents 21 "postulates"—18 axioms
559:
is an infinite set of axioms obtained by substituting all formulas of some form into a specific pattern. The set of logical axioms includes not only those axioms generated from this pattern, but also any generalization of one of those axioms. A generalization of a formula is obtained by prefixing
171:
below—but other sources use the term "Hilbert-style" as encompassing both systems with schematic axioms and systems with a rule of substitution, as this article does. The use of "Hilbert-style" and similar terms to describe axiomatic proof systems in logic is due to the influence of
Hilbert and
2549:
103:
While all sources that refer to an "axiomatic" logical proof system system characterize it simply as a logical proof system with axioms, sources that use variants of the term "Hilbert system" sometimes define it in different ways, which will not be used in this article. For instance,
3304:
3605:
formula θ involving only negation, implication, and universal quantification, then φ is derivable in the extended system if and only if θ is derivable in the original system. When fully extended, a
Hilbert system will resemble more closely a system of
2767:
357:) is a finite sequence of formulas in which each formula is either an axiom or is obtained from previous formulas by a rule of inference. These formal deductions are meant to mirror natural-language proofs, although they are far more detailed.
4078:
1526:
162:
as the only inference rules. A specific set of axioms is also sometimes called "the
Hilbert system", or "the Hilbert-style calculus". Sometimes, "Hilbert-style" is used to convey the type of axiomatic system that has its axioms given in
2615:
1395:
One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemas (metalogical variables that may stand for any
1069:
These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.
862:
2448:
5118:
and 3 "immediate-consequence" relations divided as follows: Postulates for the propostional calculus #1-8, Additional postulates for the predicate calculus #9-12, and
Additional postulates for number theory #13-21.
2052:
3756:
1186:
938:
1583:
2825:
3513:
1820:
3859:
2959:
2872:
996:
1314:
3217:
4901:
3686:
3346:
3180:
2441:
96:, which is used by many authors as a sole less specific term to declare their Hilbert systems, without mentioning any more specific terms. In this context, "Hilbert systems" are contrasted with
3387:
Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on
Metatheorems), in which case the rules Q6 and Q7 are redundant.
1884:
3893:
1439:
3927:
1371:
1084:
showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence
614:
3968:
209:
take the opposite tack, including many deduction rules but very few or no axiom schemas. The most commonly studied
Hilbert systems have either just one rule of inference –
4002:
2116:
774:
2775:
is achieved by adding axioms P4i and P5i to positive implicational logic, or by adding axiom P5i to minimal logic. Both P4i and P5i are theorems of classical propositional logic.
1940:
1376:
Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule. The exact same system was given (with an explicit substitution rule) by
1064:
1030:
2692:
658:
506:
436:
5282:
1726:
135:
2683:
2397:
1639:; as the authors that originally defined the term "Frege system" note, this actually excludes Frege's own system, given above, since it had axioms instead of axiom schemes.
1630:
2160:
1227:
3117:
2657:
1600:"set.mm" formal proof database. In fact, the very idea of using axiom schemes to replace the rule of substitution is attributed to von Neumann. The schematic version of P
160:
3210:
1126:
5957:
3088:
3019:
2324:
546:
480:
402:
378:
2901:
2344:
2284:
2188:
1674:
4009:
3800:
3370:
3059:
2979:
2364:
1445:
526:
456:
2304:
3418:
3776:
3039:
2877:
Note that these are axiom schemas, which represent infinitely many specific instances of axioms. For example, P1 might represent the particular axiom instance
4162:
add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.
6939:
6040:
5181:
2556:
3601:
that permit the use of additional connectives. These extensions are called conservative because if a formula φ involving new connectives is rewritten as a
781:
7176:
5066:
David
Hilbert (1927) "The foundations of mathematics", translated by Stephan Bauer-Menglerberg and Dagfinn Føllesdal (pp. 464–479). in:
2544:{\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}
6354:
339:
6512:
5030:
4985:
4948:
4850:
4800:
4745:
4709:
4682:
4655:
4620:
4593:
4566:
4539:
4488:
4453:
4426:
4396:
4369:
4342:
4315:
4260:
4228:
1947:
5300:
3699:
1135:
869:
237:. Some systems use a finite list of concrete formulas as axioms instead of an infinite set of formulas via axiom schemas, in which case the
6367:
5690:
2629:
1532:
5952:
7217:
6372:
6362:
6099:
5305:
2782:
88:
It is defined as a deductive system that generates theorems from axioms and inference rules, especially if the only inference rule is
5850:
5296:
3430:
7017:
6508:
5108:
5083:
4141:
3576:
2252:
326:
6932:
6605:
6349:
5174:
2981:
is a place where any formula can be placed. A variable such as this that ranges over formulae is called a 'schematic variable'.
1733:
178:
7055:
5910:
5603:
5344:
4332:
3820:
2906:
2832:
945:
4115:
3550:
3299:{\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}
2266:
describes classical equational logic. We deal with a minimal language for this logic, where formulas use only the connectives
2226:
1233:
300:
260:, no hypothetical judgments, then one can formalize the Hilbert system in such a way that its rules of inference contain only
7186:
6866:
6568:
6331:
6326:
6151:
5572:
5256:
4119:
3554:
2230:
304:
4637:
4470:
6861:
6644:
6561:
6274:
6205:
6082:
5324:
3626:
3311:
3130:
2625:
2404:
261:
5932:
4556:
6786:
6612:
6298:
5531:
5937:
7181:
7007:
6925:
6269:
6008:
5266:
5167:
1827:
6664:
6659:
4421:. Oxford : New York: Clarendon Press; Oxford University Press. pp. 4–5, 8–13, 18–19, 22, 27, 29, 191, 194.
3866:
2369:
The first four logical axiom schemas allow (together with modus ponens) for the manipulation of logical connectives.
1406:
4642:. Cambridge Tracts in Theoretical Computer Science (2 ed.). Cambridge: Cambridge University Press. p. 51.
4475:. Cambridge Tracts in Theoretical Computer Science (2 ed.). Cambridge: Cambridge University Press. p. 51.
4443:
4305:
3900:
3381:
1320:
563:
7113:
6949:
6593:
6183:
5577:
5545:
5236:
3941:
3589:
It is common to include in a Hilbert system only axioms for the logical operators implication and negation towards
3380:. Likewise, these three rules extend system for intuitionstic propositional logic (with P1-3 and P4i and P5i) to
5310:
3975:
7080:
6883:
6832:
6729:
6227:
6188:
5665:
3377:
2059:
6724:
5339:
7212:
6654:
6193:
6045:
6028:
5751:
5231:
5060:
4104:
3539:
2215:
289:
218:
7060:
6556:
6533:
6494:
6380:
6321:
5967:
5887:
5731:
5675:
5288:
4762:
4386:
4171:
4123:
4108:
3590:
3558:
3543:
2762:{\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}
2234:
2219:
308:
293:
741:
7161:
7146:
7103:
7065:
6970:
6846:
6573:
6551:
6518:
6411:
6257:
6242:
6215:
6166:
6050:
5985:
5810:
5776:
5771:
5645:
5476:
5453:
5153:
4277:
3594:
2985:
1895:
1037:
1003:
238:
230:
5132:
4612:
Logics in AI: European Workshop JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990. Proceedings
4361:
Logics in AI: European Workshop JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990. Proceedings
619:
485:
415:
7207:
7123:
7098:
6776:
6629:
6421:
6139:
5875:
5781:
5640:
5625:
5506:
5481:
3123:
The next three logical axiom schemas provide ways to add, manipulate, and remove universal quantifiers.
234:
6902:
5144:
7118:
7075:
6749:
6711:
6588:
6392:
6232:
6156:
6134:
5962:
5920:
5819:
5786:
5650:
5438:
5349:
2772:
1687:
727:
701:
115:
105:
4359:
2662:
2376:
1611:
7128:
6878:
6769:
6754:
6734:
6691:
6578:
6528:
6454:
6399:
6336:
6129:
6124:
6072:
5840:
5829:
5501:
5401:
5329:
5320:
5316:
5251:
5246:
3602:
2127:
1397:
1194:
669:
214:
5103:(10th impression with 1971 corrections ed.). Amsterdam NY: North Holland Publishing Company.
3093:
2326:. Later we show how the system can be extended to include additional logical connectives, such as
7050:
6997:
6957:
6907:
6676:
6639:
6624:
6617:
6600:
6386:
6252:
6178:
6161:
6114:
5927:
5836:
5670:
5655:
5615:
5567:
5552:
5540:
5496:
5471:
5241:
5190:
4966:"How to lie without being (easily) convicted and the lengths of proofs in propositional calculus"
2639:
140:
6404:
5860:
1081:
3193:
1087:
7035:
6990:
6842:
6649:
6459:
6449:
6341:
6222:
6057:
6033:
5814:
5798:
5703:
5680:
5557:
5526:
5491:
5386:
5221:
5104:
5079:
5026:
4981:
4944:
4921:
4846:
4796:
4741:
4705:
4678:
4651:
4616:
4589:
4562:
4535:
4484:
4449:
4422:
4392:
4365:
4338:
4311:
4256:
4224:
4176:
4159:
4073:{\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}
3607:
3598:
3064:
2995:
2309:
1521:{\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}
257:
249:
206:
202:
194:
173:
97:
82:
17:
6917:
531:
465:
387:
363:
225:, as well – and several infinite axiom schemas. Hilbert systems for alethic
7156:
7040:
6980:
6856:
6851:
6744:
6701:
6523:
6484:
6479:
6464:
6290:
6247:
6144:
5942:
5892:
5466:
5428:
4973:
4913:
4643:
4476:
4181:
2880:
2329:
2269:
2167:
1653:
1593:
256:
contain some context-changing rules. Thus, if one is interested only in the derivability of
253:
93:
78:
3785:
3355:
3044:
2964:
2349:
511:
441:
7138:
6837:
6827:
6781:
6764:
6719:
6681:
6583:
6503:
6310:
6237:
6210:
6198:
6104:
6018:
5992:
5947:
5915:
5716:
5518:
5461:
5411:
5376:
5334:
5022:
4504:
3390:
The final axiom schemas are required to work with formulas involving the equality symbol.
2289:
1129:
722:
222:
7166:
5152:
It describes (among others) a specific Hilbert-style proof system (that is restricted to
3397:
7108:
6822:
6801:
6759:
6739:
6634:
6087:
6077:
6067:
6062:
5996:
5870:
5746:
5635:
5630:
5608:
5209:
5072:
4965:
3761:
3024:
66:
2610:{\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}
185:
Most variants of Hilbert systems take a characteristic tack in the way they balance a
7201:
6975:
6796:
6474:
5981:
5766:
5756:
5726:
5711:
5381:
5056:
5015:
4873:
3779:
2633:
1605:
1377:
714:
710:
692:
190:
74:
70:
5133:"A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness"
4529:
4278:"A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness"
1635:
Systems for propositional logic whose inference rules are schematic are also called
7002:
6965:
6696:
6543:
6444:
6436:
6316:
6264:
6173:
6109:
6092:
6023:
5882:
5741:
5443:
5226:
2119:
1636:
677:
556:
405:
353:
210:
198:
89:
63:
35:
7171:
4840:
4820:
4790:
4735:
4699:
4672:
4610:
4583:
4250:
4218:
857:{\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}
7090:
7070:
7012:
6806:
6686:
5865:
5855:
5802:
5486:
5406:
5391:
5271:
5216:
4964:
Pudlák, Pavel; Buss, Samuel R. (1995). Pacholski, Leszek; Tiuryn, Jerzy (eds.).
4093:
3528:
2204:
278:
226:
7045:
7027:
5736:
5591:
5562:
5368:
409:
4925:
4647:
4480:
4154:
Because Hilbert systems have very few deduction rules, it is common to prove
244:
A characteristic feature of the many variants of Hilbert systems is that the
6888:
6791:
5844:
5761:
5721:
5685:
5621:
5433:
5423:
5396:
186:
3376:
These three additional rules extend the propositional system to axiomatise
2620:
The axiom P1 is redundant, as it follows from P3, P2 and modus ponens (see
197:. Hilbert systems can be characterised by the choice of a large number of
6873:
6671:
6119:
5824:
5418:
5074:
From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931
1597:
731:
6469:
5261:
4977:
2047:{\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}
713:
proof system that thereby qualifies as a Hilbert system dates back to
5078:(3rd printing 1976 ed.). Cambridge MA: Harvard University Press.
3751:{\displaystyle \forall x(\phi \to \psi )\to \exists x(\phi )\to \psi }
3021:
be a formula with one or more instances of the propositional variable
1181:{\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)}
933:{\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}
5159:
696:
4917:
1578:{\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}
551:
Hilbert systems are characterized by the use of numerous schemas of
4769:(Fall 2023 ed.), Metaphysics Research Lab, Stanford University
2636:
is achieved either by adding instead the axiom P4m, or by defining
1188:. Hence, Łukasiewicz is credited with this system of three axioms:
7151:
6013:
5359:
5204:
31:
4304:
Benthem, Johan van; Gupta, Amitabha; Parikh, Rohit (2011-04-02).
4943:(Extended ed.). New Jersey: World Scientific. p. 126.
2820:{\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }
718:
691:
Axiomatic proofs have been used in mathematics since the famous
6921:
5163:
3508:{\displaystyle \left(x=y\right)\to \left(\phi \to \phi \right)}
560:
zero or more universal quantifiers on the formula; for example
4087:
3522:
2198:
734:
as connectives, and it had six axioms, which were these ones:
668:
The following are some Hilbert systems that have been used in
272:
248:
is not changed in any of their rules of inference, while both
1617:
338:
100:
systems, in which no axioms are used, only inference rules.
1815:{\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}
3854:{\displaystyle \alpha \to (\beta \to \alpha \land \beta )}
2954:{\displaystyle \left(p\to q\right)\to \left(p\to q\right)}
2867:{\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}
991:{\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}
1309:{\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}
4902:"The relative efficiency of propositional proof systems"
4198:
4196:
2190: (from (4) and (3) by modus ponens)
4704:. Springer Science & Business Media. p. 201.
4615:. Springer Science & Business Media. p. 113.
4364:. Springer Science & Business Media. p. 113.
4307:
Proof, Computation and Agency: Logic at the Crossroads
4412:
4410:
4408:
4310:. Springer Science & Business Media. p. 41.
4012:
3978:
3944:
3903:
3869:
3823:
3788:
3764:
3702:
3629:
3433:
3400:
3358:
3314:
3220:
3196:
3133:
3096:
3067:
3047:
3027:
2998:
2967:
2909:
2883:
2835:
2785:
2695:
2665:
2642:
2559:
2451:
2407:
2379:
2366:, without enlarging the class of deducible formulas.
2352:
2332:
2312:
2292:
2272:
2170:
2130:
2062:
1950:
1898:
1830:
1736:
1690:
1656:
1614:
1535:
1448:
1409:
1323:
1236:
1197:
1138:
1090:
1040:
1006:
948:
872:
784:
744:
622:
566:
534:
514:
488:
468:
444:
418:
390:
366:
143:
118:
3681:{\displaystyle \forall x(\phi \to \exists y(\phi ))}
3341:{\displaystyle \phi \to \forall x\left(\phi \right)}
3175:{\displaystyle \forall x\left(\phi \right)\to \phi }
2436:{\displaystyle \phi \to \left(\psi \to \phi \right)}
7137:
7089:
7026:
6956:
6815:
6710:
6542:
6435:
6287:
5980:
5903:
5797:
5701:
5590:
5517:
5452:
5367:
5358:
5280:
5197:
5021:. Graduate Texts in Mathematics. Berlin, New York:
4585:
A Philosophical Introduction to Higher-order Logics
4334:
A Philosophical Introduction to Higher-order Logics
1680:is given below. First, the axioms are given names:
108:defines a "Hilbert system" as a system with axioms
5071:
5014:
4072:
3996:
3962:
3921:
3887:
3853:
3794:
3770:
3750:
3680:
3507:
3412:
3364:
3340:
3298:
3204:
3174:
3111:
3082:
3053:
3033:
3013:
2973:
2953:
2895:
2866:
2819:
2761:
2677:
2651:
2609:
2543:
2435:
2391:
2358:
2338:
2318:
2298:
2278:
2182:
2154:
2110:
2046:
1934:
1878:
1814:
1720:
1668:
1624:
1577:
1520:
1433:
1365:
1308:
1221:
1180:
1120:
1058:
1024:
990:
932:
856:
768:
652:
608:
540:
520:
500:
474:
450:
430:
396:
372:
154:
129:
3198:
217: – or two – with
1879:{\displaystyle ((\neg p\to \neg q)\to (q\to p))}
343:A graphic representation of the deduction system
85:, but are of interest for other logics as well.
4698:Gabbay, Dov M.; Guenthner, Franz (2013-03-14).
3888:{\displaystyle \alpha \wedge \beta \to \alpha }
1434:{\displaystyle \varphi \to (\psi \to \varphi )}
438:means that there is a deduction that ends with
3922:{\displaystyle \alpha \wedge \beta \to \beta }
1366:{\displaystyle (\neg p\to \neg q)\to (q\to p)}
609:{\displaystyle \forall y(\forall xPxy\to Pty)}
6933:
5175:
4900:Cook, Stephen A.; Reckhow, Robert A. (1979).
4765:, in Zalta, Edward N.; Nodelman, Uri (eds.),
4636:Troelstra, A. S.; Schwichtenberg, H. (2000).
4469:Troelstra, A. S.; Schwichtenberg, H. (2000).
3963:{\displaystyle \alpha \to \alpha \vee \beta }
3593:. Given these axioms, it is possible to form
8:
3997:{\displaystyle \beta \to \alpha \vee \beta }
4845:. Princeton University Press. p. 119.
4795:. Cambridge University Press. p. 185.
4122:. Unsourced material may be challenged and
3557:. Unsourced material may be challenged and
2233:. Unsourced material may be challenged and
2111:{\displaystyle (A\to (B\to A))\to (A\to A)}
307:. Unsourced material may be challenged and
6940:
6926:
6918:
6001:
5596:
5364:
5182:
5168:
5160:
4391:. Cambridge University Press. p. 19.
4223:. Cambridge University Press. p. 10.
2118: (from (1) and (2) by
4740:. Courier Corporation. pp. 102–103.
4142:Learn how and when to remove this message
4011:
3977:
3943:
3902:
3868:
3822:
3787:
3763:
3701:
3628:
3577:Learn how and when to remove this message
3432:
3399:
3357:
3313:
3219:
3197:
3195:
3132:
3095:
3066:
3046:
3026:
2997:
2966:
2908:
2882:
2834:
2784:
2694:
2664:
2641:
2558:
2450:
2406:
2378:
2351:
2331:
2311:
2291:
2271:
2253:Learn how and when to remove this message
2169:
2129:
2061:
1949:
1897:
1829:
1735:
1689:
1655:
1616:
1615:
1613:
1534:
1447:
1408:
1322:
1235:
1196:
1137:
1089:
1039:
1005:
947:
871:
783:
743:
673:
621:
565:
533:
528:is provable assuming all the formulas in
513:
487:
467:
443:
417:
389:
365:
327:Learn how and when to remove this message
168:
144:
142:
119:
117:
5008:. Vol. 1. Amsterdam: North Holland.
4737:A Beginner's Guide to Mathematical Logic
3933:Disjunction introduction and elimination
3812:Conjunction introduction and elimination
2621:
5044:(in Hungarian). Budapest: Osiris Kiadó.
5004:Curry, Haskell B.; Robert Feys (1958).
4874:"Proof Explorer - Home Page - Metamath"
4767:The Stanford Encyclopedia of Philosophy
4252:An Introduction to Substructural Logics
4192:
2162: (instance of (A1))
2054: (instance of (A2))
1942: (instance of (A1))
4895:
4893:
4868:
4866:
4864:
4862:
4834:
4832:
4814:
4812:
4784:
4782:
4729:
4727:
4725:
4723:
4721:
4972:. Berlin, Heidelberg: Springer: 152.
4789:Mendelsohn, Richard L. (2005-01-10).
4588:. Taylor & Francis. p. 424.
4337:. Taylor & Francis. p. 424.
1128:". Which, taken out of Łukasiewicz's
769:{\displaystyle a\supset (b\supset a)}
201:of logical axioms and a small set of
7:
4244:
4242:
4240:
4212:
4210:
4208:
4120:adding citations to reliable sources
3555:adding citations to reliable sources
2231:adding citations to reliable sources
1935:{\displaystyle A\to ((B\to A)\to A)}
1380:, who referred to it as the system P
1059:{\displaystyle a\supset \neg \neg a}
1025:{\displaystyle \neg \neg a\supset a}
380:is a set of formulas, considered as
305:adding citations to reliable sources
5053:(in Hungarian). Budapest: Gondolat.
4734:Smullyan, Raymond M. (2014-07-23).
4505:"Introduction to Logic - Chapter 4"
4220:An Introduction to Gödel's Theorems
653:{\displaystyle \forall xPxy\to Pty}
501:{\displaystyle \Gamma \vdash \phi }
431:{\displaystyle \Gamma \vdash \phi }
27:System of formal deduction in logic
5040:Ruzsa, Imre; Máté, András (1997).
4941:Introduction to mathematical logic
4842:Introduction to Mathematical Logic
3727:
3703:
3645:
3630:
3321:
3274:
3254:
3221:
3134:
2836:
2811:
2797:
2748:
2734:
2672:
2643:
2574:
2565:
2313:
2273:
1846:
1837:
1548:
1539:
1336:
1327:
1151:
1142:
1050:
1047:
1010:
1007:
979:
970:
623:
576:
567:
535:
489:
469:
419:
391:
367:
145:
25:
7018:List of mathematical logic topics
5055:It is a Hungarian translation of
4674:Proof Theory and Algebra in Logic
4558:Proof Theory and Algebra in Logic
6901:
4092:
3527:
2203:
2195:Predicate logic (example system)
277:
179:Principles of Mathematical Logic
5101:Introduction to Metamathematics
4822:Jan Lukasiewicz: Selected Works
4792:The Philosophy of Gottlob Frege
4701:Handbook of Philosophical Logic
3061:be another formula. Then from
1721:{\displaystyle (p\to (q\to p))}
683:
130:{\displaystyle {\rightarrow }E}
7187:List of category theory topics
4534:. Elsevier. pp. 552–553.
4067:
4061:
4049:
4046:
4040:
4034:
4031:
4028:
4025:
4019:
4013:
3982:
3948:
3913:
3879:
3848:
3836:
3830:
3827:
3742:
3739:
3733:
3724:
3721:
3715:
3709:
3675:
3672:
3669:
3657:
3651:
3642:
3636:
3497:
3485:
3479:
3476:
3464:
3453:
3382:intuitionistic predicate logic
3318:
3271:
3246:
3235:
3169:
3157:
3151:
3106:
3100:
3077:
3071:
3008:
3002:
2940:
2929:
2918:
2887:
2853:
2842:
2808:
2794:
2745:
2731:
2715:
2704:
2678:{\displaystyle \phi \to \bot }
2669:
2596:
2585:
2571:
2525:
2514:
2503:
2487:
2471:
2460:
2422:
2411:
2392:{\displaystyle \phi \to \phi }
2383:
2293:
2174:
2149:
2143:
2137:
2134:
2105:
2099:
2093:
2090:
2087:
2084:
2078:
2072:
2069:
2063:
2041:
2038:
2032:
2026:
2023:
2020:
2017:
2011:
2005:
2002:
1996:
1993:
1990:
1987:
1984:
1978:
1975:
1969:
1963:
1960:
1957:
1951:
1929:
1923:
1920:
1914:
1908:
1905:
1902:
1873:
1870:
1864:
1858:
1855:
1852:
1843:
1834:
1831:
1809:
1806:
1803:
1797:
1791:
1788:
1785:
1779:
1773:
1770:
1767:
1764:
1761:
1755:
1749:
1746:
1740:
1737:
1715:
1712:
1706:
1700:
1697:
1691:
1660:
1625:{\displaystyle {\mathcal {H}}}
1572:
1566:
1560:
1557:
1554:
1545:
1536:
1515:
1512:
1506:
1500:
1497:
1494:
1488:
1482:
1479:
1476:
1473:
1470:
1464:
1458:
1455:
1449:
1428:
1422:
1416:
1413:
1360:
1354:
1348:
1345:
1342:
1333:
1324:
1303:
1300:
1294:
1288:
1285:
1282:
1276:
1270:
1267:
1264:
1261:
1258:
1252:
1246:
1243:
1237:
1216:
1210:
1204:
1201:
1175:
1169:
1163:
1160:
1157:
1148:
1139:
985:
967:
961:
949:
927:
924:
912:
903:
897:
894:
882:
873:
851:
848:
836:
830:
818:
815:
809:
806:
794:
785:
763:
751:
638:
603:
591:
573:
120:
60:Hilbert–Ackermann system
56:Hilbert-style deductive system
18:Hilbert-style deductive system
1:
6862:History of mathematical logic
5099:Kleene, Stephen Cole (1952).
5070:van Heijenoort, Jean (1967).
4906:The Journal of Symbolic Logic
4825:. North-Holland. p. 136.
4671:Ono, Hiroakira (2019-08-02).
4609:Eijck, Jan van (1991-02-26).
4555:Ono, Hiroakira (2019-08-02).
4358:Eijck, Jan van (1991-02-26).
4255:. Routledge. pp. 73–74.
2626:classical propositional logic
2155:{\displaystyle A\to (B\to A)}
1889:And the proof is as follows:
1222:{\displaystyle p\to (q\to p)}
706:
404:could be a set of axioms for
92:. Every Hilbert system is an
6787:Primitive recursive function
4582:Bacon, Andrew (2023-09-29).
4445:A Treatise on Time and Space
4331:Bacon, Andrew (2023-09-29).
4249:Restall, Greg (2002-09-11).
3112:{\displaystyle \phi (\psi )}
2630:positive implicational logic
1604:has also been attributed to
1400:), the axioms are given as:
1132:into modern notation, means
709:300 BC. But the first known
7182:Glossary of category theory
7056:Zermelo–Fraenkel set theory
7008:Mathematical constructivism
5042:Bevezetés a modern logikába
4442:Lucas, J. R. (2018-10-10).
4385:Haack, Susan (1978-07-27).
4217:Smith, Peter (2013-02-21).
3807:Conjunction and disjunction
2652:{\displaystyle \lnot \phi }
726:. Frege's system used only
674:§ Schematic form of P2
233:, additionally require the
169:§ Schematic form of P2
155:{\displaystyle {\forall }I}
81:are most often studied for
7234:
7177:Mathematical structuralism
7114:Intuitionistic type theory
6950:Foundations of Mathematics
5851:Schröder–Bernstein theorem
5578:Monadic predicate calculus
5237:Foundations of mathematics
4528:Buss, S. R. (1998-07-09).
4448:. Routledge. p. 152.
4158:that show that additional
3614:Existential quantification
2628:; without axiom P4 we get
2624:). These axioms describe
1650:As an example, a proof of
1588:The schematic version of P
1384:and helped popularize it.
52:Hilbert-style proof system
7218:Automated theorem proving
7081:List of set theory topics
6897:
6884:Philosophy of mathematics
6833:Automated theorem proving
6004:
5958:Von Neumann–Bernays–Gödel
5599:
4819:Łukasiewicz, Jan (1970).
4202:Máté & Ruzsa 1997:129
3378:classical predicate logic
3205:{\displaystyle \,\!\phi }
1121:{\displaystyle CCNpNqCqp}
5061:semantic theory of truth
5013:Monk, J. Donald (1976).
5006:Combinatory Logic Vol. I
4939:Walicki, Michał (2017).
4648:10.1017/cbo9781139168717
4531:Handbook of Proof Theory
4481:10.1017/cbo9781139168717
3083:{\displaystyle \phi (p)}
3014:{\displaystyle \phi (p)}
2903:, or it might represent
2319:{\displaystyle \forall }
2306:and only the quantifier
7061:Constructive set theory
6534:Self-verifying theories
6355:Tarski's axiomatization
5306:Tarski's undefinability
5301:incompleteness theorems
5049:Tarski, Alfred (1990).
4839:Church, Alonzo (1996).
4761:Franks, Curtis (2023),
4677:. Springer. p. 5.
4561:. Springer. p. 5.
4509:intrologic.stanford.edu
4417:Bostock, David (1997).
4172:List of Hilbert systems
3595:conservative extensions
3591:functional completeness
3519:Conservative extensions
3186:may be substituted for
676:, is also considered a
616:is a generalization of
541:{\displaystyle \Gamma }
475:{\displaystyle \Gamma }
397:{\displaystyle \Gamma }
373:{\displaystyle \Gamma }
347:In a Hilbert system, a
7162:Higher category theory
7066:Descriptive set theory
6971:Mathematical induction
6908:Mathematics portal
6519:Proof of impossibility
6167:propositional variable
5477:Propositional calculus
5154:propositional calculus
5059:'s selected papers on
4970:Computer Science Logic
4276:Gaifman, Haim (2002).
4074:
3998:
3964:
3923:
3889:
3855:
3796:
3772:
3752:
3682:
3509:
3414:
3366:
3342:
3300:
3206:
3176:
3113:
3084:
3055:
3035:
3015:
2984:With a second rule of
2975:
2955:
2897:
2896:{\displaystyle p\to p}
2868:
2821:
2763:
2679:
2653:
2611:
2545:
2437:
2393:
2360:
2340:
2339:{\displaystyle \land }
2320:
2300:
2280:
2279:{\displaystyle \lnot }
2184:
2183:{\displaystyle A\to A}
2156:
2112:
2048:
1936:
1880:
1816:
1722:
1670:
1669:{\displaystyle A\to A}
1626:
1579:
1522:
1435:
1367:
1310:
1223:
1182:
1122:
1060:
1026:
992:
934:
858:
770:
654:
610:
542:
522:
502:
476:
452:
432:
398:
374:
344:
156:
131:
7124:Univalent foundations
7109:Dependent type theory
7099:Axiom of reducibility
6777:Kolmogorov complexity
6730:Computably enumerable
6630:Model complete theory
6422:Principia Mathematica
5482:Propositional formula
5311:Banach–Tarski paradox
5145:"Propositional logic"
5051:Bizonyítás és igazság
4763:"Propositional Logic"
4075:
3999:
3965:
3924:
3890:
3856:
3797:
3795:{\displaystyle \psi }
3773:
3753:
3683:
3510:
3415:
3367:
3365:{\displaystyle \phi }
3343:
3301:
3207:
3177:
3114:
3085:
3056:
3054:{\displaystyle \psi }
3036:
3016:
2976:
2974:{\displaystyle \phi }
2956:
2898:
2869:
2822:
2764:
2680:
2654:
2612:
2546:
2438:
2394:
2361:
2359:{\displaystyle \lor }
2341:
2321:
2301:
2281:
2185:
2157:
2113:
2049:
1937:
1881:
1817:
1723:
1671:
1627:
1596:, and is used in the
1580:
1523:
1436:
1368:
1311:
1224:
1183:
1123:
1061:
1027:
993:
935:
859:
771:
655:
611:
543:
523:
521:{\displaystyle \phi }
503:
477:
458:using as axioms only
453:
451:{\displaystyle \phi }
433:
399:
375:
342:
231:Hilbert-Lewis systems
157:
132:
7119:Homotopy type theory
7046:Axiomatic set theory
6725:Church–Turing thesis
6712:Computability theory
5921:continuum hypothesis
5439:Square of opposition
5297:Gödel's completeness
4388:Philosophy of Logics
4116:improve this section
4010:
3976:
3972:introduction right:
3942:
3901:
3867:
3821:
3786:
3762:
3700:
3627:
3603:logically equivalent
3551:improve this section
3431:
3398:
3356:
3312:
3218:
3194:
3131:
3094:
3065:
3045:
3025:
2996:
2986:uniform substitution
2965:
2907:
2881:
2833:
2783:
2773:Intuitionistic logic
2693:
2663:
2640:
2557:
2449:
2405:
2377:
2350:
2330:
2310:
2299:{\displaystyle \to }
2290:
2270:
2227:improve this section
2168:
2128:
2060:
1948:
1896:
1828:
1734:
1688:
1654:
1612:
1533:
1446:
1407:
1398:well-formed formulas
1321:
1234:
1195:
1136:
1088:
1038:
1004:
946:
870:
782:
742:
702:Elements of Geometry
620:
564:
532:
512:
486:
482:. Thus, informally,
466:
442:
416:
388:
364:
301:improve this section
239:uniform substitution
215:propositional logics
141:
116:
48:Hilbert-style system
34:, more specifically
6879:Mathematical object
6770:P versus NP problem
6735:Computable function
6529:Reverse mathematics
6455:Logical consequence
6332:primitive recursive
6327:elementary function
6100:Free/bound variable
5953:Tarski–Grothendieck
5472:Logical connectives
5402:Logical equivalence
5252:Logical consequence
3938:introduction left:
3897:elimination right:
3420:for every variable
3413:{\displaystyle x=x}
1388:Schematic form of P
672:. One of them, the
670:propositional logic
664:Propositional logic
229:, sometimes called
42:, sometimes called
7104:Simple type theory
7051:Zermelo set theory
6998:Mathematical proof
6958:Mathematical logic
6677:Transfer principle
6640:Semantics of logic
6625:Categorical theory
6601:Non-standard model
6115:Logical connective
5242:Information theory
5191:Mathematical logic
5017:Mathematical Logic
4978:10.1007/BFb0022253
4639:Basic Proof Theory
4472:Basic Proof Theory
4419:Intermediate logic
4070:
3994:
3960:
3919:
3885:
3863:elimination left:
3851:
3792:
3768:
3748:
3678:
3505:
3410:
3362:
3338:
3296:
3202:
3172:
3109:
3080:
3051:
3031:
3011:
2971:
2951:
2893:
2864:
2817:
2759:
2675:
2649:
2607:
2541:
2433:
2389:
2356:
2336:
2316:
2296:
2276:
2180:
2152:
2108:
2044:
1932:
1876:
1812:
1718:
1666:
1643:Proof example in P
1622:
1575:
1518:
1431:
1363:
1306:
1219:
1178:
1118:
1073:
1056:
1022:
988:
930:
854:
766:
650:
606:
538:
518:
498:
472:
448:
428:
394:
370:
345:
241:rule is required.
235:necessitation rule
203:rules of inference
195:rules of inference
152:
127:
7195:
7194:
7076:Russell's paradox
6991:Natural deduction
6915:
6914:
6847:Abstract category
6650:Theories of truth
6460:Rule of inference
6450:Natural deduction
6431:
6430:
5976:
5975:
5681:Cartesian product
5586:
5585:
5492:Many-valued logic
5467:Boolean functions
5350:Russell's paradox
5325:diagonal argument
5222:First-order logic
5032:978-0-387-90170-1
4987:978-3-540-49404-1
4950:978-981-4719-95-7
4852:978-0-691-02906-1
4802:978-1-139-44403-3
4747:978-0-486-49237-7
4711:978-94-017-0458-8
4684:978-981-13-7997-0
4657:978-0-521-77911-1
4622:978-3-540-53686-4
4595:978-1-000-92575-3
4568:978-981-13-7997-0
4541:978-0-08-053318-6
4490:978-0-521-77911-1
4455:978-0-429-68517-0
4428:978-0-19-875141-0
4398:978-0-521-29329-7
4371:978-3-540-53686-4
4344:978-1-000-92575-3
4317:978-94-007-0080-2
4262:978-1-135-11131-1
4230:978-1-107-02284-3
4177:Natural deduction
4152:
4151:
4144:
3771:{\displaystyle x}
3608:natural deduction
3599:deduction theorem
3587:
3586:
3579:
3034:{\displaystyle p}
2263:
2262:
2255:
1632:in this context.
1592:is attributed to
337:
336:
329:
269:Formal deductions
250:natural deduction
207:natural deduction
98:natural deduction
83:first-order logic
79:deductive systems
16:(Redirected from
7225:
7157:Category of sets
7129:Girard's paradox
7041:Naive set theory
6981:Axiomatic system
6948:Major topics in
6942:
6935:
6928:
6919:
6906:
6905:
6857:History of logic
6852:Category of sets
6745:Decision problem
6524:Ordinal analysis
6465:Sequent calculus
6363:Boolean algebras
6303:
6302:
6277:
6248:logical/constant
6002:
5988:
5911:Zermelo–Fraenkel
5662:Set operations:
5597:
5534:
5365:
5345:Löwenheim–Skolem
5232:Formal semantics
5184:
5177:
5170:
5161:
5151:
5149:
5139:
5137:
5114:
5089:
5077:
5054:
5045:
5036:
5020:
5009:
4992:
4991:
4961:
4955:
4954:
4936:
4930:
4929:
4897:
4888:
4887:
4885:
4884:
4870:
4857:
4856:
4836:
4827:
4826:
4816:
4807:
4806:
4786:
4777:
4776:
4775:
4774:
4758:
4752:
4751:
4731:
4716:
4715:
4695:
4689:
4688:
4668:
4662:
4661:
4633:
4627:
4626:
4606:
4600:
4599:
4579:
4573:
4572:
4552:
4546:
4545:
4525:
4519:
4518:
4516:
4515:
4501:
4495:
4494:
4466:
4460:
4459:
4439:
4433:
4432:
4414:
4403:
4402:
4382:
4376:
4375:
4355:
4349:
4348:
4328:
4322:
4321:
4301:
4295:
4294:
4292:
4291:
4282:
4273:
4267:
4266:
4246:
4235:
4234:
4214:
4203:
4200:
4182:Sequent calculus
4147:
4140:
4136:
4133:
4127:
4096:
4088:
4079:
4077:
4076:
4071:
4003:
4001:
4000:
3995:
3969:
3967:
3966:
3961:
3928:
3926:
3925:
3920:
3894:
3892:
3891:
3886:
3860:
3858:
3857:
3852:
3801:
3799:
3798:
3793:
3777:
3775:
3774:
3769:
3757:
3755:
3754:
3749:
3687:
3685:
3684:
3679:
3582:
3575:
3571:
3568:
3562:
3531:
3523:
3514:
3512:
3511:
3506:
3504:
3500:
3452:
3448:
3419:
3417:
3416:
3411:
3371:
3369:
3368:
3363:
3347:
3345:
3344:
3339:
3337:
3305:
3303:
3302:
3297:
3295:
3291:
3290:
3270:
3245:
3241:
3211:
3209:
3208:
3203:
3181:
3179:
3178:
3173:
3150:
3118:
3116:
3115:
3110:
3089:
3087:
3086:
3081:
3060:
3058:
3057:
3052:
3040:
3038:
3037:
3032:
3020:
3018:
3017:
3012:
2980:
2978:
2977:
2972:
2960:
2958:
2957:
2952:
2950:
2946:
2928:
2924:
2902:
2900:
2899:
2894:
2873:
2871:
2870:
2865:
2863:
2859:
2826:
2824:
2823:
2818:
2807:
2803:
2768:
2766:
2765:
2760:
2758:
2754:
2744:
2740:
2714:
2710:
2684:
2682:
2681:
2676:
2658:
2656:
2655:
2650:
2616:
2614:
2613:
2608:
2606:
2602:
2584:
2580:
2550:
2548:
2547:
2542:
2540:
2536:
2535:
2531:
2513:
2509:
2486:
2482:
2481:
2477:
2442:
2440:
2439:
2434:
2432:
2428:
2398:
2396:
2395:
2390:
2365:
2363:
2362:
2357:
2345:
2343:
2342:
2337:
2325:
2323:
2322:
2317:
2305:
2303:
2302:
2297:
2285:
2283:
2282:
2277:
2258:
2251:
2247:
2244:
2238:
2207:
2199:
2189:
2187:
2186:
2181:
2161:
2159:
2158:
2153:
2117:
2115:
2114:
2109:
2053:
2051:
2050:
2045:
1941:
1939:
1938:
1933:
1885:
1883:
1882:
1877:
1821:
1819:
1818:
1813:
1727:
1725:
1724:
1719:
1675:
1673:
1672:
1667:
1631:
1629:
1628:
1623:
1621:
1620:
1594:John von Neumann
1584:
1582:
1581:
1576:
1527:
1525:
1524:
1519:
1440:
1438:
1437:
1432:
1372:
1370:
1369:
1364:
1315:
1313:
1312:
1307:
1228:
1226:
1225:
1220:
1187:
1185:
1184:
1179:
1127:
1125:
1124:
1119:
1065:
1063:
1062:
1057:
1034:Proposition 41:
1031:
1029:
1028:
1023:
1000:Proposition 31:
997:
995:
994:
989:
942:Proposition 28:
939:
937:
936:
931:
863:
861:
860:
855:
775:
773:
772:
767:
711:fully formalized
708:
659:
657:
656:
651:
615:
613:
612:
607:
547:
545:
544:
539:
527:
525:
524:
519:
507:
505:
504:
499:
481:
479:
478:
473:
462:and elements of
457:
455:
454:
449:
437:
435:
434:
429:
403:
401:
400:
395:
379:
377:
376:
371:
349:formal deduction
332:
325:
321:
318:
312:
281:
273:
265:of tautologies.
254:sequent calculus
223:predicate logics
167:form, as in the
161:
159:
158:
153:
148:
136:
134:
133:
128:
123:
94:axiomatic system
44:Hilbert calculus
21:
7233:
7232:
7228:
7227:
7226:
7224:
7223:
7222:
7213:Logical calculi
7198:
7197:
7196:
7191:
7139:Category theory
7133:
7085:
7022:
6952:
6946:
6916:
6911:
6900:
6893:
6838:Category theory
6828:Algebraic logic
6811:
6782:Lambda calculus
6720:Church encoding
6706:
6682:Truth predicate
6538:
6504:Complete theory
6427:
6296:
6292:
6288:
6283:
6275:
5995: and
5991:
5986:
5972:
5948:New Foundations
5916:axiom of choice
5899:
5861:Gödel numbering
5801: and
5793:
5697:
5582:
5532:
5513:
5462:Boolean algebra
5448:
5412:Equiconsistency
5377:Classical logic
5354:
5335:Halting problem
5323: and
5299: and
5287: and
5286:
5281:Theorems (
5276:
5193:
5188:
5147:
5142:
5135:
5131:Gaifman, Haim.
5130:
5127:
5111:
5098:
5086:
5069:
5048:
5039:
5033:
5023:Springer-Verlag
5012:
5003:
5000:
4995:
4988:
4963:
4962:
4958:
4951:
4938:
4937:
4933:
4918:10.2307/2273702
4899:
4898:
4891:
4882:
4880:
4878:us.metamath.org
4872:
4871:
4860:
4853:
4838:
4837:
4830:
4818:
4817:
4810:
4803:
4788:
4787:
4780:
4772:
4770:
4760:
4759:
4755:
4748:
4733:
4732:
4719:
4712:
4697:
4696:
4692:
4685:
4670:
4669:
4665:
4658:
4635:
4634:
4630:
4623:
4608:
4607:
4603:
4596:
4581:
4580:
4576:
4569:
4554:
4553:
4549:
4542:
4527:
4526:
4522:
4513:
4511:
4503:
4502:
4498:
4491:
4468:
4467:
4463:
4456:
4441:
4440:
4436:
4429:
4416:
4415:
4406:
4399:
4384:
4383:
4379:
4372:
4357:
4356:
4352:
4345:
4330:
4329:
4325:
4318:
4303:
4302:
4298:
4289:
4287:
4280:
4275:
4274:
4270:
4263:
4248:
4247:
4238:
4231:
4216:
4215:
4206:
4201:
4194:
4190:
4168:
4160:deduction rules
4148:
4137:
4131:
4128:
4113:
4097:
4086:
4008:
4007:
3974:
3973:
3940:
3939:
3899:
3898:
3865:
3864:
3819:
3818:
3809:
3784:
3783:
3760:
3759:
3698:
3697:
3625:
3624:
3616:
3583:
3572:
3566:
3563:
3548:
3532:
3521:
3460:
3456:
3438:
3434:
3429:
3428:
3396:
3395:
3354:
3353:
3352:is not free in
3327:
3310:
3309:
3280:
3260:
3253:
3249:
3231:
3227:
3216:
3215:
3192:
3191:
3140:
3129:
3128:
3092:
3091:
3063:
3062:
3043:
3042:
3023:
3022:
2994:
2993:
2963:
2962:
2936:
2932:
2914:
2910:
2905:
2904:
2879:
2878:
2849:
2845:
2831:
2830:
2790:
2786:
2781:
2780:
2727:
2723:
2722:
2718:
2700:
2696:
2691:
2690:
2661:
2660:
2638:
2637:
2592:
2588:
2564:
2560:
2555:
2554:
2521:
2517:
2499:
2495:
2494:
2490:
2467:
2463:
2456:
2452:
2447:
2446:
2418:
2414:
2403:
2402:
2375:
2374:
2348:
2347:
2328:
2327:
2308:
2307:
2288:
2287:
2268:
2267:
2259:
2248:
2242:
2239:
2224:
2208:
2197:
2166:
2165:
2126:
2125:
2058:
2057:
1946:
1945:
1894:
1893:
1826:
1825:
1732:
1731:
1686:
1685:
1679:
1652:
1651:
1648:
1646:
1610:
1609:
1603:
1591:
1531:
1530:
1444:
1443:
1405:
1404:
1393:
1391:
1383:
1319:
1318:
1232:
1231:
1193:
1192:
1134:
1133:
1130:Polish notation
1086:
1085:
1082:Jan Łukasiewicz
1079:
1077:
1074:Łukasiewicz's P
1036:
1035:
1002:
1001:
944:
943:
868:
867:
866:Proposition 8:
780:
779:
778:Proposition 2:
740:
739:
738:Proposition 1:
723:Begriffsschrift
689:
686:Begriffsschrift
666:
618:
617:
562:
561:
530:
529:
510:
509:
484:
483:
464:
463:
440:
439:
414:
413:
412:. The notation
386:
385:
384:. For example,
362:
361:
333:
322:
316:
313:
298:
282:
271:
139:
138:
114:
113:
62:, is a type of
28:
23:
22:
15:
12:
11:
5:
7231:
7229:
7221:
7220:
7215:
7210:
7200:
7199:
7193:
7192:
7190:
7189:
7184:
7179:
7174:
7172:∞-topos theory
7169:
7164:
7159:
7154:
7149:
7143:
7141:
7135:
7134:
7132:
7131:
7126:
7121:
7116:
7111:
7106:
7101:
7095:
7093:
7087:
7086:
7084:
7083:
7078:
7073:
7068:
7063:
7058:
7053:
7048:
7043:
7038:
7032:
7030:
7024:
7023:
7021:
7020:
7015:
7010:
7005:
7000:
6995:
6994:
6993:
6988:
6986:Hilbert system
6983:
6973:
6968:
6962:
6960:
6954:
6953:
6947:
6945:
6944:
6937:
6930:
6922:
6913:
6912:
6898:
6895:
6894:
6892:
6891:
6886:
6881:
6876:
6871:
6870:
6869:
6859:
6854:
6849:
6840:
6835:
6830:
6825:
6823:Abstract logic
6819:
6817:
6813:
6812:
6810:
6809:
6804:
6802:Turing machine
6799:
6794:
6789:
6784:
6779:
6774:
6773:
6772:
6767:
6762:
6757:
6752:
6742:
6740:Computable set
6737:
6732:
6727:
6722:
6716:
6714:
6708:
6707:
6705:
6704:
6699:
6694:
6689:
6684:
6679:
6674:
6669:
6668:
6667:
6662:
6657:
6647:
6642:
6637:
6635:Satisfiability
6632:
6627:
6622:
6621:
6620:
6610:
6609:
6608:
6598:
6597:
6596:
6591:
6586:
6581:
6576:
6566:
6565:
6564:
6559:
6552:Interpretation
6548:
6546:
6540:
6539:
6537:
6536:
6531:
6526:
6521:
6516:
6506:
6501:
6500:
6499:
6498:
6497:
6487:
6482:
6472:
6467:
6462:
6457:
6452:
6447:
6441:
6439:
6433:
6432:
6429:
6428:
6426:
6425:
6417:
6416:
6415:
6414:
6409:
6408:
6407:
6402:
6397:
6377:
6376:
6375:
6373:minimal axioms
6370:
6359:
6358:
6357:
6346:
6345:
6344:
6339:
6334:
6329:
6324:
6319:
6306:
6304:
6285:
6284:
6282:
6281:
6280:
6279:
6267:
6262:
6261:
6260:
6255:
6250:
6245:
6235:
6230:
6225:
6220:
6219:
6218:
6213:
6203:
6202:
6201:
6196:
6191:
6186:
6176:
6171:
6170:
6169:
6164:
6159:
6149:
6148:
6147:
6142:
6137:
6132:
6127:
6122:
6112:
6107:
6102:
6097:
6096:
6095:
6090:
6085:
6080:
6070:
6065:
6063:Formation rule
6060:
6055:
6054:
6053:
6048:
6038:
6037:
6036:
6026:
6021:
6016:
6011:
6005:
5999:
5982:Formal systems
5978:
5977:
5974:
5973:
5971:
5970:
5965:
5960:
5955:
5950:
5945:
5940:
5935:
5930:
5925:
5924:
5923:
5918:
5907:
5905:
5901:
5900:
5898:
5897:
5896:
5895:
5885:
5880:
5879:
5878:
5871:Large cardinal
5868:
5863:
5858:
5853:
5848:
5834:
5833:
5832:
5827:
5822:
5807:
5805:
5795:
5794:
5792:
5791:
5790:
5789:
5784:
5779:
5769:
5764:
5759:
5754:
5749:
5744:
5739:
5734:
5729:
5724:
5719:
5714:
5708:
5706:
5699:
5698:
5696:
5695:
5694:
5693:
5688:
5683:
5678:
5673:
5668:
5660:
5659:
5658:
5653:
5643:
5638:
5636:Extensionality
5633:
5631:Ordinal number
5628:
5618:
5613:
5612:
5611:
5600:
5594:
5588:
5587:
5584:
5583:
5581:
5580:
5575:
5570:
5565:
5560:
5555:
5550:
5549:
5548:
5538:
5537:
5536:
5523:
5521:
5515:
5514:
5512:
5511:
5510:
5509:
5504:
5499:
5489:
5484:
5479:
5474:
5469:
5464:
5458:
5456:
5450:
5449:
5447:
5446:
5441:
5436:
5431:
5426:
5421:
5416:
5415:
5414:
5404:
5399:
5394:
5389:
5384:
5379:
5373:
5371:
5362:
5356:
5355:
5353:
5352:
5347:
5342:
5337:
5332:
5327:
5315:Cantor's
5313:
5308:
5303:
5293:
5291:
5278:
5277:
5275:
5274:
5269:
5264:
5259:
5254:
5249:
5244:
5239:
5234:
5229:
5224:
5219:
5214:
5213:
5212:
5201:
5199:
5195:
5194:
5189:
5187:
5186:
5179:
5172:
5164:
5158:
5157:
5143:Farmer, W. M.
5140:
5126:
5125:External links
5123:
5122:
5121:
5120:
5119:
5109:
5096:
5095:
5094:
5090:
5084:
5064:
5046:
5037:
5031:
5010:
4999:
4996:
4994:
4993:
4986:
4956:
4949:
4931:
4889:
4858:
4851:
4828:
4808:
4801:
4778:
4753:
4746:
4717:
4710:
4690:
4683:
4663:
4656:
4628:
4621:
4601:
4594:
4574:
4567:
4547:
4540:
4520:
4496:
4489:
4461:
4454:
4434:
4427:
4404:
4397:
4377:
4370:
4350:
4343:
4323:
4316:
4296:
4268:
4261:
4236:
4229:
4204:
4191:
4189:
4186:
4185:
4184:
4179:
4174:
4167:
4164:
4150:
4149:
4100:
4098:
4091:
4085:
4082:
4081:
4080:
4069:
4066:
4063:
4060:
4057:
4054:
4051:
4048:
4045:
4042:
4039:
4036:
4033:
4030:
4027:
4024:
4021:
4018:
4015:
4004:
3993:
3990:
3987:
3984:
3981:
3970:
3959:
3956:
3953:
3950:
3947:
3935:
3934:
3930:
3929:
3918:
3915:
3912:
3909:
3906:
3895:
3884:
3881:
3878:
3875:
3872:
3861:
3850:
3847:
3844:
3841:
3838:
3835:
3832:
3829:
3826:
3817:introduction:
3814:
3813:
3808:
3805:
3804:
3803:
3791:
3767:
3747:
3744:
3741:
3738:
3735:
3732:
3729:
3726:
3723:
3720:
3717:
3714:
3711:
3708:
3705:
3694:
3693:
3689:
3688:
3677:
3674:
3671:
3668:
3665:
3662:
3659:
3656:
3653:
3650:
3647:
3644:
3641:
3638:
3635:
3632:
3621:
3620:
3615:
3612:
3585:
3584:
3535:
3533:
3526:
3520:
3517:
3516:
3515:
3503:
3499:
3496:
3493:
3490:
3487:
3484:
3481:
3478:
3475:
3472:
3469:
3466:
3463:
3459:
3455:
3451:
3447:
3444:
3441:
3437:
3425:
3409:
3406:
3403:
3374:
3373:
3361:
3336:
3333:
3330:
3326:
3323:
3320:
3317:
3306:
3294:
3289:
3286:
3283:
3279:
3276:
3273:
3269:
3266:
3263:
3259:
3256:
3252:
3248:
3244:
3240:
3237:
3234:
3230:
3226:
3223:
3212:
3201:
3171:
3168:
3165:
3162:
3159:
3156:
3153:
3149:
3146:
3143:
3139:
3136:
3121:
3120:
3108:
3105:
3102:
3099:
3079:
3076:
3073:
3070:
3050:
3030:
3010:
3007:
3004:
3001:
2970:
2949:
2945:
2942:
2939:
2935:
2931:
2927:
2923:
2920:
2917:
2913:
2892:
2889:
2886:
2875:
2874:
2862:
2858:
2855:
2852:
2848:
2844:
2841:
2838:
2827:
2816:
2813:
2810:
2806:
2802:
2799:
2796:
2793:
2789:
2770:
2769:
2757:
2753:
2750:
2747:
2743:
2739:
2736:
2733:
2730:
2726:
2721:
2717:
2713:
2709:
2706:
2703:
2699:
2674:
2671:
2668:
2648:
2645:
2618:
2617:
2605:
2601:
2598:
2595:
2591:
2587:
2583:
2579:
2576:
2573:
2570:
2567:
2563:
2551:
2539:
2534:
2530:
2527:
2524:
2520:
2516:
2512:
2508:
2505:
2502:
2498:
2493:
2489:
2485:
2480:
2476:
2473:
2470:
2466:
2462:
2459:
2455:
2443:
2431:
2427:
2424:
2421:
2417:
2413:
2410:
2399:
2388:
2385:
2382:
2355:
2335:
2315:
2295:
2275:
2261:
2260:
2211:
2209:
2202:
2196:
2193:
2192:
2191:
2179:
2176:
2173:
2163:
2151:
2148:
2145:
2142:
2139:
2136:
2133:
2123:
2107:
2104:
2101:
2098:
2095:
2092:
2089:
2086:
2083:
2080:
2077:
2074:
2071:
2068:
2065:
2055:
2043:
2040:
2037:
2034:
2031:
2028:
2025:
2022:
2019:
2016:
2013:
2010:
2007:
2004:
2001:
1998:
1995:
1992:
1989:
1986:
1983:
1980:
1977:
1974:
1971:
1968:
1965:
1962:
1959:
1956:
1953:
1943:
1931:
1928:
1925:
1922:
1919:
1916:
1913:
1910:
1907:
1904:
1901:
1887:
1886:
1875:
1872:
1869:
1866:
1863:
1860:
1857:
1854:
1851:
1848:
1845:
1842:
1839:
1836:
1833:
1822:
1811:
1808:
1805:
1802:
1799:
1796:
1793:
1790:
1787:
1784:
1781:
1778:
1775:
1772:
1769:
1766:
1763:
1760:
1757:
1754:
1751:
1748:
1745:
1742:
1739:
1728:
1717:
1714:
1711:
1708:
1705:
1702:
1699:
1696:
1693:
1677:
1665:
1662:
1659:
1647:
1644:
1641:
1619:
1601:
1589:
1586:
1585:
1574:
1571:
1568:
1565:
1562:
1559:
1556:
1553:
1550:
1547:
1544:
1541:
1538:
1528:
1517:
1514:
1511:
1508:
1505:
1502:
1499:
1496:
1493:
1490:
1487:
1484:
1481:
1478:
1475:
1472:
1469:
1466:
1463:
1460:
1457:
1454:
1451:
1441:
1430:
1427:
1424:
1421:
1418:
1415:
1412:
1392:
1389:
1386:
1381:
1374:
1373:
1362:
1359:
1356:
1353:
1350:
1347:
1344:
1341:
1338:
1335:
1332:
1329:
1326:
1316:
1305:
1302:
1299:
1296:
1293:
1290:
1287:
1284:
1281:
1278:
1275:
1272:
1269:
1266:
1263:
1260:
1257:
1254:
1251:
1248:
1245:
1242:
1239:
1229:
1218:
1215:
1212:
1209:
1206:
1203:
1200:
1177:
1174:
1171:
1168:
1165:
1162:
1159:
1156:
1153:
1150:
1147:
1144:
1141:
1117:
1114:
1111:
1108:
1105:
1102:
1099:
1096:
1093:
1078:
1075:
1072:
1067:
1066:
1055:
1052:
1049:
1046:
1043:
1032:
1021:
1018:
1015:
1012:
1009:
998:
987:
984:
981:
978:
975:
972:
969:
966:
963:
960:
957:
954:
951:
940:
929:
926:
923:
920:
917:
914:
911:
908:
905:
902:
899:
896:
893:
890:
887:
884:
881:
878:
875:
864:
853:
850:
847:
844:
841:
838:
835:
832:
829:
826:
823:
820:
817:
814:
811:
808:
805:
802:
799:
796:
793:
790:
787:
776:
765:
762:
759:
756:
753:
750:
747:
688:
682:
665:
662:
649:
646:
643:
640:
637:
634:
631:
628:
625:
605:
602:
599:
596:
593:
590:
587:
584:
581:
578:
575:
572:
569:
553:logical axioms
537:
517:
497:
494:
491:
471:
460:logical axioms
447:
427:
424:
421:
393:
369:
335:
334:
285:
283:
276:
270:
267:
219:generalisation
191:logical axioms
151:
147:
126:
122:
69:attributed to
40:Hilbert system
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
7230:
7219:
7216:
7214:
7211:
7209:
7206:
7205:
7203:
7188:
7185:
7183:
7180:
7178:
7175:
7173:
7170:
7168:
7165:
7163:
7160:
7158:
7155:
7153:
7150:
7148:
7145:
7144:
7142:
7140:
7136:
7130:
7127:
7125:
7122:
7120:
7117:
7115:
7112:
7110:
7107:
7105:
7102:
7100:
7097:
7096:
7094:
7092:
7088:
7082:
7079:
7077:
7074:
7072:
7069:
7067:
7064:
7062:
7059:
7057:
7054:
7052:
7049:
7047:
7044:
7042:
7039:
7037:
7034:
7033:
7031:
7029:
7025:
7019:
7016:
7014:
7011:
7009:
7006:
7004:
7001:
6999:
6996:
6992:
6989:
6987:
6984:
6982:
6979:
6978:
6977:
6976:Formal system
6974:
6972:
6969:
6967:
6964:
6963:
6961:
6959:
6955:
6951:
6943:
6938:
6936:
6931:
6929:
6924:
6923:
6920:
6910:
6909:
6904:
6896:
6890:
6887:
6885:
6882:
6880:
6877:
6875:
6872:
6868:
6865:
6864:
6863:
6860:
6858:
6855:
6853:
6850:
6848:
6844:
6841:
6839:
6836:
6834:
6831:
6829:
6826:
6824:
6821:
6820:
6818:
6814:
6808:
6805:
6803:
6800:
6798:
6797:Recursive set
6795:
6793:
6790:
6788:
6785:
6783:
6780:
6778:
6775:
6771:
6768:
6766:
6763:
6761:
6758:
6756:
6753:
6751:
6748:
6747:
6746:
6743:
6741:
6738:
6736:
6733:
6731:
6728:
6726:
6723:
6721:
6718:
6717:
6715:
6713:
6709:
6703:
6700:
6698:
6695:
6693:
6690:
6688:
6685:
6683:
6680:
6678:
6675:
6673:
6670:
6666:
6663:
6661:
6658:
6656:
6653:
6652:
6651:
6648:
6646:
6643:
6641:
6638:
6636:
6633:
6631:
6628:
6626:
6623:
6619:
6616:
6615:
6614:
6611:
6607:
6606:of arithmetic
6604:
6603:
6602:
6599:
6595:
6592:
6590:
6587:
6585:
6582:
6580:
6577:
6575:
6572:
6571:
6570:
6567:
6563:
6560:
6558:
6555:
6554:
6553:
6550:
6549:
6547:
6545:
6541:
6535:
6532:
6530:
6527:
6525:
6522:
6520:
6517:
6514:
6513:from ZFC
6510:
6507:
6505:
6502:
6496:
6493:
6492:
6491:
6488:
6486:
6483:
6481:
6478:
6477:
6476:
6473:
6471:
6468:
6466:
6463:
6461:
6458:
6456:
6453:
6451:
6448:
6446:
6443:
6442:
6440:
6438:
6434:
6424:
6423:
6419:
6418:
6413:
6412:non-Euclidean
6410:
6406:
6403:
6401:
6398:
6396:
6395:
6391:
6390:
6388:
6385:
6384:
6382:
6378:
6374:
6371:
6369:
6366:
6365:
6364:
6360:
6356:
6353:
6352:
6351:
6347:
6343:
6340:
6338:
6335:
6333:
6330:
6328:
6325:
6323:
6320:
6318:
6315:
6314:
6312:
6308:
6307:
6305:
6300:
6294:
6289:Example
6286:
6278:
6273:
6272:
6271:
6268:
6266:
6263:
6259:
6256:
6254:
6251:
6249:
6246:
6244:
6241:
6240:
6239:
6236:
6234:
6231:
6229:
6226:
6224:
6221:
6217:
6214:
6212:
6209:
6208:
6207:
6204:
6200:
6197:
6195:
6192:
6190:
6187:
6185:
6182:
6181:
6180:
6177:
6175:
6172:
6168:
6165:
6163:
6160:
6158:
6155:
6154:
6153:
6150:
6146:
6143:
6141:
6138:
6136:
6133:
6131:
6128:
6126:
6123:
6121:
6118:
6117:
6116:
6113:
6111:
6108:
6106:
6103:
6101:
6098:
6094:
6091:
6089:
6086:
6084:
6081:
6079:
6076:
6075:
6074:
6071:
6069:
6066:
6064:
6061:
6059:
6056:
6052:
6049:
6047:
6046:by definition
6044:
6043:
6042:
6039:
6035:
6032:
6031:
6030:
6027:
6025:
6022:
6020:
6017:
6015:
6012:
6010:
6007:
6006:
6003:
6000:
5998:
5994:
5989:
5983:
5979:
5969:
5966:
5964:
5961:
5959:
5956:
5954:
5951:
5949:
5946:
5944:
5941:
5939:
5936:
5934:
5933:Kripke–Platek
5931:
5929:
5926:
5922:
5919:
5917:
5914:
5913:
5912:
5909:
5908:
5906:
5902:
5894:
5891:
5890:
5889:
5886:
5884:
5881:
5877:
5874:
5873:
5872:
5869:
5867:
5864:
5862:
5859:
5857:
5854:
5852:
5849:
5846:
5842:
5838:
5835:
5831:
5828:
5826:
5823:
5821:
5818:
5817:
5816:
5812:
5809:
5808:
5806:
5804:
5800:
5796:
5788:
5785:
5783:
5780:
5778:
5777:constructible
5775:
5774:
5773:
5770:
5768:
5765:
5763:
5760:
5758:
5755:
5753:
5750:
5748:
5745:
5743:
5740:
5738:
5735:
5733:
5730:
5728:
5725:
5723:
5720:
5718:
5715:
5713:
5710:
5709:
5707:
5705:
5700:
5692:
5689:
5687:
5684:
5682:
5679:
5677:
5674:
5672:
5669:
5667:
5664:
5663:
5661:
5657:
5654:
5652:
5649:
5648:
5647:
5644:
5642:
5639:
5637:
5634:
5632:
5629:
5627:
5623:
5619:
5617:
5614:
5610:
5607:
5606:
5605:
5602:
5601:
5598:
5595:
5593:
5589:
5579:
5576:
5574:
5571:
5569:
5566:
5564:
5561:
5559:
5556:
5554:
5551:
5547:
5544:
5543:
5542:
5539:
5535:
5530:
5529:
5528:
5525:
5524:
5522:
5520:
5516:
5508:
5505:
5503:
5500:
5498:
5495:
5494:
5493:
5490:
5488:
5485:
5483:
5480:
5478:
5475:
5473:
5470:
5468:
5465:
5463:
5460:
5459:
5457:
5455:
5454:Propositional
5451:
5445:
5442:
5440:
5437:
5435:
5432:
5430:
5427:
5425:
5422:
5420:
5417:
5413:
5410:
5409:
5408:
5405:
5403:
5400:
5398:
5395:
5393:
5390:
5388:
5385:
5383:
5382:Logical truth
5380:
5378:
5375:
5374:
5372:
5370:
5366:
5363:
5361:
5357:
5351:
5348:
5346:
5343:
5341:
5338:
5336:
5333:
5331:
5328:
5326:
5322:
5318:
5314:
5312:
5309:
5307:
5304:
5302:
5298:
5295:
5294:
5292:
5290:
5284:
5279:
5273:
5270:
5268:
5265:
5263:
5260:
5258:
5255:
5253:
5250:
5248:
5245:
5243:
5240:
5238:
5235:
5233:
5230:
5228:
5225:
5223:
5220:
5218:
5215:
5211:
5208:
5207:
5206:
5203:
5202:
5200:
5196:
5192:
5185:
5180:
5178:
5173:
5171:
5166:
5165:
5162:
5155:
5146:
5141:
5134:
5129:
5128:
5124:
5116:
5115:
5112:
5110:0-7204-2103-9
5106:
5102:
5097:
5091:
5087:
5085:0-674-32449-8
5081:
5076:
5075:
5068:
5067:
5065:
5062:
5058:
5057:Alfred Tarski
5052:
5047:
5043:
5038:
5034:
5028:
5024:
5019:
5018:
5011:
5007:
5002:
5001:
4997:
4989:
4983:
4979:
4975:
4971:
4967:
4960:
4957:
4952:
4946:
4942:
4935:
4932:
4927:
4923:
4919:
4915:
4911:
4907:
4903:
4896:
4894:
4890:
4879:
4875:
4869:
4867:
4865:
4863:
4859:
4854:
4848:
4844:
4843:
4835:
4833:
4829:
4824:
4823:
4815:
4813:
4809:
4804:
4798:
4794:
4793:
4785:
4783:
4779:
4768:
4764:
4757:
4754:
4749:
4743:
4739:
4738:
4730:
4728:
4726:
4724:
4722:
4718:
4713:
4707:
4703:
4702:
4694:
4691:
4686:
4680:
4676:
4675:
4667:
4664:
4659:
4653:
4649:
4645:
4641:
4640:
4632:
4629:
4624:
4618:
4614:
4613:
4605:
4602:
4597:
4591:
4587:
4586:
4578:
4575:
4570:
4564:
4560:
4559:
4551:
4548:
4543:
4537:
4533:
4532:
4524:
4521:
4510:
4506:
4500:
4497:
4492:
4486:
4482:
4478:
4474:
4473:
4465:
4462:
4457:
4451:
4447:
4446:
4438:
4435:
4430:
4424:
4420:
4413:
4411:
4409:
4405:
4400:
4394:
4390:
4389:
4381:
4378:
4373:
4367:
4363:
4362:
4354:
4351:
4346:
4340:
4336:
4335:
4327:
4324:
4319:
4313:
4309:
4308:
4300:
4297:
4286:
4279:
4272:
4269:
4264:
4258:
4254:
4253:
4245:
4243:
4241:
4237:
4232:
4226:
4222:
4221:
4213:
4211:
4209:
4205:
4199:
4197:
4193:
4187:
4183:
4180:
4178:
4175:
4173:
4170:
4169:
4165:
4163:
4161:
4157:
4146:
4143:
4135:
4125:
4121:
4117:
4111:
4110:
4106:
4101:This section
4099:
4095:
4090:
4089:
4083:
4064:
4058:
4055:
4052:
4043:
4037:
4022:
4016:
4006:elimination:
4005:
3991:
3988:
3985:
3979:
3971:
3957:
3954:
3951:
3945:
3937:
3936:
3932:
3931:
3916:
3910:
3907:
3904:
3896:
3882:
3876:
3873:
3870:
3862:
3845:
3842:
3839:
3833:
3824:
3816:
3815:
3811:
3810:
3806:
3789:
3781:
3780:free variable
3765:
3745:
3736:
3730:
3718:
3712:
3706:
3696:
3695:
3691:
3690:
3666:
3663:
3660:
3654:
3648:
3639:
3633:
3623:
3622:
3618:
3617:
3613:
3611:
3609:
3604:
3600:
3596:
3592:
3581:
3578:
3570:
3560:
3556:
3552:
3546:
3545:
3541:
3536:This section
3534:
3530:
3525:
3524:
3518:
3501:
3494:
3491:
3488:
3482:
3473:
3470:
3467:
3461:
3457:
3449:
3445:
3442:
3439:
3435:
3426:
3423:
3407:
3404:
3401:
3393:
3392:
3391:
3388:
3385:
3383:
3379:
3359:
3351:
3334:
3331:
3328:
3324:
3315:
3307:
3292:
3287:
3284:
3281:
3277:
3267:
3264:
3261:
3257:
3250:
3242:
3238:
3232:
3228:
3224:
3213:
3199:
3189:
3185:
3166:
3163:
3160:
3154:
3147:
3144:
3141:
3137:
3126:
3125:
3124:
3103:
3097:
3074:
3068:
3048:
3028:
3005:
2999:
2991:
2990:
2989:
2987:
2982:
2968:
2947:
2943:
2937:
2933:
2925:
2921:
2915:
2911:
2890:
2884:
2860:
2856:
2850:
2846:
2839:
2828:
2814:
2804:
2800:
2791:
2787:
2778:
2777:
2776:
2774:
2755:
2751:
2741:
2737:
2728:
2724:
2719:
2711:
2707:
2701:
2697:
2688:
2687:
2686:
2666:
2646:
2635:
2634:Minimal logic
2631:
2627:
2623:
2603:
2599:
2593:
2589:
2581:
2577:
2568:
2561:
2552:
2537:
2532:
2528:
2522:
2518:
2510:
2506:
2500:
2496:
2491:
2483:
2478:
2474:
2468:
2464:
2457:
2453:
2444:
2429:
2425:
2419:
2415:
2408:
2400:
2386:
2380:
2372:
2371:
2370:
2367:
2353:
2333:
2257:
2254:
2246:
2236:
2232:
2228:
2222:
2221:
2217:
2212:This section
2210:
2206:
2201:
2200:
2194:
2177:
2171:
2164:
2146:
2140:
2131:
2124:
2121:
2102:
2096:
2081:
2075:
2066:
2056:
2035:
2029:
2014:
2008:
1999:
1981:
1972:
1966:
1954:
1944:
1926:
1917:
1911:
1899:
1892:
1891:
1890:
1867:
1861:
1849:
1840:
1823:
1800:
1794:
1782:
1776:
1758:
1752:
1743:
1729:
1709:
1703:
1694:
1683:
1682:
1681:
1663:
1657:
1642:
1640:
1638:
1637:Frege systems
1633:
1607:
1599:
1595:
1569:
1563:
1551:
1542:
1529:
1509:
1503:
1491:
1485:
1467:
1461:
1452:
1442:
1425:
1419:
1410:
1403:
1402:
1401:
1399:
1387:
1385:
1379:
1378:Alonzo Church
1357:
1351:
1339:
1330:
1317:
1297:
1291:
1279:
1273:
1255:
1249:
1240:
1230:
1213:
1207:
1198:
1191:
1190:
1189:
1172:
1166:
1154:
1145:
1131:
1115:
1112:
1109:
1106:
1103:
1100:
1097:
1094:
1091:
1083:
1071:
1053:
1044:
1041:
1033:
1019:
1016:
1013:
999:
982:
976:
973:
964:
958:
955:
952:
941:
921:
918:
915:
909:
906:
900:
891:
888:
885:
879:
876:
865:
845:
842:
839:
833:
827:
824:
821:
812:
803:
800:
797:
791:
788:
777:
760:
757:
754:
748:
745:
737:
736:
735:
733:
729:
725:
724:
720:
716:
715:Gottlob Frege
712:
704:
703:
698:
694:
693:Ancient Greek
687:
681:
679:
675:
671:
663:
661:
647:
644:
641:
635:
632:
629:
626:
600:
597:
594:
588:
585:
582:
579:
570:
558:
554:
549:
515:
495:
492:
461:
445:
425:
422:
411:
407:
383:
358:
356:
355:
350:
341:
331:
328:
320:
310:
306:
302:
296:
295:
291:
286:This section
284:
280:
275:
274:
268:
266:
263:
259:
255:
251:
247:
242:
240:
236:
232:
228:
224:
220:
216:
212:
208:
205:. Systems of
204:
200:
196:
192:
188:
183:
181:
180:
175:
170:
166:
149:
124:
111:
107:
101:
99:
95:
91:
86:
84:
80:
76:
75:David Hilbert
72:
71:Gottlob Frege
68:
65:
61:
57:
53:
49:
45:
41:
37:
33:
19:
7208:Proof theory
7152:Topos theory
7003:Model theory
6985:
6966:Peano axioms
6899:
6697:Ultraproduct
6544:Model theory
6509:Independence
6489:
6445:Formal proof
6437:Proof theory
6420:
6393:
6350:real numbers
6322:second-order
6233:Substitution
6110:Metalanguage
6051:conservative
6024:Axiom schema
5968:Constructive
5938:Morse–Kelley
5904:Set theories
5883:Aleph number
5876:inaccessible
5782:Grothendieck
5666:intersection
5553:Higher-order
5541:Second-order
5487:Truth tables
5444:Venn diagram
5227:Formal proof
5100:
5073:
5050:
5041:
5016:
5005:
4969:
4959:
4940:
4934:
4909:
4905:
4881:. Retrieved
4877:
4841:
4821:
4791:
4771:, retrieved
4766:
4756:
4736:
4700:
4693:
4673:
4666:
4638:
4631:
4611:
4604:
4584:
4577:
4557:
4550:
4530:
4523:
4512:. Retrieved
4508:
4499:
4471:
4464:
4444:
4437:
4418:
4387:
4380:
4360:
4353:
4333:
4326:
4306:
4299:
4288:. Retrieved
4284:
4271:
4251:
4219:
4156:metatheorems
4155:
4153:
4138:
4129:
4114:Please help
4102:
4084:Metatheorems
3619:Introduction
3588:
3573:
3564:
3549:Please help
3537:
3421:
3389:
3386:
3375:
3349:
3187:
3183:
3122:
2983:
2876:
2771:
2619:
2368:
2264:
2249:
2240:
2225:Please help
2213:
2120:modus ponens
1888:
1649:
1634:
1608:, and named
1587:
1394:
1375:
1080:
1068:
721:
700:
690:
685:
678:Frege system
667:
557:axiom schema
552:
550:
459:
406:group theory
381:
359:
352:
348:
346:
323:
314:
299:Please help
287:
245:
243:
227:modal logics
221:, to handle
211:modus ponens
184:
177:
164:
109:
102:
90:modus ponens
87:
64:formal proof
59:
55:
51:
47:
43:
39:
36:proof theory
29:
7091:Type theory
7071:Determinacy
7013:Modal logic
6807:Type theory
6755:undecidable
6687:Truth value
6574:equivalence
6253:non-logical
5866:Enumeration
5856:Isomorphism
5803:cardinality
5787:Von Neumann
5752:Ultrafilter
5717:Uncountable
5651:equivalence
5568:Quantifiers
5558:Fixed-point
5527:First-order
5407:Consistency
5392:Proposition
5369:Traditional
5340:Lindström's
5330:Compactness
5272:Type theory
5217:Cardinality
3692:Elimination
2243:August 2024
728:implication
508:means that
317:August 2024
258:tautologies
7202:Categories
7167:∞-groupoid
7028:Set theory
6618:elementary
6311:arithmetic
6179:Quantifier
6157:functional
6029:Expression
5747:Transitive
5691:identities
5676:complement
5609:hereditary
5592:Set theory
4998:References
4883:2024-07-02
4773:2024-03-22
4514:2024-08-16
4290:2024-08-19
4132:March 2024
3567:March 2024
3041:, and let
695:textbook,
410:set theory
382:hypotheses
6889:Supertask
6792:Recursion
6750:decidable
6584:saturated
6562:of models
6485:deductive
6480:axiomatic
6400:Hilbert's
6387:Euclidean
6368:canonical
6291:axiomatic
6223:Signature
6152:Predicate
6041:Extension
5963:Ackermann
5888:Operation
5767:Universal
5757:Recursive
5732:Singleton
5727:Inhabited
5712:Countable
5702:Types of
5686:power set
5656:partition
5573:Predicate
5519:Predicate
5434:Syllogism
5424:Soundness
5397:Inference
5387:Tautology
5289:paradoxes
4926:0022-4812
4912:(1): 39.
4103:does not
4065:γ
4062:→
4059:β
4056:∨
4053:α
4050:→
4044:γ
4041:→
4038:β
4029:→
4023:γ
4020:→
4017:α
3992:β
3989:∨
3986:α
3983:→
3980:β
3958:β
3955:∨
3952:α
3949:→
3946:α
3917:β
3914:→
3911:β
3908:∧
3905:α
3883:α
3880:→
3877:β
3874:∧
3871:α
3846:β
3843:∧
3840:α
3837:→
3834:β
3828:→
3825:α
3790:ψ
3778:is not a
3746:ψ
3743:→
3737:ϕ
3728:∃
3725:→
3719:ψ
3716:→
3713:ϕ
3704:∀
3655:ϕ
3646:∃
3643:→
3640:ϕ
3631:∀
3538:does not
3483:ϕ
3480:→
3462:ϕ
3454:→
3360:ϕ
3332:ϕ
3322:∀
3319:→
3316:ϕ
3285:ψ
3275:∀
3272:→
3265:ϕ
3255:∀
3247:→
3239:ψ
3236:→
3233:ϕ
3222:∀
3200:ϕ
3155:ϕ
3152:→
3145:ϕ
3135:∀
3104:ψ
3098:ϕ
3069:ϕ
3049:ψ
3000:ϕ
2969:ϕ
2941:→
2930:→
2919:→
2888:→
2857:ψ
2854:→
2851:ϕ
2843:→
2840:ϕ
2837:¬
2815:ϕ
2812:¬
2809:→
2801:ϕ
2798:¬
2795:→
2792:ϕ
2752:ϕ
2749:¬
2746:→
2738:ψ
2735:¬
2732:→
2729:ϕ
2716:→
2708:ψ
2705:→
2702:ϕ
2673:⊥
2670:→
2667:ϕ
2647:ϕ
2644:¬
2600:ϕ
2597:→
2594:ψ
2586:→
2578:ψ
2575:¬
2572:→
2569:ϕ
2566:¬
2529:ξ
2526:→
2523:ϕ
2515:→
2507:ψ
2504:→
2501:ϕ
2488:→
2475:ξ
2472:→
2469:ψ
2461:→
2458:ϕ
2426:ϕ
2423:→
2420:ψ
2412:→
2409:ϕ
2387:ϕ
2384:→
2381:ϕ
2354:∨
2334:∧
2314:∀
2294:→
2274:¬
2214:does not
2175:→
2144:→
2135:→
2100:→
2091:→
2079:→
2070:→
2033:→
2024:→
2012:→
2003:→
1991:→
1979:→
1970:→
1958:→
1924:→
1915:→
1903:→
1865:→
1856:→
1847:¬
1844:→
1838:¬
1798:→
1789:→
1780:→
1768:→
1756:→
1747:→
1707:→
1698:→
1661:→
1570:φ
1567:→
1564:ψ
1558:→
1552:ψ
1549:¬
1546:→
1543:φ
1540:¬
1510:χ
1507:→
1504:φ
1498:→
1492:ψ
1489:→
1486:φ
1477:→
1468:χ
1465:→
1462:ψ
1456:→
1453:φ
1426:φ
1423:→
1420:ψ
1414:→
1411:φ
1355:→
1346:→
1337:¬
1334:→
1328:¬
1295:→
1286:→
1277:→
1265:→
1253:→
1244:→
1211:→
1202:→
1170:→
1161:→
1152:¬
1149:→
1143:¬
1051:¬
1048:¬
1045:⊃
1017:⊃
1011:¬
1008:¬
980:¬
977:⊃
971:¬
965:⊃
956:⊃
919:⊃
910:⊃
901:⊃
889:⊃
880:⊃
843:⊃
834:⊃
825:⊃
813:⊃
801:⊃
792:⊃
758:⊃
749:⊃
639:→
624:∀
592:→
577:∀
568:∀
536:Γ
516:ϕ
496:ϕ
493:⊢
490:Γ
470:Γ
446:ϕ
426:ϕ
423:⊢
420:Γ
392:Γ
368:Γ
288:does not
262:judgments
187:trade-off
174:Ackermann
165:schematic
146:∀
121:→
106:Troelstra
7147:Category
6874:Logicism
6867:timeline
6843:Concrete
6702:Validity
6672:T-schema
6665:Kripke's
6660:Tarski's
6655:semantic
6645:Strength
6594:submodel
6589:spectrum
6557:function
6405:Tarski's
6394:Elements
6381:geometry
6337:Robinson
6258:variable
6243:function
6216:spectrum
6206:Sentence
6162:variable
6105:Language
6058:Relation
6019:Automata
6009:Alphabet
5993:language
5847:-jection
5825:codomain
5811:Function
5772:Universe
5742:Infinite
5646:Relation
5429:Validity
5419:Argument
5317:theorem,
4285:Columbia
4166:See also
3090:, infer
2992:US. Let
1598:Metamath
732:negation
684:Frege's
360:Suppose
189:between
182:(1928).
77:. These
6816:Related
6613:Diagram
6511: (
6490:Hilbert
6475:Systems
6470:Theorem
6348:of the
6293:systems
6073:Formula
6068:Grammar
5984: (
5928:General
5641:Forcing
5626:Element
5546:Monadic
5321:paradox
5262:Theorem
5198:General
4124:removed
4109:sources
3597:of the
3559:removed
3544:sources
2235:removed
2220:sources
1606:Hilbert
309:removed
294:sources
246:context
199:schemas
6579:finite
6342:Skolem
6295:
6270:Theory
6238:Symbol
6228:String
6211:atomic
6088:ground
6083:closed
6078:atomic
6034:ground
5997:syntax
5893:binary
5820:domain
5737:Finite
5502:finite
5360:Logics
5319:
5267:Theory
5107:
5082:
5029:
4984:
4947:
4924:
4849:
4799:
4744:
4708:
4681:
4654:
4619:
4592:
4565:
4538:
4487:
4452:
4425:
4395:
4368:
4341:
4314:
4259:
4227:
3758:where
3348:where
3182:where
2961:: the
697:Euclid
213:, for
67:system
6569:Model
6317:Peano
6174:Proof
6014:Arity
5943:Naive
5830:image
5762:Fuzzy
5722:Empty
5671:union
5616:Class
5257:Model
5247:Lemma
5205:Axiom
5148:(PDF)
5136:(PDF)
4281:(PDF)
4188:Notes
2829:P5i.
2779:P4i.
2689:P4m.
2622:proof
1824:(A3)
1730:(A2)
1684:(A1)
555:. An
354:proof
112:with
32:logic
6692:Type
6495:list
6299:list
6276:list
6265:Term
6199:rank
6093:open
5987:list
5799:Maps
5704:sets
5563:Free
5533:list
5283:list
5210:list
5105:ISBN
5080:ISBN
5027:ISBN
4982:ISBN
4945:ISBN
4922:ISSN
4847:ISBN
4797:ISBN
4742:ISBN
4706:ISBN
4679:ISBN
4652:ISBN
4617:ISBN
4590:ISBN
4563:ISBN
4536:ISBN
4485:ISBN
4450:ISBN
4423:ISBN
4393:ISBN
4366:ISBN
4339:ISBN
4312:ISBN
4257:ISBN
4225:ISBN
4107:any
4105:cite
3542:any
3540:cite
3427:I9.
3394:I8.
3308:Q7.
3214:Q6.
3127:Q5.
2553:P4.
2445:P3.
2401:P2.
2373:P1.
2346:and
2286:and
2218:any
2216:cite
1676:in P
730:and
719:1879
351:(or
292:any
290:cite
252:and
193:and
137:and
73:and
38:, a
7036:Set
6379:of
6361:of
6309:of
5841:Sur
5815:Map
5622:Ur-
5604:Set
4974:doi
4914:doi
4644:doi
4477:doi
4118:by
3782:of
3553:by
3190:in
2659:as
2229:by
717:'s
699:'s
408:or
303:by
176:'s
110:and
58:or
30:In
7204::
6765:NP
6389::
6383::
6313::
5990:),
5845:Bi
5837:In
5156:).
5025:.
4980:.
4968:.
4920:.
4910:44
4908:.
4904:.
4892:^
4876:.
4861:^
4831:^
4811:^
4781:^
4720:^
4650:.
4507:.
4483:.
4407:^
4283:.
4239:^
4207:^
4195:^
3664::=
3610:.
3492::=
3471::=
3384:.
3164::=
2685:.
2632:.
1382:2,
707:c.
705:,
680:.
660:.
548:.
54:,
50:,
46:,
6941:e
6934:t
6927:v
6845:/
6760:P
6515:)
6301:)
6297:(
6194:∀
6189:!
6184:∃
6145:=
6140:↔
6135:→
6130:∧
6125:∨
6120:¬
5843:/
5839:/
5813:/
5624:)
5620:(
5507:∞
5497:3
5285:)
5183:e
5176:t
5169:v
5150:.
5138:.
5113:.
5088:.
5063:.
5035:.
4990:.
4976::
4953:.
4928:.
4916::
4886:.
4855:.
4805:.
4750:.
4714:.
4687:.
4660:.
4646::
4625:.
4598:.
4571:.
4544:.
4517:.
4493:.
4479::
4458:.
4431:.
4401:.
4374:.
4347:.
4320:.
4293:.
4265:.
4233:.
4145:)
4139:(
4134:)
4130:(
4126:.
4112:.
4068:)
4047:)
4035:(
4032:(
4026:)
4014:(
3849:)
3831:(
3802:.
3766:x
3740:)
3734:(
3731:x
3722:)
3710:(
3707:x
3676:)
3673:)
3670:]
3667:y
3661:x
3658:[
3652:(
3649:y
3637:(
3634:x
3580:)
3574:(
3569:)
3565:(
3561:.
3547:.
3502:)
3498:]
3495:y
3489:z
3486:[
3477:]
3474:x
3468:z
3465:[
3458:(
3450:)
3446:y
3443:=
3440:x
3436:(
3424:.
3422:x
3408:x
3405:=
3402:x
3372:.
3350:x
3335:)
3329:(
3325:x
3293:)
3288:)
3282:(
3278:x
3268:)
3262:(
3258:x
3251:(
3243:)
3229:(
3225:x
3188:x
3184:t
3170:]
3167:t
3161:x
3158:[
3148:)
3142:(
3138:x
3119:.
3107:)
3101:(
3078:)
3075:p
3072:(
3029:p
3009:)
3006:p
3003:(
2948:)
2944:q
2938:p
2934:(
2926:)
2922:q
2916:p
2912:(
2891:p
2885:p
2861:)
2847:(
2805:)
2788:(
2756:)
2742:)
2725:(
2720:(
2712:)
2698:(
2604:)
2590:(
2582:)
2562:(
2538:)
2533:)
2519:(
2511:)
2497:(
2492:(
2484:)
2479:)
2465:(
2454:(
2430:)
2416:(
2256:)
2250:(
2245:)
2241:(
2237:.
2223:.
2178:A
2172:A
2150:)
2147:A
2141:B
2138:(
2132:A
2122:)
2106:)
2103:A
2097:A
2094:(
2088:)
2085:)
2082:A
2076:B
2073:(
2067:A
2064:(
2042:)
2039:)
2036:A
2030:A
2027:(
2021:)
2018:)
2015:A
2009:B
2006:(
2000:A
1997:(
1994:(
1988:)
1985:)
1982:A
1976:)
1973:A
1967:B
1964:(
1961:(
1955:A
1952:(
1930:)
1927:A
1921:)
1918:A
1912:B
1909:(
1906:(
1900:A
1874:)
1871:)
1868:p
1862:q
1859:(
1853:)
1850:q
1841:p
1835:(
1832:(
1810:)
1807:)
1804:)
1801:r
1795:p
1792:(
1786:)
1783:q
1777:p
1774:(
1771:(
1765:)
1762:)
1759:r
1753:q
1750:(
1744:p
1741:(
1738:(
1716:)
1713:)
1710:p
1704:q
1701:(
1695:p
1692:(
1678:2
1664:A
1658:A
1645:2
1618:H
1602:2
1590:2
1573:)
1561:(
1555:)
1537:(
1516:)
1513:)
1501:(
1495:)
1483:(
1480:(
1474:)
1471:)
1459:(
1450:(
1429:)
1417:(
1390:2
1361:)
1358:p
1352:q
1349:(
1343:)
1340:q
1331:p
1325:(
1304:)
1301:)
1298:r
1292:p
1289:(
1283:)
1280:q
1274:p
1271:(
1268:(
1262:)
1259:)
1256:r
1250:q
1247:(
1241:p
1238:(
1217:)
1214:p
1208:q
1205:(
1199:p
1176:)
1173:p
1167:q
1164:(
1158:)
1155:q
1146:p
1140:(
1116:p
1113:q
1110:C
1107:q
1104:N
1101:p
1098:N
1095:C
1092:C
1076:2
1054:a
1042:a
1020:a
1014:a
986:)
983:b
974:a
968:(
962:)
959:a
953:b
950:(
928:)
925:)
922:a
916:d
913:(
907:b
904:(
898:)
895:)
892:a
886:b
883:(
877:d
874:(
852:)
849:)
846:a
840:c
837:(
831:)
828:b
822:c
819:(
816:(
810:)
807:)
804:a
798:b
795:(
789:c
786:(
764:)
761:a
755:b
752:(
746:a
648:y
645:t
642:P
636:y
633:x
630:P
627:x
604:)
601:y
598:t
595:P
589:y
586:x
583:P
580:x
574:(
571:y
330:)
324:(
319:)
315:(
311:.
297:.
150:I
125:E
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.