5530:
2245:
The fixed-point operations that we defined so far iterate the inductive definitions of the predicates mentioned in the formula indefinitely, until a fixed point is reached. In implementations, it may be necessary to bound the number of iterations to limit the computation time. The resulting operators
1199:
This inflationary fixed-point agrees with the least-fixed point where the latter is defined. Although at first glance it seems as if inflationary fixed-point logic should be more expressive than least fixed-point logic since it supports a wider range of fixed-point arguments, in fact, every
1216:
While all the fixed-point operators introduced so far iterated only on the definition of a single predicate, many computer programs are more naturally thought of as iterating over several predicates simultaneously. By either increasing the
2228:
1221:
of the fixed-point operators or by nesting them, every simultaneous least, inflationary or partial fixed-point can in fact be expressed using the corresponding single-iteration constructions discussed above.
2660:
2075:
1984:
1123:
1078:
2124:
1695:
1194:
552:
2477:
2556:
1865:
1350:
103:
1263:
428:
1784:
3299:
3234:
3180:
3085:
3036:
2949:
2395:
2292:
482:
2512:
2433:
2027:
1904:
1582:
1553:
1524:
1495:
1466:
1437:
1408:
1379:
901:
305:
276:
247:
218:
169:
2687:
761:
2754:
2734:
859:
821:(that is, occurrences preceded by an even number of negations). This guarantees monotonicity of the fixed-point construction (That is, if the second order variable is
2800:
1732:
1627:
715:
626:
589:
2868:
1810:
2714:
962:
935:
788:
3114:
2978:
2901:
2833:
2350:
2321:
358:
1033:
1013:
325:
189:
682:
809:
Since the iterated predicates involved in calculating the partial fixed point are not in general monotone, the fixed-point may not always exist. FO(LFP,X),
3909:
2129:
4584:
4667:
3808:
2561:
3576:
Yuri
Gurevich and Saharon Shelah, Fixed-pointed extension of first order logic, Annals of Pure and Applied Logic 32 (1986) 265--280.
27:
are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by
4981:
5139:
3748:
3927:
4994:
4317:
4999:
4989:
4726:
4579:
3932:
3544:
2035:
1944:
1083:
1038:
3923:
2246:
are also of interest from a theoretical point of view since they can also be used to characterise complexity classes.
2084:
1636:
983:
The expressivity of least-fixed point logic coincides exactly with the expressivity of the database querying language
5135:
3769:
3460:
3351:
4477:
1128:
5232:
4976:
3801:
487:
5554:
4537:
4230:
2438:
3971:
987:, showing that, on ordered structures, Datalog can express exactly those queries executable in polynomial time.
5493:
5195:
4958:
4953:
4778:
4199:
3883:
3619:
1941:) is defined as FO(TC,X) where the transitive closure operator is deterministic. This means that when we apply
1929:. This characterisation is a crucial part of Immerman's proof that NL is closed under complement (NL = co-NL).
1245:
using first-order connectives and predicates, second-order variables as well as a transitive closure operator
5488:
5271:
5188:
4901:
4832:
4709:
3951:
28:
2517:
5413:
5239:
4925:
4559:
4158:
1815:
1268:
88:
5291:
5286:
4896:
4635:
4564:
3893:
3794:
1248:
5220:
4810:
4204:
4172:
3863:
995:
Another way to ensure the monotonicity of the fixed-point construction is by only adding new tuples to
387:
5510:
5459:
5356:
4854:
4815:
4292:
3937:
3381:
Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on
Principles of Programming Languages - POPL '79
1737:
813:, is the set of formulas in FO(PFP,X) where the partial fixed point is taken only over such formulas
3966:
3527:
3245:
3187:
3121:
3045:
2986:
2909:
2355:
2252:
433:
5564:
5559:
5351:
5281:
4820:
4672:
4655:
4378:
3858:
2482:
2403:
5183:
5160:
5121:
5007:
4948:
4594:
4514:
4358:
4302:
3915:
32:
1997:
1874:
1558:
1529:
1500:
1471:
1442:
1413:
1384:
1355:
864:
281:
252:
223:
194:
108:
5473:
5200:
5178:
5145:
5038:
4884:
4869:
4842:
4793:
4677:
4612:
4437:
4403:
4398:
4272:
4103:
4080:
3522:
3323:
2665:
732:
43:
2739:
2719:
828:
5403:
5256:
5048:
4766:
4502:
4408:
4267:
4252:
4133:
4108:
2763:
1704:
1594:
687:
598:
561:
3517:
Vardi, Moshe Y. (1982). "The complexity of relational query languages (Extended
Abstract)".
2838:
2323:
is a (class of) functions from integers to integers, and for different classes of functions
1789:
1230:
Rather than allow induction over arbitrary predicates, transitive closure logic allows only
5376:
5338:
5215:
5019:
4859:
4783:
4761:
4589:
4547:
4446:
4413:
4277:
4065:
3976:
2692:
940:
913:
766:
3090:
2954:
2877:
2809:
2326:
2297:
793:
It has been proven that on ordered finite structures, a property is expressible in FO(PFP,
8:
5505:
5396:
5381:
5361:
5318:
5205:
5155:
5081:
5026:
4963:
4756:
4751:
4699:
4467:
4456:
4128:
4028:
3956:
3947:
3943:
3878:
3873:
337:
5534:
5303:
5266:
5251:
5244:
5227:
5031:
5013:
4879:
4805:
4788:
4741:
4554:
4463:
4297:
4282:
4242:
4194:
4179:
4167:
4123:
4098:
3868:
3817:
3625:
3550:
3466:
3394:
1231:
1018:
998:
310:
174:
82:
20:
4487:
3502:
3485:
3343:
633:
5529:
5469:
5276:
5086:
5076:
4968:
4849:
4684:
4660:
4441:
4425:
4330:
4307:
4153:
4118:
4013:
3848:
3775:
3765:
3744:
3664:
3615:
3540:
3470:
3456:
3357:
3347:
78:
63:
3519:
Proceedings of the fourteenth annual ACM symposium on Theory of computing - STOC '82
5483:
5478:
5371:
5328:
5150:
5111:
5106:
5091:
4917:
4874:
4771:
4569:
4519:
4093:
4055:
3736:
3656:
3629:
3607:
3604:
Proceedings of the fifteenth annual ACM symposium on Theory of computing - STOC '83
3554:
3532:
3497:
3448:
3398:
3384:
3339:
3327:
5464:
5454:
5408:
5391:
5346:
5308:
5210:
5130:
4937:
4864:
4837:
4825:
4731:
4645:
4619:
4574:
4542:
4343:
4145:
4088:
4038:
4003:
3961:
3039:
2078:
1926:
3445:[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science
2951:
to be the FO-formulae with an iteration operator whose exponent is in the class
5449:
5428:
5386:
5366:
5261:
5116:
4714:
4704:
4694:
4689:
4623:
4497:
4373:
4262:
4257:
4235:
3836:
3237:
2558:. We first need to define quantifier blocks (QB), a quantifier block is a list
2234:
977:
51:
3740:
2223:{\displaystyle \psi (u,v)=\phi (u,v)\wedge \forall x(x=v\vee \neg \phi (u,x))}
790:
s, so with a polynomial-space counter we can check if there is a loop or not.
5548:
5423:
5101:
4608:
4393:
4383:
4353:
4338:
4008:
3779:
3668:
3440:
3361:
965:
3452:
5323:
5170:
5071:
5063:
4943:
4891:
4800:
4736:
4719:
4650:
4509:
4368:
4070:
3853:
3599:
3611:
3536:
3389:
3376:
5433:
5313:
4492:
4482:
4429:
4113:
4033:
4018:
3898:
3843:
969:
4363:
4218:
4189:
3995:
47:
54:
suggested fixed-point logic as an expressive database query language.
5515:
5418:
4471:
4388:
4348:
4312:
4248:
4060:
4050:
4023:
3786:
3759:
3644:
3441:"Fixpoint extensions of first-order logic and datalog-like languages"
3660:
46:
in 1974, and it was introduced to computer scientists in 1979, when
5500:
5298:
4746:
4451:
4045:
5096:
3888:
984:
36:
3302:
2655:{\displaystyle (Q_{1}x_{1},\phi _{1})...(Q_{k}x_{k},\phi _{k})}
2233:
Over ordered structures, FO characterises the complexity class
1925:
Over ordered structures, FO characterises the complexity class
1015:
at every stage of iteration, without removing tuples for which
964:
iterations. The
Immerman-Vardi theorem, shown independently by
906:
Due to monotonicity, we only add vectors to the truth table of
798:
4640:
3986:
3831:
3735:. Perspectives in Mathematical Logic (2 ed.). Springer.
1218:
42:
Least fixed-point logic was first studied systematically by
937:
possible vectors we will always find a fixed point before
1932:
3645:"Nondeterministic Space is Closed under Complementation"
3606:. New York, New York, USA: ACM Press. pp. 347â354.
1410:
are tuples of pairwise distinct first-order variables,
595:). Then, either there is a fixed point, or the list of
3248:
3190:
3124:
3093:
3048:
2989:
2957:
2912:
2880:
2841:
2812:
2766:
2742:
2722:
2695:
2668:
2564:
2520:
2485:
2441:
2406:
2358:
2329:
2300:
2255:
2132:
2087:
2038:
2000:
1947:
1877:
1818:
1792:
1740:
1707:
1639:
1597:
1561:
1532:
1503:
1474:
1445:
1416:
1387:
1358:
1271:
1251:
1131:
1086:
1041:
1021:
1001:
943:
916:
867:
831:
769:
735:
690:
636:
601:
564:
490:
436:
390:
340:
313:
284:
255:
226:
197:
177:
111:
91:
3332:
2835:time. One should pay attention that here there are
3486:"Relational queries computable in polynomial time"
3293:
3228:
3174:
3108:
3079:
3030:
2972:
2943:
2895:
2862:
2827:
2794:
2748:
2728:
2708:
2681:
2654:
2550:
2506:
2471:
2427:
2389:
2344:
2315:
2286:
2222:
2118:
2069:
2021:
1978:
1898:
1859:
1804:
1778:
1726:
1689:
1621:
1576:
1547:
1518:
1489:
1460:
1431:
1402:
1373:
1344:
1257:
1188:
1117:
1072:
1027:
1007:
956:
929:
895:
853:
782:
755:
709:
676:
620:
583:
546:
476:
422:
352:
319:
299:
270:
241:
212:
183:
163:
97:
2070:{\displaystyle \operatorname {DTC} (\phi _{u,v})}
1979:{\displaystyle \operatorname {DTC} (\phi _{u,v})}
1118:{\displaystyle \operatorname {PFP} (\psi _{P,x})}
1073:{\displaystyle \operatorname {IFP} (\phi _{P,x})}
990:
5546:
2119:{\displaystyle \operatorname {TC} (\psi _{u,v})}
1690:{\displaystyle {\mathsf {TC}}(\phi _{u,v})(x,y)}
721:if there is a fixed point, else as false. Since
3383:. New York, New York, USA: ACM Press: 110â119.
3730:
3438:
2874:variables and each of those variable are used
1189:{\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}
684:is defined as the value of the fixed point of
3802:
3731:Ebbinghaus, Heinz-Dieter; Flum, Jörg (1999).
3328:"Elementary Induction on Abstract Structures"
3600:"Languages which capture complexity classes"
3521:. New York, NY, USA: ACM. pp. 137â146.
2802:the iteration operator, which is defined as
2352:we will obtain different complexity classes
547:{\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}
57:
3447:. IEEE Comput. Soc. Press. pp. 71â79.
3375:Aho, Alfred V.; Ullman, Jeffrey D. (1979).
3322:
3305:. It is also another way to write FO(PFP).
2472:{\displaystyle (\forall x(P\Rightarrow Q))}
2249:We will define first-order with iteration,
1225:
3994:
3809:
3795:
3377:"Universality of data retrieval languages"
3240:. It is also another way to write FO(IFP).
2980:, and we obtain the following equalities:
817:that only contain positive occurrences of
804:
591:substituted for the second-order variable
85:as well as a partial fixed point operator
3526:
3501:
3388:
3374:
2760:is a quantifiers block then we will call
1211:
3642:
3597:
3483:
384:as variables. We can iteratively define
5547:
3816:
3254:
3251:
3196:
3193:
3130:
3127:
3054:
3051:
2995:
2992:
2918:
2915:
2689:s are quantifier-free FO-formulae and
2551:{\displaystyle (\exists x(P\wedge Q))}
2364:
2361:
2261:
2258:
1933:Deterministic transitive closure logic
1645:
1642:
79:first-order connectives and predicates
3790:
3593:
3591:
3516:
1241:) is the set of formulas formed from
1035:no longer holds. Formally, we define
73:) is the set of formulas formed from
3757:
1860:{\displaystyle \phi (z_{i},z_{i+1})}
1345:{\displaystyle {\vec {s}}{\vec {t}}}
368:be a second-order variable of arity
249:a tuple of terms and the lengths of
98:{\displaystyle \operatorname {PFP} }
1871:is a formula written in FO(TC) and
1468:tuples of terms and the lengths of
1258:{\displaystyle \operatorname {TC} }
13:
3588:
2870:quantifiers in the list, but only
2743:
2723:
2524:
2489:
2445:
2410:
2196:
2175:
1265:used to form formulas of the form
220:a tuple of first-order variables,
105:used to form formulas of the form
14:
5576:
3585:Ebbinghaus and Flum, pp. 179, 193
3439:Abiteboul, S.; Vianu, V. (1989).
1204:)-formula is equivalent to an FO(
5528:
423:{\displaystyle (P_{i})_{i\in N}}
3711:
3702:
3693:
3684:
3675:
3636:
3579:
3570:
2400:In this section we will write
1779:{\displaystyle z_{1}=x,z_{n}=y}
376:be an FO(PFP,X) function using
3561:
3510:
3477:
3432:
3423:
3414:
3405:
3368:
3316:
3294:{\displaystyle {\mathsf {FO}}}
3288:
3281:
3275:
3259:
3229:{\displaystyle {\mathsf {FO}}}
3223:
3218:
3212:
3201:
3175:{\displaystyle {\mathsf {FO}}}
3169:
3164:
3158:
3151:
3138:
3135:
3103:
3097:
3080:{\displaystyle {\mathsf {FO}}}
3074:
3071:
3065:
3059:
3031:{\displaystyle {\mathsf {FO}}}
3025:
3016:
3003:
3000:
2967:
2961:
2944:{\displaystyle {\mathsf {FO}}}
2938:
2935:
2929:
2923:
2890:
2884:
2857:
2851:
2822:
2816:
2787:
2781:
2774:
2767:
2649:
2613:
2601:
2565:
2545:
2542:
2530:
2521:
2498:
2486:
2466:
2463:
2457:
2451:
2442:
2419:
2407:
2390:{\displaystyle {\mathsf {FO}}}
2384:
2381:
2375:
2369:
2339:
2333:
2310:
2304:
2287:{\displaystyle {\mathsf {FO}}}
2281:
2278:
2272:
2266:
2217:
2214:
2202:
2181:
2169:
2157:
2148:
2136:
2113:
2094:
2064:
2045:
2016:
2004:
1973:
1954:
1893:
1881:
1854:
1822:
1721:
1708:
1684:
1672:
1669:
1650:
1587:TC is defined as follows: Let
1568:
1539:
1510:
1481:
1452:
1423:
1394:
1365:
1336:
1324:
1315:
1301:
1286:
1272:
1183:
1177:
1168:
1156:
1147:
1135:
1112:
1093:
1067:
1048:
991:Inflationary fixed-point logic
890:
884:
848:
842:
704:
691:
671:
668:
662:
637:
615:
602:
541:
516:
507:
501:
477:{\displaystyle P_{0}(x)=false}
453:
447:
405:
391:
291:
262:
233:
204:
155:
146:
126:
112:
1:
5489:History of mathematical logic
3724:
3503:10.1016/s0019-9958(86)80029-8
3344:10.1016/s0049-237x(08)x7092-2
2507:{\displaystyle (\exists xP)Q}
2428:{\displaystyle (\forall xP)Q}
2240:
29:descriptive complexity theory
16:Concept in mathematical logic
5414:Primitive recursive function
797:) if and only if it lies in
191:is a second-order variable,
7:
3567:Ebbinghaus and Flum, p. 242
3420:Ebbinghaus and Flum, p. 121
3411:Ebbinghaus and Flum, p. 121
1990:, there exists at most one
980:on all ordered structures.
910:, and since there are only
307:coincide with the arity of
10:
5581:
4478:SchröderâBernstein theorem
4205:Monadic predicate calculus
3864:Foundations of mathematics
3087:is FO-uniform AC of depth
2022:{\displaystyle \phi (u,v)}
1899:{\displaystyle \phi (x,y)}
1591:be a positive integer and
1577:{\displaystyle {\vec {t}}}
1548:{\displaystyle {\vec {s}}}
1519:{\displaystyle {\vec {y}}}
1490:{\displaystyle {\vec {x}}}
1461:{\displaystyle {\vec {s}}}
1432:{\displaystyle {\vec {t}}}
1403:{\displaystyle {\vec {y}}}
1374:{\displaystyle {\vec {x}}}
1234:to be expressed directly.
896:{\displaystyle P_{i+1}(x)}
725:s are properties of arity
300:{\displaystyle {\vec {t}}}
271:{\displaystyle {\vec {x}}}
242:{\displaystyle {\vec {t}}}
213:{\displaystyle {\vec {x}}}
164:{\displaystyle {\vec {t}}}
31:and their relationship to
5524:
5511:Philosophy of mathematics
5460:Automated theorem proving
5442:
5337:
5169:
5062:
4914:
4631:
4607:
4585:Von NeumannâBernaysâGödel
4530:
4424:
4328:
4226:
4217:
4144:
4079:
3985:
3907:
3824:
3741:10.1007/978-3-662-03182-7
3649:SIAM Journal on Computing
2682:{\displaystyle \phi _{i}}
1906:means that the variables
756:{\displaystyle 2^{n^{k}}}
58:Partial fixed-point logic
3309:
2749:{\displaystyle \exists }
2729:{\displaystyle \forall }
1226:Transitive closure logic
854:{\displaystyle P_{i}(x)}
33:database query languages
5161:Self-verifying theories
4982:Tarski's axiomatization
3933:Tarski's undefinability
3928:incompleteness theorems
3758:Neil, Immerman (1999).
3643:Immerman, Neil (1988).
3598:Immerman, Neil (1983).
3490:Information and Control
3484:Immerman, Neil (1986).
3453:10.1109/lics.1989.39160
3324:Moschovakis, Yiannis N.
3038:is equal to FO-uniform
2795:{\displaystyle ^{t(n)}}
1986:, we know that for all
1727:{\displaystyle (z_{i})}
1697:is true if there exist
1622:{\displaystyle u,v,x,y}
811:least fixed-point logic
805:Least fixed-point logic
710:{\displaystyle (P_{i})}
621:{\displaystyle (P_{i})}
584:{\displaystyle P_{i-1}}
5555:Descriptive complexity
5535:Mathematics portal
5146:Proof of impossibility
4794:propositional variable
4104:Propositional calculus
3761:Descriptive complexity
3295:
3230:
3176:
3110:
3081:
3032:
2974:
2945:
2897:
2864:
2863:{\displaystyle k*t(n)}
2829:
2796:
2750:
2730:
2710:
2683:
2656:
2552:
2508:
2473:
2429:
2391:
2346:
2317:
2288:
2224:
2120:
2071:
2023:
1980:
1900:
1861:
1806:
1805:{\displaystyle i<n}
1780:
1728:
1691:
1623:
1578:
1549:
1520:
1491:
1462:
1433:
1404:
1375:
1346:
1259:
1212:Simultaneous induction
1190:
1119:
1074:
1029:
1009:
958:
931:
897:
855:
784:
757:
711:
678:
622:
585:
548:
478:
424:
354:
321:
301:
272:
243:
214:
185:
165:
99:
83:second-order variables
44:Yiannis N. Moschovakis
5404:Kolmogorov complexity
5357:Computably enumerable
5257:Model complete theory
5049:Principia Mathematica
4109:Propositional formula
3938:BanachâTarski paradox
3717:Immerman 1999, p. 161
3612:10.1145/800061.808765
3537:10.1145/800070.802186
3429:Immerman 1999, p. 161
3390:10.1145/567752.567763
3296:
3231:
3177:
3111:
3082:
3033:
2975:
2946:
2898:
2865:
2830:
2797:
2751:
2731:
2711:
2709:{\displaystyle Q_{i}}
2684:
2657:
2553:
2509:
2474:
2430:
2392:
2347:
2318:
2289:
2225:
2121:
2072:
2024:
1981:
1901:
1862:
1807:
1781:
1729:
1701:vectors of variables
1692:
1624:
1579:
1550:
1521:
1492:
1463:
1434:
1405:
1376:
1347:
1260:
1191:
1120:
1075:
1030:
1010:
959:
957:{\displaystyle n^{k}}
932:
930:{\displaystyle n^{k}}
898:
856:
785:
783:{\displaystyle P_{i}}
758:
712:
679:
623:
586:
549:
479:
425:
355:
322:
302:
273:
244:
215:
186:
166:
100:
5352:ChurchâTuring thesis
5339:Computability theory
4548:continuum hypothesis
4066:Square of opposition
3924:Gödel's completeness
3708:Immerman 1999, p. 58
3699:Immerman 1999, p. 84
3690:Immerman 1999, p. 82
3681:Immerman 1999, p. 63
3246:
3188:
3122:
3109:{\displaystyle t(n)}
3091:
3046:
2987:
2973:{\displaystyle t(n)}
2955:
2910:
2896:{\displaystyle t(n)}
2878:
2839:
2828:{\displaystyle t(n)}
2810:
2764:
2740:
2720:
2693:
2666:
2562:
2518:
2483:
2439:
2404:
2356:
2345:{\displaystyle t(n)}
2327:
2316:{\displaystyle t(n)}
2298:
2253:
2130:
2085:
2036:
2032:We can suppose that
1998:
1945:
1875:
1816:
1790:
1738:
1705:
1637:
1595:
1559:
1530:
1501:
1472:
1443:
1414:
1385:
1356:
1269:
1249:
1129:
1084:
1039:
1019:
999:
972:, shows that FO(LFP,
941:
914:
865:
829:
767:
733:
729:, there are at most
688:
634:
599:
562:
488:
434:
388:
338:
311:
282:
253:
224:
195:
175:
109:
89:
64:relational signature
5506:Mathematical object
5397:P versus NP problem
5362:Computable function
5156:Reverse mathematics
5082:Logical consequence
4959:primitive recursive
4954:elementary function
4727:Free/bound variable
4580:TarskiâGrothendieck
4099:Logical connectives
4029:Logical equivalence
3879:Logical consequence
3733:Finite Model Theory
1232:transitive closures
353:{\displaystyle x,y}
35:, in particular to
5304:Transfer principle
5267:Semantics of logic
5252:Categorical theory
5228:Non-standard model
4742:Logical connective
3869:Information theory
3818:Mathematical logic
3291:
3226:
3172:
3106:
3077:
3028:
2970:
2941:
2906:We can now define
2893:
2860:
2825:
2792:
2746:
2726:
2706:
2679:
2652:
2548:
2504:
2469:
2425:
2387:
2342:
2313:
2284:
2220:
2116:
2067:
2019:
1976:
1896:
1857:
1802:
1776:
1724:
1687:
1619:
1574:
1545:
1516:
1487:
1458:
1429:
1400:
1371:
1342:
1255:
1186:
1115:
1070:
1025:
1005:
954:
927:
893:
851:
780:
753:
707:
674:
618:
581:
544:
474:
420:
350:
317:
297:
268:
239:
210:
181:
161:
95:
25:fixed-point logics
21:mathematical logic
5542:
5541:
5474:Abstract category
5277:Theories of truth
5087:Rule of inference
5077:Natural deduction
5058:
5057:
4603:
4602:
4308:Cartesian product
4213:
4212:
4119:Many-valued logic
4094:Boolean functions
3977:Russell's paradox
3952:diagonal argument
3849:First-order logic
3750:978-3-662-03184-1
1571:
1542:
1513:
1484:
1455:
1426:
1397:
1368:
1339:
1327:
1304:
1289:
1028:{\displaystyle P}
1008:{\displaystyle P}
320:{\displaystyle P}
294:
265:
236:
207:
184:{\displaystyle P}
158:
129:
5572:
5533:
5532:
5484:History of logic
5479:Category of sets
5372:Decision problem
5151:Ordinal analysis
5092:Sequent calculus
4990:Boolean algebras
4930:
4929:
4904:
4875:logical/constant
4629:
4628:
4615:
4538:ZermeloâFraenkel
4289:Set operations:
4224:
4223:
4161:
3992:
3991:
3972:LöwenheimâSkolem
3859:Formal semantics
3811:
3804:
3797:
3788:
3787:
3783:
3754:
3718:
3715:
3709:
3706:
3700:
3697:
3691:
3688:
3682:
3679:
3673:
3672:
3640:
3634:
3633:
3595:
3586:
3583:
3577:
3574:
3568:
3565:
3559:
3558:
3530:
3514:
3508:
3507:
3505:
3481:
3475:
3474:
3436:
3430:
3427:
3421:
3418:
3412:
3409:
3403:
3402:
3392:
3372:
3366:
3365:
3320:
3300:
3298:
3297:
3292:
3287:
3286:
3285:
3284:
3258:
3257:
3235:
3233:
3232:
3227:
3222:
3221:
3200:
3199:
3181:
3179:
3178:
3173:
3168:
3167:
3134:
3133:
3115:
3113:
3112:
3107:
3086:
3084:
3083:
3078:
3058:
3057:
3037:
3035:
3034:
3029:
3024:
3023:
2999:
2998:
2979:
2977:
2976:
2971:
2950:
2948:
2947:
2942:
2922:
2921:
2902:
2900:
2899:
2894:
2873:
2869:
2867:
2866:
2861:
2834:
2832:
2831:
2826:
2805:
2801:
2799:
2798:
2793:
2791:
2790:
2759:
2755:
2753:
2752:
2747:
2735:
2733:
2732:
2727:
2715:
2713:
2712:
2707:
2705:
2704:
2688:
2686:
2685:
2680:
2678:
2677:
2661:
2659:
2658:
2653:
2648:
2647:
2635:
2634:
2625:
2624:
2600:
2599:
2587:
2586:
2577:
2576:
2557:
2555:
2554:
2549:
2513:
2511:
2510:
2505:
2478:
2476:
2475:
2470:
2434:
2432:
2431:
2426:
2396:
2394:
2393:
2388:
2368:
2367:
2351:
2349:
2348:
2343:
2322:
2320:
2319:
2314:
2293:
2291:
2290:
2285:
2265:
2264:
2229:
2227:
2226:
2221:
2125:
2123:
2122:
2117:
2112:
2111:
2076:
2074:
2073:
2068:
2063:
2062:
2028:
2026:
2025:
2020:
1993:
1989:
1985:
1983:
1982:
1977:
1972:
1971:
1921:
1917:
1914:are replaced by
1913:
1909:
1905:
1903:
1902:
1897:
1870:
1866:
1864:
1863:
1858:
1853:
1852:
1834:
1833:
1811:
1809:
1808:
1803:
1785:
1783:
1782:
1777:
1769:
1768:
1750:
1749:
1733:
1731:
1730:
1725:
1720:
1719:
1700:
1696:
1694:
1693:
1688:
1668:
1667:
1649:
1648:
1633:variables. Then
1632:
1628:
1626:
1625:
1620:
1590:
1583:
1581:
1580:
1575:
1573:
1572:
1564:
1554:
1552:
1551:
1546:
1544:
1543:
1535:
1525:
1523:
1522:
1517:
1515:
1514:
1506:
1496:
1494:
1493:
1488:
1486:
1485:
1477:
1467:
1465:
1464:
1459:
1457:
1456:
1448:
1438:
1436:
1435:
1430:
1428:
1427:
1419:
1409:
1407:
1406:
1401:
1399:
1398:
1390:
1380:
1378:
1377:
1372:
1370:
1369:
1361:
1351:
1349:
1348:
1343:
1341:
1340:
1332:
1329:
1328:
1320:
1308:
1307:
1306:
1305:
1297:
1291:
1290:
1282:
1264:
1262:
1261:
1256:
1195:
1193:
1192:
1187:
1124:
1122:
1121:
1116:
1111:
1110:
1079:
1077:
1076:
1071:
1066:
1065:
1034:
1032:
1031:
1026:
1014:
1012:
1011:
1006:
976:) characterises
963:
961:
960:
955:
953:
952:
936:
934:
933:
928:
926:
925:
909:
902:
900:
899:
894:
883:
882:
860:
858:
857:
852:
841:
840:
824:
820:
816:
789:
787:
786:
781:
779:
778:
762:
760:
759:
754:
752:
751:
750:
749:
728:
724:
720:
716:
714:
713:
708:
703:
702:
683:
681:
680:
677:{\displaystyle }
675:
655:
654:
627:
625:
624:
619:
614:
613:
594:
590:
588:
587:
582:
580:
579:
557:
553:
551:
550:
545:
534:
533:
500:
499:
483:
481:
480:
475:
446:
445:
429:
427:
426:
421:
419:
418:
403:
402:
383:
379:
375:
371:
367:
363:
359:
357:
356:
351:
333:
326:
324:
323:
318:
306:
304:
303:
298:
296:
295:
287:
277:
275:
274:
269:
267:
266:
258:
248:
246:
245:
240:
238:
237:
229:
219:
217:
216:
211:
209:
208:
200:
190:
188:
187:
182:
170:
168:
167:
162:
160:
159:
151:
139:
138:
131:
130:
122:
104:
102:
101:
96:
5580:
5579:
5575:
5574:
5573:
5571:
5570:
5569:
5565:Predicate logic
5560:Database theory
5545:
5544:
5543:
5538:
5527:
5520:
5465:Category theory
5455:Algebraic logic
5438:
5409:Lambda calculus
5347:Church encoding
5333:
5309:Truth predicate
5165:
5131:Complete theory
5054:
4923:
4919:
4915:
4910:
4902:
4622: and
4618:
4613:
4599:
4575:New Foundations
4543:axiom of choice
4526:
4488:Gödel numbering
4428: and
4420:
4324:
4209:
4159:
4140:
4089:Boolean algebra
4075:
4039:Equiconsistency
4004:Classical logic
3981:
3962:Halting problem
3950: and
3926: and
3914: and
3913:
3908:Theorems (
3903:
3820:
3815:
3772:
3751:
3727:
3722:
3721:
3716:
3712:
3707:
3703:
3698:
3694:
3689:
3685:
3680:
3676:
3661:10.1137/0217058
3641:
3637:
3622:
3596:
3589:
3584:
3580:
3575:
3571:
3566:
3562:
3547:
3528:10.1.1.331.6045
3515:
3511:
3496:(1â3): 86â104.
3482:
3478:
3463:
3437:
3433:
3428:
3424:
3419:
3415:
3410:
3406:
3373:
3369:
3354:
3321:
3317:
3312:
3271:
3267:
3266:
3262:
3250:
3249:
3247:
3244:
3243:
3208:
3204:
3192:
3191:
3189:
3186:
3185:
3182:is equal to NC.
3154:
3150:
3126:
3125:
3123:
3120:
3119:
3092:
3089:
3088:
3050:
3049:
3047:
3044:
3043:
3019:
3015:
2991:
2990:
2988:
2985:
2984:
2956:
2953:
2952:
2914:
2913:
2911:
2908:
2907:
2879:
2876:
2875:
2871:
2840:
2837:
2836:
2811:
2808:
2807:
2803:
2777:
2773:
2765:
2762:
2761:
2757:
2741:
2738:
2737:
2721:
2718:
2717:
2700:
2696:
2694:
2691:
2690:
2673:
2669:
2667:
2664:
2663:
2643:
2639:
2630:
2626:
2620:
2616:
2595:
2591:
2582:
2578:
2572:
2568:
2563:
2560:
2559:
2519:
2516:
2515:
2484:
2481:
2480:
2440:
2437:
2436:
2405:
2402:
2401:
2360:
2359:
2357:
2354:
2353:
2328:
2325:
2324:
2299:
2296:
2295:
2257:
2256:
2254:
2251:
2250:
2243:
2131:
2128:
2127:
2101:
2097:
2086:
2083:
2082:
2079:syntactic sugar
2052:
2048:
2037:
2034:
2033:
1999:
1996:
1995:
1991:
1987:
1961:
1957:
1946:
1943:
1942:
1935:
1919:
1915:
1911:
1907:
1876:
1873:
1872:
1868:
1867:is true. Here,
1842:
1838:
1829:
1825:
1817:
1814:
1813:
1791:
1788:
1787:
1764:
1760:
1745:
1741:
1739:
1736:
1735:
1715:
1711:
1706:
1703:
1702:
1698:
1657:
1653:
1641:
1640:
1638:
1635:
1634:
1630:
1596:
1593:
1592:
1588:
1563:
1562:
1560:
1557:
1556:
1534:
1533:
1531:
1528:
1527:
1505:
1504:
1502:
1499:
1498:
1476:
1475:
1473:
1470:
1469:
1447:
1446:
1444:
1441:
1440:
1418:
1417:
1415:
1412:
1411:
1389:
1388:
1386:
1383:
1382:
1360:
1359:
1357:
1354:
1353:
1331:
1330:
1319:
1318:
1296:
1295:
1281:
1280:
1279:
1275:
1270:
1267:
1266:
1250:
1247:
1246:
1228:
1214:
1130:
1127:
1126:
1100:
1096:
1085:
1082:
1081:
1055:
1051:
1040:
1037:
1036:
1020:
1017:
1016:
1000:
997:
996:
993:
948:
944:
942:
939:
938:
921:
917:
915:
912:
911:
907:
872:
868:
866:
863:
862:
861:always implies
836:
832:
830:
827:
826:
822:
818:
814:
807:
774:
770:
768:
765:
764:
763:values for the
745:
741:
740:
736:
734:
731:
730:
726:
722:
718:
698:
694:
689:
686:
685:
644:
640:
635:
632:
631:
609:
605:
600:
597:
596:
592:
569:
565:
563:
560:
559:
555:
523:
519:
495:
491:
489:
486:
485:
441:
437:
435:
432:
431:
408:
404:
398:
394:
389:
386:
385:
381:
377:
373:
369:
365:
361:
339:
336:
335:
334:be an integer,
331:
312:
309:
308:
286:
285:
283:
280:
279:
257:
256:
254:
251:
250:
228:
227:
225:
222:
221:
199:
198:
196:
193:
192:
176:
173:
172:
150:
149:
121:
120:
119:
115:
110:
107:
106:
90:
87:
86:
60:
17:
12:
11:
5:
5578:
5568:
5567:
5562:
5557:
5540:
5539:
5525:
5522:
5521:
5519:
5518:
5513:
5508:
5503:
5498:
5497:
5496:
5486:
5481:
5476:
5467:
5462:
5457:
5452:
5450:Abstract logic
5446:
5444:
5440:
5439:
5437:
5436:
5431:
5429:Turing machine
5426:
5421:
5416:
5411:
5406:
5401:
5400:
5399:
5394:
5389:
5384:
5379:
5369:
5367:Computable set
5364:
5359:
5354:
5349:
5343:
5341:
5335:
5334:
5332:
5331:
5326:
5321:
5316:
5311:
5306:
5301:
5296:
5295:
5294:
5289:
5284:
5274:
5269:
5264:
5262:Satisfiability
5259:
5254:
5249:
5248:
5247:
5237:
5236:
5235:
5225:
5224:
5223:
5218:
5213:
5208:
5203:
5193:
5192:
5191:
5186:
5179:Interpretation
5175:
5173:
5167:
5166:
5164:
5163:
5158:
5153:
5148:
5143:
5133:
5128:
5127:
5126:
5125:
5124:
5114:
5109:
5099:
5094:
5089:
5084:
5079:
5074:
5068:
5066:
5060:
5059:
5056:
5055:
5053:
5052:
5044:
5043:
5042:
5041:
5036:
5035:
5034:
5029:
5024:
5004:
5003:
5002:
5000:minimal axioms
4997:
4986:
4985:
4984:
4973:
4972:
4971:
4966:
4961:
4956:
4951:
4946:
4933:
4931:
4912:
4911:
4909:
4908:
4907:
4906:
4894:
4889:
4888:
4887:
4882:
4877:
4872:
4862:
4857:
4852:
4847:
4846:
4845:
4840:
4830:
4829:
4828:
4823:
4818:
4813:
4803:
4798:
4797:
4796:
4791:
4786:
4776:
4775:
4774:
4769:
4764:
4759:
4754:
4749:
4739:
4734:
4729:
4724:
4723:
4722:
4717:
4712:
4707:
4697:
4692:
4690:Formation rule
4687:
4682:
4681:
4680:
4675:
4665:
4664:
4663:
4653:
4648:
4643:
4638:
4632:
4626:
4609:Formal systems
4605:
4604:
4601:
4600:
4598:
4597:
4592:
4587:
4582:
4577:
4572:
4567:
4562:
4557:
4552:
4551:
4550:
4545:
4534:
4532:
4528:
4527:
4525:
4524:
4523:
4522:
4512:
4507:
4506:
4505:
4498:Large cardinal
4495:
4490:
4485:
4480:
4475:
4461:
4460:
4459:
4454:
4449:
4434:
4432:
4422:
4421:
4419:
4418:
4417:
4416:
4411:
4406:
4396:
4391:
4386:
4381:
4376:
4371:
4366:
4361:
4356:
4351:
4346:
4341:
4335:
4333:
4326:
4325:
4323:
4322:
4321:
4320:
4315:
4310:
4305:
4300:
4295:
4287:
4286:
4285:
4280:
4270:
4265:
4263:Extensionality
4260:
4258:Ordinal number
4255:
4245:
4240:
4239:
4238:
4227:
4221:
4215:
4214:
4211:
4210:
4208:
4207:
4202:
4197:
4192:
4187:
4182:
4177:
4176:
4175:
4165:
4164:
4163:
4150:
4148:
4142:
4141:
4139:
4138:
4137:
4136:
4131:
4126:
4116:
4111:
4106:
4101:
4096:
4091:
4085:
4083:
4077:
4076:
4074:
4073:
4068:
4063:
4058:
4053:
4048:
4043:
4042:
4041:
4031:
4026:
4021:
4016:
4011:
4006:
4000:
3998:
3989:
3983:
3982:
3980:
3979:
3974:
3969:
3964:
3959:
3954:
3942:Cantor's
3940:
3935:
3930:
3920:
3918:
3905:
3904:
3902:
3901:
3896:
3891:
3886:
3881:
3876:
3871:
3866:
3861:
3856:
3851:
3846:
3841:
3840:
3839:
3828:
3826:
3822:
3821:
3814:
3813:
3806:
3799:
3791:
3785:
3784:
3770:
3755:
3749:
3726:
3723:
3720:
3719:
3710:
3701:
3692:
3683:
3674:
3655:(5): 935â938.
3635:
3620:
3587:
3578:
3569:
3560:
3546:978-0897910705
3545:
3509:
3476:
3461:
3431:
3422:
3413:
3404:
3367:
3352:
3314:
3313:
3311:
3308:
3307:
3306:
3290:
3283:
3280:
3277:
3274:
3270:
3265:
3261:
3256:
3253:
3241:
3225:
3220:
3217:
3214:
3211:
3207:
3203:
3198:
3195:
3183:
3171:
3166:
3163:
3160:
3157:
3153:
3149:
3146:
3143:
3140:
3137:
3132:
3129:
3117:
3105:
3102:
3099:
3096:
3076:
3073:
3070:
3067:
3064:
3061:
3056:
3053:
3042:, and in fact
3027:
3022:
3018:
3014:
3011:
3008:
3005:
3002:
2997:
2994:
2969:
2966:
2963:
2960:
2940:
2937:
2934:
2931:
2928:
2925:
2920:
2917:
2892:
2889:
2886:
2883:
2859:
2856:
2853:
2850:
2847:
2844:
2824:
2821:
2818:
2815:
2789:
2786:
2783:
2780:
2776:
2772:
2769:
2745:
2725:
2703:
2699:
2676:
2672:
2651:
2646:
2642:
2638:
2633:
2629:
2623:
2619:
2615:
2612:
2609:
2606:
2603:
2598:
2594:
2590:
2585:
2581:
2575:
2571:
2567:
2547:
2544:
2541:
2538:
2535:
2532:
2529:
2526:
2523:
2503:
2500:
2497:
2494:
2491:
2488:
2468:
2465:
2462:
2459:
2456:
2453:
2450:
2447:
2444:
2424:
2421:
2418:
2415:
2412:
2409:
2386:
2383:
2380:
2377:
2374:
2371:
2366:
2363:
2341:
2338:
2335:
2332:
2312:
2309:
2306:
2303:
2283:
2280:
2277:
2274:
2271:
2268:
2263:
2260:
2242:
2239:
2219:
2216:
2213:
2210:
2207:
2204:
2201:
2198:
2195:
2192:
2189:
2186:
2183:
2180:
2177:
2174:
2171:
2168:
2165:
2162:
2159:
2156:
2153:
2150:
2147:
2144:
2141:
2138:
2135:
2115:
2110:
2107:
2104:
2100:
2096:
2093:
2090:
2066:
2061:
2058:
2055:
2051:
2047:
2044:
2041:
2018:
2015:
2012:
2009:
2006:
2003:
1975:
1970:
1967:
1964:
1960:
1956:
1953:
1950:
1934:
1931:
1895:
1892:
1889:
1886:
1883:
1880:
1856:
1851:
1848:
1845:
1841:
1837:
1832:
1828:
1824:
1821:
1801:
1798:
1795:
1786:, and for all
1775:
1772:
1767:
1763:
1759:
1756:
1753:
1748:
1744:
1723:
1718:
1714:
1710:
1686:
1683:
1680:
1677:
1674:
1671:
1666:
1663:
1660:
1656:
1652:
1647:
1644:
1629:be vectors of
1618:
1615:
1612:
1609:
1606:
1603:
1600:
1570:
1567:
1541:
1538:
1512:
1509:
1483:
1480:
1454:
1451:
1425:
1422:
1396:
1393:
1367:
1364:
1338:
1335:
1326:
1323:
1317:
1314:
1311:
1303:
1300:
1294:
1288:
1285:
1278:
1274:
1254:
1227:
1224:
1213:
1210:
1185:
1182:
1179:
1176:
1173:
1170:
1167:
1164:
1161:
1158:
1155:
1152:
1149:
1146:
1143:
1140:
1137:
1134:
1114:
1109:
1106:
1103:
1099:
1095:
1092:
1089:
1069:
1064:
1061:
1058:
1054:
1050:
1047:
1044:
1024:
1004:
992:
989:
951:
947:
924:
920:
892:
889:
886:
881:
878:
875:
871:
850:
847:
844:
839:
835:
806:
803:
777:
773:
748:
744:
739:
706:
701:
697:
693:
673:
670:
667:
664:
661:
658:
653:
650:
647:
643:
639:
617:
612:
608:
604:
578:
575:
572:
568:
543:
540:
537:
532:
529:
526:
522:
518:
515:
512:
509:
506:
503:
498:
494:
473:
470:
467:
464:
461:
458:
455:
452:
449:
444:
440:
417:
414:
411:
407:
401:
397:
393:
360:be vectors of
349:
346:
343:
316:
293:
290:
264:
261:
235:
232:
206:
203:
180:
157:
154:
148:
145:
142:
137:
134:
128:
125:
118:
114:
94:
59:
56:
52:Jeffrey Ullman
15:
9:
6:
4:
3:
2:
5577:
5566:
5563:
5561:
5558:
5556:
5553:
5552:
5550:
5537:
5536:
5531:
5523:
5517:
5514:
5512:
5509:
5507:
5504:
5502:
5499:
5495:
5492:
5491:
5490:
5487:
5485:
5482:
5480:
5477:
5475:
5471:
5468:
5466:
5463:
5461:
5458:
5456:
5453:
5451:
5448:
5447:
5445:
5441:
5435:
5432:
5430:
5427:
5425:
5424:Recursive set
5422:
5420:
5417:
5415:
5412:
5410:
5407:
5405:
5402:
5398:
5395:
5393:
5390:
5388:
5385:
5383:
5380:
5378:
5375:
5374:
5373:
5370:
5368:
5365:
5363:
5360:
5358:
5355:
5353:
5350:
5348:
5345:
5344:
5342:
5340:
5336:
5330:
5327:
5325:
5322:
5320:
5317:
5315:
5312:
5310:
5307:
5305:
5302:
5300:
5297:
5293:
5290:
5288:
5285:
5283:
5280:
5279:
5278:
5275:
5273:
5270:
5268:
5265:
5263:
5260:
5258:
5255:
5253:
5250:
5246:
5243:
5242:
5241:
5238:
5234:
5233:of arithmetic
5231:
5230:
5229:
5226:
5222:
5219:
5217:
5214:
5212:
5209:
5207:
5204:
5202:
5199:
5198:
5197:
5194:
5190:
5187:
5185:
5182:
5181:
5180:
5177:
5176:
5174:
5172:
5168:
5162:
5159:
5157:
5154:
5152:
5149:
5147:
5144:
5141:
5140:from ZFC
5137:
5134:
5132:
5129:
5123:
5120:
5119:
5118:
5115:
5113:
5110:
5108:
5105:
5104:
5103:
5100:
5098:
5095:
5093:
5090:
5088:
5085:
5083:
5080:
5078:
5075:
5073:
5070:
5069:
5067:
5065:
5061:
5051:
5050:
5046:
5045:
5040:
5039:non-Euclidean
5037:
5033:
5030:
5028:
5025:
5023:
5022:
5018:
5017:
5015:
5012:
5011:
5009:
5005:
5001:
4998:
4996:
4993:
4992:
4991:
4987:
4983:
4980:
4979:
4978:
4974:
4970:
4967:
4965:
4962:
4960:
4957:
4955:
4952:
4950:
4947:
4945:
4942:
4941:
4939:
4935:
4934:
4932:
4927:
4921:
4916:Example
4913:
4905:
4900:
4899:
4898:
4895:
4893:
4890:
4886:
4883:
4881:
4878:
4876:
4873:
4871:
4868:
4867:
4866:
4863:
4861:
4858:
4856:
4853:
4851:
4848:
4844:
4841:
4839:
4836:
4835:
4834:
4831:
4827:
4824:
4822:
4819:
4817:
4814:
4812:
4809:
4808:
4807:
4804:
4802:
4799:
4795:
4792:
4790:
4787:
4785:
4782:
4781:
4780:
4777:
4773:
4770:
4768:
4765:
4763:
4760:
4758:
4755:
4753:
4750:
4748:
4745:
4744:
4743:
4740:
4738:
4735:
4733:
4730:
4728:
4725:
4721:
4718:
4716:
4713:
4711:
4708:
4706:
4703:
4702:
4701:
4698:
4696:
4693:
4691:
4688:
4686:
4683:
4679:
4676:
4674:
4673:by definition
4671:
4670:
4669:
4666:
4662:
4659:
4658:
4657:
4654:
4652:
4649:
4647:
4644:
4642:
4639:
4637:
4634:
4633:
4630:
4627:
4625:
4621:
4616:
4610:
4606:
4596:
4593:
4591:
4588:
4586:
4583:
4581:
4578:
4576:
4573:
4571:
4568:
4566:
4563:
4561:
4560:KripkeâPlatek
4558:
4556:
4553:
4549:
4546:
4544:
4541:
4540:
4539:
4536:
4535:
4533:
4529:
4521:
4518:
4517:
4516:
4513:
4511:
4508:
4504:
4501:
4500:
4499:
4496:
4494:
4491:
4489:
4486:
4484:
4481:
4479:
4476:
4473:
4469:
4465:
4462:
4458:
4455:
4453:
4450:
4448:
4445:
4444:
4443:
4439:
4436:
4435:
4433:
4431:
4427:
4423:
4415:
4412:
4410:
4407:
4405:
4404:constructible
4402:
4401:
4400:
4397:
4395:
4392:
4390:
4387:
4385:
4382:
4380:
4377:
4375:
4372:
4370:
4367:
4365:
4362:
4360:
4357:
4355:
4352:
4350:
4347:
4345:
4342:
4340:
4337:
4336:
4334:
4332:
4327:
4319:
4316:
4314:
4311:
4309:
4306:
4304:
4301:
4299:
4296:
4294:
4291:
4290:
4288:
4284:
4281:
4279:
4276:
4275:
4274:
4271:
4269:
4266:
4264:
4261:
4259:
4256:
4254:
4250:
4246:
4244:
4241:
4237:
4234:
4233:
4232:
4229:
4228:
4225:
4222:
4220:
4216:
4206:
4203:
4201:
4198:
4196:
4193:
4191:
4188:
4186:
4183:
4181:
4178:
4174:
4171:
4170:
4169:
4166:
4162:
4157:
4156:
4155:
4152:
4151:
4149:
4147:
4143:
4135:
4132:
4130:
4127:
4125:
4122:
4121:
4120:
4117:
4115:
4112:
4110:
4107:
4105:
4102:
4100:
4097:
4095:
4092:
4090:
4087:
4086:
4084:
4082:
4081:Propositional
4078:
4072:
4069:
4067:
4064:
4062:
4059:
4057:
4054:
4052:
4049:
4047:
4044:
4040:
4037:
4036:
4035:
4032:
4030:
4027:
4025:
4022:
4020:
4017:
4015:
4012:
4010:
4009:Logical truth
4007:
4005:
4002:
4001:
3999:
3997:
3993:
3990:
3988:
3984:
3978:
3975:
3973:
3970:
3968:
3965:
3963:
3960:
3958:
3955:
3953:
3949:
3945:
3941:
3939:
3936:
3934:
3931:
3929:
3925:
3922:
3921:
3919:
3917:
3911:
3906:
3900:
3897:
3895:
3892:
3890:
3887:
3885:
3882:
3880:
3877:
3875:
3872:
3870:
3867:
3865:
3862:
3860:
3857:
3855:
3852:
3850:
3847:
3845:
3842:
3838:
3835:
3834:
3833:
3830:
3829:
3827:
3823:
3819:
3812:
3807:
3805:
3800:
3798:
3793:
3792:
3789:
3781:
3777:
3773:
3771:0-387-98600-6
3767:
3763:
3762:
3756:
3752:
3746:
3742:
3738:
3734:
3729:
3728:
3714:
3705:
3696:
3687:
3678:
3670:
3666:
3662:
3658:
3654:
3650:
3646:
3639:
3631:
3627:
3623:
3617:
3613:
3609:
3605:
3601:
3594:
3592:
3582:
3573:
3564:
3556:
3552:
3548:
3542:
3538:
3534:
3529:
3524:
3520:
3513:
3504:
3499:
3495:
3491:
3487:
3480:
3472:
3468:
3464:
3462:0-8186-1954-6
3458:
3454:
3450:
3446:
3442:
3435:
3426:
3417:
3408:
3400:
3396:
3391:
3386:
3382:
3378:
3371:
3363:
3359:
3355:
3353:9780444105370
3349:
3345:
3341:
3337:
3333:
3329:
3325:
3319:
3315:
3304:
3278:
3272:
3268:
3263:
3242:
3239:
3215:
3209:
3205:
3184:
3161:
3155:
3147:
3144:
3141:
3118:
3100:
3094:
3068:
3062:
3041:
3020:
3012:
3009:
3006:
2983:
2982:
2981:
2964:
2958:
2932:
2926:
2904:
2887:
2881:
2854:
2848:
2845:
2842:
2819:
2813:
2784:
2778:
2770:
2716:s are either
2701:
2697:
2674:
2670:
2644:
2640:
2636:
2631:
2627:
2621:
2617:
2610:
2607:
2604:
2596:
2592:
2588:
2583:
2579:
2573:
2569:
2539:
2536:
2533:
2527:
2501:
2495:
2492:
2460:
2454:
2448:
2422:
2416:
2413:
2398:
2378:
2372:
2336:
2330:
2307:
2301:
2275:
2269:
2247:
2238:
2236:
2231:
2211:
2208:
2205:
2199:
2193:
2190:
2187:
2184:
2178:
2172:
2166:
2163:
2160:
2154:
2151:
2145:
2142:
2139:
2133:
2108:
2105:
2102:
2098:
2091:
2088:
2080:
2059:
2056:
2053:
2049:
2042:
2039:
2030:
2013:
2010:
2007:
2001:
1968:
1965:
1962:
1958:
1951:
1948:
1940:
1930:
1928:
1923:
1890:
1887:
1884:
1878:
1849:
1846:
1843:
1839:
1835:
1830:
1826:
1819:
1799:
1796:
1793:
1773:
1770:
1765:
1761:
1757:
1754:
1751:
1746:
1742:
1716:
1712:
1681:
1678:
1675:
1664:
1661:
1658:
1654:
1616:
1613:
1610:
1607:
1604:
1601:
1598:
1585:
1565:
1536:
1507:
1478:
1449:
1420:
1391:
1362:
1333:
1321:
1312:
1309:
1298:
1292:
1283:
1276:
1252:
1244:
1240:
1235:
1233:
1223:
1220:
1209:
1207:
1203:
1197:
1180:
1174:
1171:
1165:
1162:
1159:
1153:
1150:
1144:
1141:
1138:
1132:
1107:
1104:
1101:
1097:
1090:
1087:
1062:
1059:
1056:
1052:
1045:
1042:
1022:
1002:
988:
986:
981:
979:
975:
971:
967:
949:
945:
922:
918:
904:
887:
879:
876:
873:
869:
845:
837:
833:
812:
802:
800:
796:
791:
775:
771:
746:
742:
737:
699:
695:
665:
659:
656:
651:
648:
645:
641:
629:
628:s is cyclic.
610:
606:
576:
573:
570:
566:
538:
535:
530:
527:
524:
520:
513:
510:
504:
496:
492:
471:
468:
465:
462:
459:
456:
450:
442:
438:
415:
412:
409:
399:
395:
347:
344:
341:
328:
314:
288:
259:
230:
201:
178:
152:
143:
140:
135:
132:
123:
116:
92:
84:
80:
76:
72:
68:
65:
55:
53:
49:
45:
40:
38:
34:
30:
26:
22:
5526:
5324:Ultraproduct
5171:Model theory
5136:Independence
5072:Formal proof
5064:Proof theory
5047:
5020:
4977:real numbers
4949:second-order
4860:Substitution
4737:Metalanguage
4678:conservative
4651:Axiom schema
4595:Constructive
4565:MorseâKelley
4531:Set theories
4510:Aleph number
4503:inaccessible
4409:Grothendieck
4293:intersection
4184:
4180:Higher-order
4168:Second-order
4114:Truth tables
4071:Venn diagram
3854:Formal proof
3764:. Springer.
3760:
3732:
3713:
3704:
3695:
3686:
3677:
3652:
3648:
3638:
3603:
3581:
3572:
3563:
3518:
3512:
3493:
3489:
3479:
3444:
3434:
3425:
3416:
3407:
3380:
3370:
3335:
3331:
3318:
3301:is equal to
3236:is equal to
2905:
2399:
2248:
2244:
2232:
2031:
1938:
1936:
1924:
1586:
1242:
1238:
1236:
1229:
1215:
1205:
1201:
1198:
994:
982:
973:
905:
810:
808:
794:
792:
630:
329:
74:
70:
66:
61:
41:
24:
18:
5434:Type theory
5382:undecidable
5314:Truth value
5201:equivalence
4880:non-logical
4493:Enumeration
4483:Isomorphism
4430:cardinality
4414:Von Neumann
4379:Ultrafilter
4344:Uncountable
4278:equivalence
4195:Quantifiers
4185:Fixed-point
4154:First-order
4034:Consistency
4019:Proposition
3996:Traditional
3967:Lindström's
3957:Compactness
3899:Type theory
3844:Cardinality
1208:)-formula.
364:variables,
5549:Categories
5245:elementary
4938:arithmetic
4806:Quantifier
4784:functional
4656:Expression
4374:Transitive
4318:identities
4303:complement
4236:hereditary
4219:Set theory
3725:References
3621:0897910990
2662:where the
2241:Iterations
1994:such that
1734:such that
1584:coincide.
430:such that
372:, and let
48:Alfred Aho
5516:Supertask
5419:Recursion
5377:decidable
5211:saturated
5189:of models
5112:deductive
5107:axiomatic
5027:Hilbert's
5014:Euclidean
4995:canonical
4918:axiomatic
4850:Signature
4779:Predicate
4668:Extension
4590:Ackermann
4515:Operation
4394:Universal
4384:Recursive
4359:Singleton
4354:Inhabited
4339:Countable
4329:Types of
4313:power set
4283:partition
4200:Predicate
4146:Predicate
4061:Syllogism
4051:Soundness
4024:Inference
4014:Tautology
3916:paradoxes
3780:901297152
3669:0097-5397
3523:CiteSeerX
3471:206437693
3362:0049-237X
3145:
3010:
2846:∗
2744:∃
2724:∀
2671:ϕ
2641:ϕ
2593:ϕ
2537:∧
2525:∃
2490:∃
2458:⇒
2446:∀
2411:∀
2200:ϕ
2197:¬
2194:∨
2176:∀
2173:∧
2155:ϕ
2134:ψ
2099:ψ
2092:
2050:ϕ
2043:
2002:ϕ
1959:ϕ
1952:
1879:ϕ
1820:ϕ
1655:ϕ
1569:→
1540:→
1511:→
1482:→
1453:→
1424:→
1395:→
1366:→
1337:→
1325:→
1313:φ
1310:
1302:→
1287:→
1172:∨
1154:ϕ
1133:ψ
1098:ψ
1091:
1053:ϕ
1046:
660:φ
657:
574:−
554:(meaning
528:−
514:φ
413:∈
292:→
263:→
234:→
205:→
156:→
144:φ
141:
127:→
5501:Logicism
5494:timeline
5470:Concrete
5329:Validity
5299:T-schema
5292:Kripke's
5287:Tarski's
5282:semantic
5272:Strength
5221:submodel
5216:spectrum
5184:function
5032:Tarski's
5021:Elements
5008:geometry
4964:Robinson
4885:variable
4870:function
4843:spectrum
4833:Sentence
4789:variable
4732:Language
4685:Relation
4646:Automata
4636:Alphabet
4620:language
4474:-jection
4452:codomain
4438:Function
4399:Universe
4369:Infinite
4273:Relation
4056:Validity
4046:Argument
3944:theorem,
3326:(1974).
2806:written
2514:to mean
2435:to mean
1352:, where
966:Immerman
171:, where
5443:Related
5240:Diagram
5138: (
5117:Hilbert
5102:Systems
5097:Theorem
4975:of the
4920:systems
4700:Formula
4695:Grammar
4611: (
4555:General
4268:Forcing
4253:Element
4173:Monadic
3948:paradox
3889:Theorem
3825:General
3630:7503265
3555:7869248
3399:3242505
2903:times.
2294:; here
985:Datalog
825:, then
37:Datalog
5206:finite
4969:Skolem
4922:
4897:Theory
4865:Symbol
4855:String
4838:atomic
4715:ground
4710:closed
4705:atomic
4661:ground
4624:syntax
4520:binary
4447:domain
4364:Finite
4129:finite
3987:Logics
3946:
3894:Theory
3778:
3768:
3747:
3667:
3628:
3618:
3553:
3543:
3525:
3469:
3459:
3397:
3360:
3350:
3303:PSPACE
2126:where
1869:φ
1125:where
815:φ
799:PSPACE
556:φ
374:φ
77:using
62:For a
5196:Model
4944:Peano
4801:Proof
4641:Arity
4570:Naive
4457:image
4389:Fuzzy
4349:Empty
4298:union
4243:Class
3884:Model
3874:Lemma
3832:Axiom
3626:S2CID
3551:S2CID
3467:S2CID
3395:S2CID
3310:Notes
3238:PTIME
2756:. If
1219:arity
970:Vardi
558:with
69:, FO(
5319:Type
5122:list
4926:list
4903:list
4892:Term
4826:rank
4720:open
4614:list
4426:Maps
4331:sets
4190:Free
4160:list
3910:list
3837:list
3776:OCLC
3766:ISBN
3745:ISBN
3665:ISSN
3616:ISBN
3541:ISBN
3457:ISBN
3358:ISSN
3348:ISBN
2479:and
2081:for
1918:and
1910:and
1797:<
1555:and
1439:and
1381:and
1196:.
968:and
484:and
380:and
330:Let
278:and
50:and
5006:of
4988:of
4936:of
4468:Sur
4442:Map
4249:Ur-
4231:Set
3737:doi
3657:doi
3608:doi
3533:doi
3498:doi
3449:doi
3385:doi
3340:doi
3142:log
3007:log
2736:or
2237:.
2077:is
2040:DTC
1949:DTC
1937:FO(
1237:FO(
1200:FO(
1088:PFP
1080:as
1043:IFP
903:).
717:on
642:PFP
327:.
117:PFP
93:PFP
19:In
5551::
5392:NP
5016::
5010::
4940::
4617:),
4472:Bi
4464:In
3774:.
3743:.
3663:.
3653:17
3651:.
3647:.
3624:.
3614:.
3602:.
3590:^
3549:.
3539:.
3531:.
3494:68
3492:.
3488:.
3465:.
3455:.
3443:.
3393:.
3379:.
3356:.
3346:.
3338:.
3336:77
3334:.
3330:.
3040:AC
2397:.
2230:.
2089:TC
2029:.
1927:NL
1922:.
1812:,
1526:,
1497:,
1277:TC
1253:TC
801:.
81:,
39:.
23:,
5472:/
5387:P
5142:)
4928:)
4924:(
4821:â
4816:!
4811:â
4772:=
4767:â
4762:â
4757:â§
4752:âš
4747:ÂŹ
4470:/
4466:/
4440:/
4251:)
4247:(
4134:â
4124:3
3912:)
3810:e
3803:t
3796:v
3782:.
3753:.
3739::
3671:.
3659::
3632:.
3610::
3557:.
3535::
3506:.
3500::
3473:.
3451::
3401:.
3387::
3364:.
3342::
3289:]
3282:)
3279:1
3276:(
3273:O
3269:n
3264:2
3260:[
3255:O
3252:F
3224:]
3219:)
3216:1
3213:(
3210:O
3206:n
3202:[
3197:O
3194:F
3170:]
3165:)
3162:1
3159:(
3156:O
3152:)
3148:n
3139:(
3136:[
3131:O
3128:F
3116:.
3104:)
3101:n
3098:(
3095:t
3075:]
3072:)
3069:n
3066:(
3063:t
3060:[
3055:O
3052:F
3026:]
3021:i
3017:)
3013:n
3004:(
3001:[
2996:O
2993:F
2968:)
2965:n
2962:(
2959:t
2939:]
2936:)
2933:n
2930:(
2927:t
2924:[
2919:O
2916:F
2891:)
2888:n
2885:(
2882:t
2872:k
2858:)
2855:n
2852:(
2849:t
2843:k
2823:)
2820:n
2817:(
2814:t
2804:Q
2788:)
2785:n
2782:(
2779:t
2775:]
2771:Q
2768:[
2758:Q
2702:i
2698:Q
2675:i
2650:)
2645:k
2637:,
2632:k
2628:x
2622:k
2618:Q
2614:(
2611:.
2608:.
2605:.
2602:)
2597:1
2589:,
2584:1
2580:x
2574:1
2570:Q
2566:(
2546:)
2543:)
2540:Q
2534:P
2531:(
2528:x
2522:(
2502:Q
2499:)
2496:P
2493:x
2487:(
2467:)
2464:)
2461:Q
2455:P
2452:(
2449:x
2443:(
2423:Q
2420:)
2417:P
2414:x
2408:(
2385:]
2382:)
2379:n
2376:(
2373:t
2370:[
2365:O
2362:F
2340:)
2337:n
2334:(
2331:t
2311:)
2308:n
2305:(
2302:t
2282:]
2279:)
2276:n
2273:(
2270:t
2267:[
2262:O
2259:F
2235:L
2218:)
2215:)
2212:x
2209:,
2206:u
2203:(
2191:v
2188:=
2185:x
2182:(
2179:x
2170:)
2167:v
2164:,
2161:u
2158:(
2152:=
2149:)
2146:v
2143:,
2140:u
2137:(
2114:)
2109:v
2106:,
2103:u
2095:(
2065:)
2060:v
2057:,
2054:u
2046:(
2017:)
2014:v
2011:,
2008:u
2005:(
1992:v
1988:u
1974:)
1969:v
1966:,
1963:u
1955:(
1939:X
1920:y
1916:x
1912:v
1908:u
1894:)
1891:y
1888:,
1885:x
1882:(
1855:)
1850:1
1847:+
1844:i
1840:z
1836:,
1831:i
1827:z
1823:(
1800:n
1794:i
1774:y
1771:=
1766:n
1762:z
1758:,
1755:x
1752:=
1747:1
1743:z
1722:)
1717:i
1713:z
1709:(
1699:n
1685:)
1682:y
1679:,
1676:x
1673:(
1670:)
1665:v
1662:,
1659:u
1651:(
1646:C
1643:T
1631:k
1617:y
1614:,
1611:x
1608:,
1605:v
1602:,
1599:u
1589:k
1566:t
1537:s
1508:y
1479:x
1450:s
1421:t
1392:y
1363:x
1334:t
1322:s
1316:]
1299:y
1293:,
1284:x
1273:[
1243:X
1239:X
1206:X
1202:X
1184:)
1181:x
1178:(
1175:P
1169:)
1166:x
1163:,
1160:P
1157:(
1151:=
1148:)
1145:x
1142:,
1139:P
1136:(
1113:)
1108:x
1105:,
1102:P
1094:(
1068:)
1063:x
1060:,
1057:P
1049:(
1023:P
1003:P
978:P
974:X
950:k
946:n
923:k
919:n
908:P
891:)
888:x
885:(
880:1
877:+
874:i
870:P
849:)
846:x
843:(
838:i
834:P
823:P
819:P
795:X
776:i
772:P
747:k
743:n
738:2
727:k
723:P
719:y
705:)
700:i
696:P
692:(
672:]
669:)
666:y
663:(
652:x
649:,
646:P
638:[
616:)
611:i
607:P
603:(
593:P
577:1
571:i
567:P
542:)
539:x
536:,
531:1
525:i
521:P
517:(
511:=
508:)
505:x
502:(
497:i
493:P
472:e
469:s
466:l
463:a
460:f
457:=
454:)
451:x
448:(
443:0
439:P
416:N
410:i
406:)
400:i
396:P
392:(
382:P
378:x
370:k
366:P
362:k
348:y
345:,
342:x
332:k
315:P
289:t
260:x
231:t
202:x
179:P
153:t
147:]
136:P
133:,
124:x
113:[
75:X
71:X
67:X
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.