3355:
1227:, where one usually wants to maximize (or minimize) an objective function subject to some constraints. However, leaving aside the objective function, the basic issue of simply deciding whether the constraints are satisfiable can be challenging or undecidable in some settings. The following table summarizes the main cases.
439:
with negation, it is generally possible to re-express the question of the validity of a formula to one involving satisfiability, because of the relationships between the concepts expressed in the above square of opposition. In particular Ï is valid if and only if ÂŹÏ is unsatisfiable, which is to say
351:
Satisfiability and validity are defined for a single formula, but can be generalized to an arbitrary theory or set of formulas: a theory is satisfiable if at least one interpretation makes every formula in the theory true, and valid if every formula is true in every interpretation. For example,
316:) to be an assignment of values to the variables and an assignment of meaning to all other non-logical symbols, and a formula is said to be satisfiable if there is some interpretation which makes it true. While this allows non-standard interpretations of symbols such as
517:. If satisfiability were also a semi-decidable problem, then the problem of the existence of counter-models would be too (a formula has counter-models iff its negation is satisfiable). So the problem of logical validity would be decidable, which contradicts the
921:
831:
630:, the problems of satisfiability and finite satisfiability coincide, as a formula of that logic has a model if and only if it has a finite model. This question is important in the mathematical field of
1067:
973:
364:. The negation of satisfiability is unsatisfiability, and the negation of validity is invalidity. These four concepts are related to each other in a manner exactly analogous to
1141:
that must exist by the second axiom, the finiteness of a model would require the existence of a loop, which would violate the third and fourth axioms, whether it loops back on
1734:
1116:
753:
2409:
1175:
of deciding satisfiability for an input formula in a given logic may differ from that of deciding finite satisfiability; in fact, for some logics, only one of them is
195:
1166:
697:
670:
306:
227:
149:
65:
117:
91:
1136:
334:
274:
2492:
1633:
505:. This fact has to do with the undecidability of the validity problem for FOL. The question of the status of the validity problem was posed firstly by
2806:
2964:
1602:
1583:
3459:
1752:
2819:
2142:
3391:
1276:
2404:
2824:
2814:
2551:
1757:
837:
3454:
2302:
1748:
514:
361:
3499:
2960:
1531:
1503:
1469:
1441:
1377:
759:
3057:
2801:
1626:
3484:
2362:
2055:
1796:
1522:
Alexander
Bockmayr; Volker Weispfenning (2001). "Solving Numerical Constraints". In John Alan Robinson; Andrei Voronkov (eds.).
1461:
1215:
1172:
478:
3318:
3020:
2783:
2778:
2603:
2024:
1708:
1367:
1211:
416:
388:
341:
982:
3313:
3096:
3013:
2726:
2657:
2534:
1776:
470:
2384:
3545:
3238:
3064:
2750:
1983:
464:
3509:
2389:
2721:
2460:
1718:
1619:
345:
3504:
3116:
3111:
1431:
3530:
3442:
3045:
2635:
2029:
1997:
1688:
1317:
1282:
1762:
3335:
3284:
3181:
2679:
2640:
2117:
1224:
1199:
404:
3427:
3176:
1791:
1468:. Technische UniversitĂ€t Dresden â Institute for Technical Computer Science. pp. 28â32. Archived from
3106:
2645:
2497:
2480:
2203:
1683:
927:
3447:
3384:
3008:
2985:
2946:
2832:
2773:
2419:
2339:
2183:
2127:
1740:
1387:
3535:
3479:
3298:
3025:
3003:
2970:
2863:
2709:
2694:
2667:
2618:
2502:
2437:
2262:
2228:
2223:
2097:
1928:
1905:
1372:
309:
245:
32:
3540:
3228:
3081:
2873:
2591:
2327:
2233:
2092:
2077:
1958:
1933:
1187:
627:
549:
is a collection of elements, taken from the structure, that satisfy Ï, then it is commonly written that
451:, the satisfiability problem is trivial, as every formula is satisfiable, while the validity problem is
448:
444:
3354:
3474:
3469:
3421:
3201:
3163:
3040:
2844:
2684:
2608:
2586:
2414:
2372:
2271:
2238:
2102:
1890:
1801:
1176:
518:
510:
369:
356:
are satisfiable because they are true in the natural numbers. This concept is closely related to the
1072:
709:
440:
it is false that ÂŹÏ is satisfiable. Put another way, Ï is satisfiable if and only if ÂŹÏ is invalid.
3415:
3330:
3221:
3206:
3186:
3143:
3030:
2980:
2906:
2851:
2788:
2581:
2576:
2524:
2292:
2281:
1953:
1853:
1781:
1772:
1768:
1703:
1698:
1261:
1195:
642:
631:
494:
380:
24:
637:
Finite satisfiability and satisfiability need not coincide in general. For instance, consider the
3377:
3359:
3128:
3091:
3076:
3069:
3052:
2838:
2704:
2630:
2613:
2566:
2379:
2288:
2122:
2107:
2067:
2019:
2004:
1992:
1948:
1923:
1693:
1642:
1251:
412:
241:
20:
2856:
2312:
473:, satisfiability is decidable for propositional formulae. In particular, satisfiability is an
360:
of a theory, and in fact is equivalent to consistency for first-order logic, a result known as
3294:
3101:
2911:
2901:
2793:
2674:
2509:
2485:
2266:
2250:
2155:
2132:
2009:
1978:
1943:
1838:
1673:
1598:
1579:
1527:
1499:
1437:
1333:
1183:
638:
538:
490:
400:
396:
392:
384:
237:
162:
3437:
3308:
3303:
3196:
3153:
2975:
2936:
2931:
2916:
2742:
2699:
2596:
2394:
2344:
1918:
1880:
1382:
1362:
1272:
700:
376:
152:
1144:
675:
648:
279:
200:
122:
38:
3404:
3289:
3279:
3233:
3216:
3171:
3133:
3035:
2955:
2762:
2689:
2662:
2650:
2556:
2470:
2444:
2399:
2367:
2168:
1970:
1913:
1863:
1828:
1786:
1567:
1191:
561:
498:
436:
96:
70:
3274:
3253:
3211:
3191:
2941:
2539:
2529:
2519:
2514:
2448:
2322:
2198:
2087:
2082:
2060:
1661:
1571:
1457:
1138:
1121:
534:
452:
420:
408:
319:
259:
233:
3524:
3248:
2926:
2433:
2218:
2208:
2178:
2163:
1833:
1427:
506:
502:
424:
447:, the questions of validity and satisfiability may be unrelated. In the case of the
159:
if every assignment of values to its variables makes the formula true. For example,
3148:
2995:
2896:
2888:
2768:
2716:
2625:
2561:
2544:
2475:
2334:
2193:
1895:
1678:
1423:
530:
353:
313:
3489:
3432:
3369:
3258:
3138:
2317:
2307:
2254:
1938:
1858:
1843:
1723:
1668:
1257:
474:
357:
232:
Formally, satisfiability is studied with respect to a fixed logic defining the
2188:
2043:
2014:
1820:
1297:
For linear constraints, a fuller picture is provided by the following table.
3464:
3400:
3340:
3243:
2296:
2213:
2173:
2137:
2073:
1885:
1875:
1848:
365:
249:
151:
is not satisfiable over the integers. The dual concept to satisfiability is
3325:
3123:
2571:
2276:
1870:
1069:, but it can be shown that it has no finite model (starting at the fact
2921:
1713:
391:, or SAT. In general, the problem of determining whether a sentence of
1611:
521:, a result stating the negative answer for the Entscheidungsproblem.
513:. The universal validity of a formula is a semi-decidable problem by
419:
are used to attempt to decide satisfiability. Whether a particular
2465:
1811:
1656:
1247:
622:, which is the question of determining whether a formula admits a
337:
916:{\displaystyle \forall xyz(R(y,x)\wedge R(z,x)\rightarrow y=z))}
477:
problem, and is one of the most intensively studied problems in
344:
problem considers satisfiability of a formula with respect to a
3373:
1615:
826:{\displaystyle \forall xy(R(x,y)\rightarrow \exists zR(y,z))}
595:
is a collection of atomic sentences (a theory) satisfied by
248:. Rather than being syntactic, however, satisfiability is a
1593:
A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009).
1517:
1515:
537:
is satisfiable if there is a collection of elements of a
336:, one can restrict their meaning by providing additional
1551:
Boolos, George; Burgess, John; Jeffrey, Richard (2007).
1147:
1124:
1075:
1062:{\displaystyle R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots }
985:
930:
840:
762:
712:
678:
651:
322:
282:
262:
203:
165:
125:
99:
73:
41:
31:
if it is true under some assignment of values to its
1406:
3267:
3162:
2994:
2887:
2739:
2432:
2355:
2249:
2153:
2042:
1969:
1904:
1819:
1810:
1732:
1649:
626:model that makes it true. For a logic that has the
1160:
1130:
1110:
1061:
967:
915:
825:
747:
691:
664:
423:is decidable or not depends whether the theory is
328:
300:
268:
221:
189:
143:
111:
85:
59:
1576:Decision Procedures: An Algorithmic Point of View
348:, which is a (finite or infinite) set of axioms.
560:If Ï has no free variables, that is, if Ï is an
459:Propositional satisfiability for classical logic
618:A problem related to satisfiability is that of
1436:. Cambridge University Press. pp. 58â92.
3385:
1627:
979:The resulting formula has the infinite model
8:
256:of the symbols, for example, the meaning of
1555:(5th ed.). Cambridge University Press.
3392:
3378:
3370:
2453:
2048:
1816:
1634:
1620:
1612:
1498:. Cambridge University Press. p. 12.
1578:. Springer Science & Business Media.
1152:
1146:
1123:
1099:
1086:
1074:
1044:
1031:
1009:
996:
984:
956:
929:
839:
761:
736:
723:
711:
683:
677:
656:
650:
443:For logics without negation, such as the
321:
281:
261:
202:
164:
124:
98:
72:
40:
1524:Handbook of Automated Reasoning Volume I
1299:
1229:
1202:applied to the negation of the formula.
968:{\displaystyle \forall x\neg R(x,a_{0})}
1399:
1351:Table source: Bockmayr and Weispfenning
1292:Table source: Bockmayr and Weispfenning
431:Reduction of validity to satisfiability
67:is satisfiable because it is true when
395:is satisfiable is not decidable. In
7:
1466:Lecture Notes â Advanced Logics
579:In this case, one may also say that
545:is a structure, Ï is a formula, and
379:of determining whether a formula in
1462:"Chapter 1.3 Undecidability of FOL"
1277:Cylindrical algebraic decomposition
485:Satisfiability in first-order logic
252:property because it relates to the
1409:, p. 120: "A set of sentences is
1407:Boolos, Burgess & Jeffrey 2007
937:
931:
841:
796:
763:
645:of the following sentences, where
14:
541:that render the formula true. If
3353:
197:is valid over the integers, but
3460:Gödel's incompleteness theorems
1216:Constraint satisfaction problem
583:is a model for Ï, or that Ï is
479:computational complexity theory
449:positive propositional calculus
445:positive propositional calculus
352:theories of arithmetic such as
1378:Karp's 21 NP-complete problems
1368:Boolean satisfiability problem
1212:Satisfiability modulo theories
1111:{\displaystyle R(a_{0},a_{1})}
1105:
1079:
1050:
1024:
1015:
989:
962:
943:
910:
907:
895:
892:
880:
871:
859:
853:
820:
817:
805:
793:
790:
778:
772:
748:{\displaystyle R(a_{0},a_{1})}
742:
716:
525:Satisfiability in model theory
497:. More specifically, it is a
389:Boolean satisfiability problem
342:satisfiability modulo theories
1:
3314:History of mathematical logic
1223:often appear in the field of
471:classical propositional logic
16:Concept in mathematical logic
3455:Gödel's completeness theorem
3239:Primitive recursive function
1168:or on a different element).
515:Gödel's completeness theorem
465:Propositional satisfiability
362:Gödel's completeness theorem
236:of allowed symbols, such as
1433:Term Rewriting and All That
1186:, finite satisfiability is
1118:and following the chain of
35:. For example, the formula
3562:
3443:Foundations of mathematics
2303:SchröderâBernstein theorem
2030:Monadic predicate calculus
1689:Foundations of mathematics
1595:Handbook of Satisfiability
1526:. Elsevier and MIT Press.
1413:if some interpretation .".
1209:
501:problem and therefore not
462:
3411:
3349:
3336:Philosophy of mathematics
3285:Automated theorem proving
2456:
2410:Von NeumannâBernaysâGödel
2051:
1536:. (Elsevier) (MIT Press).
1225:mathematical optimization
564:, and it is satisfied by
493:(FOL), satisfiability is
427:and on other conditions.
405:automated theorem proving
308:. Formally, we define an
3485:LöwenheimâSkolem theorem
1494:Wilifrid Hodges (1997).
1173:computational complexity
641:formula obtained as the
3510:Useâmention distinction
2986:Self-verifying theories
2807:Tarski's axiomatization
1758:Tarski's undefinability
1753:incompleteness theorems
1553:Computability and Logic
1388:Constraint satisfaction
1283:Hilbert's tenth problem
190:{\displaystyle x+3=3+x}
3505:Typeâtoken distinction
3360:Mathematics portal
2971:Proof of impossibility
2619:propositional variable
1929:Propositional calculus
1496:A Shorter Model Theory
1373:Circuit satisfiability
1200:Trakhtenbrot's theorem
1188:recursively enumerable
1162:
1132:
1112:
1063:
969:
917:
827:
749:
693:
666:
387:, and is known as the
330:
302:
270:
223:
191:
145:
113:
87:
61:
3229:Kolmogorov complexity
3182:Computably enumerable
3082:Model complete theory
2874:Principia Mathematica
1934:Propositional formula
1763:BanachâTarski paradox
1221:Numerical constraints
1210:Further information:
1206:Numerical constraints
1163:
1161:{\displaystyle a_{0}}
1133:
1113:
1064:
970:
918:
828:
750:
694:
692:{\displaystyle a_{1}}
667:
665:{\displaystyle a_{0}}
628:finite model property
620:finite satisfiability
614:Finite satisfiability
519:ChurchâTuring theorem
331:
303:
301:{\displaystyle x+1=x}
276:in a formula such as
271:
224:
222:{\displaystyle x+3=y}
192:
146:
144:{\displaystyle x+1=x}
114:
88:
62:
60:{\displaystyle x+3=y}
3428:ChurchâTuring thesis
3422:Entscheidungsproblem
3177:ChurchâTuring thesis
3164:Computability theory
2373:continuum hypothesis
1891:Square of opposition
1749:Gödel's completeness
1145:
1122:
1073:
983:
928:
838:
760:
710:
676:
649:
511:Entscheidungsproblem
370:square of opposition
320:
280:
260:
201:
163:
123:
119:, while the formula
97:
71:
39:
3546:Philosophy of logic
3331:Mathematical object
3222:P versus NP problem
3187:Computable function
2981:Reverse mathematics
2907:Logical consequence
2784:primitive recursive
2779:elementary function
2552:Free/bound variable
2405:TarskiâGrothendieck
1924:Logical connectives
1854:Logical equivalence
1704:Logical consequence
1334:Linear inequalities
1262:integer programming
632:finite model theory
509:, as the so-called
381:propositional logic
246:propositional logic
112:{\displaystyle y=6}
86:{\displaystyle x=3}
3129:Transfer principle
3092:Semantics of logic
3077:Categorical theory
3053:Non-standard model
2567:Logical connective
1694:Information theory
1643:Mathematical logic
1475:on 14 October 2020
1252:linear programming
1158:
1128:
1108:
1059:
965:
913:
823:
745:
689:
662:
568:, then one writes
413:congruence closure
383:is satisfiable is
326:
298:
266:
242:second-order logic
219:
187:
141:
109:
83:
57:
21:mathematical logic
3531:Concepts in logic
3518:
3517:
3367:
3366:
3299:Abstract category
3102:Theories of truth
2912:Rule of inference
2902:Natural deduction
2883:
2882:
2428:
2427:
2133:Cartesian product
2038:
2037:
1944:Many-valued logic
1919:Boolean functions
1802:Russell's paradox
1777:diagonal argument
1674:First-order logic
1604:978-1-60750-376-7
1585:978-3-540-74104-6
1348:
1347:
1303:Constraints over:
1289:
1288:
1184:first-order logic
1131:{\displaystyle R}
639:first-order logic
491:first-order logic
407:, the methods of
401:equational theory
397:universal algebra
393:first-order logic
329:{\displaystyle +}
269:{\displaystyle +}
238:first-order logic
3553:
3438:Effective method
3416:Cantor's theorem
3394:
3387:
3380:
3371:
3358:
3357:
3309:History of logic
3304:Category of sets
3197:Decision problem
2976:Ordinal analysis
2917:Sequent calculus
2815:Boolean algebras
2755:
2754:
2729:
2700:logical/constant
2454:
2440:
2363:ZermeloâFraenkel
2114:Set operations:
2049:
1986:
1817:
1797:LöwenheimâSkolem
1684:Formal semantics
1636:
1629:
1622:
1613:
1608:
1589:
1556:
1538:
1537:
1519:
1510:
1509:
1491:
1485:
1484:
1482:
1480:
1474:
1454:
1448:
1447:
1420:
1414:
1404:
1363:2-satisfiability
1318:Linear equations
1312:natural numbers
1300:
1230:
1222:
1167:
1165:
1164:
1159:
1157:
1156:
1137:
1135:
1134:
1129:
1117:
1115:
1114:
1109:
1104:
1103:
1091:
1090:
1068:
1066:
1065:
1060:
1049:
1048:
1036:
1035:
1014:
1013:
1001:
1000:
974:
972:
971:
966:
961:
960:
922:
920:
919:
914:
832:
830:
829:
824:
754:
752:
751:
746:
741:
740:
728:
727:
698:
696:
695:
690:
688:
687:
671:
669:
668:
663:
661:
660:
437:classical logics
354:Peano arithmetic
335:
333:
332:
327:
307:
305:
304:
299:
275:
273:
272:
267:
228:
226:
225:
220:
196:
194:
193:
188:
150:
148:
147:
142:
118:
116:
115:
110:
92:
90:
89:
84:
66:
64:
63:
58:
3561:
3560:
3556:
3555:
3554:
3552:
3551:
3550:
3521:
3520:
3519:
3514:
3407:
3405:metamathematics
3398:
3368:
3363:
3352:
3345:
3290:Category theory
3280:Algebraic logic
3263:
3234:Lambda calculus
3172:Church encoding
3158:
3134:Truth predicate
2990:
2956:Complete theory
2879:
2748:
2744:
2740:
2735:
2727:
2447: and
2443:
2438:
2424:
2400:New Foundations
2368:axiom of choice
2351:
2313:Gödel numbering
2253: and
2245:
2149:
2034:
1984:
1965:
1914:Boolean algebra
1900:
1864:Equiconsistency
1829:Classical logic
1806:
1787:Halting problem
1775: and
1751: and
1739: and
1738:
1733:Theorems (
1728:
1645:
1640:
1605:
1592:
1586:
1568:Daniel Kroening
1566:
1563:
1561:Further reading
1550:
1547:
1542:
1541:
1534:
1521:
1520:
1513:
1506:
1493:
1492:
1488:
1478:
1476:
1472:
1458:Baier, Christel
1456:
1455:
1451:
1444:
1422:
1421:
1417:
1405:
1401:
1396:
1359:
1220:
1218:
1208:
1148:
1143:
1142:
1120:
1119:
1095:
1082:
1071:
1070:
1040:
1027:
1005:
992:
981:
980:
978:
952:
926:
925:
836:
835:
758:
757:
732:
719:
708:
707:
679:
674:
673:
652:
647:
646:
616:
562:atomic sentence
527:
487:
469:In the case of
467:
461:
433:
318:
317:
278:
277:
258:
257:
199:
198:
161:
160:
155:; a formula is
121:
120:
95:
94:
69:
68:
37:
36:
17:
12:
11:
5:
3559:
3557:
3549:
3548:
3543:
3538:
3533:
3523:
3522:
3516:
3515:
3513:
3512:
3507:
3502:
3497:
3495:Satisfiability
3492:
3487:
3482:
3480:Interpretation
3477:
3472:
3467:
3462:
3457:
3452:
3451:
3450:
3440:
3435:
3430:
3425:
3418:
3412:
3409:
3408:
3399:
3397:
3396:
3389:
3382:
3374:
3365:
3364:
3350:
3347:
3346:
3344:
3343:
3338:
3333:
3328:
3323:
3322:
3321:
3311:
3306:
3301:
3292:
3287:
3282:
3277:
3275:Abstract logic
3271:
3269:
3265:
3264:
3262:
3261:
3256:
3254:Turing machine
3251:
3246:
3241:
3236:
3231:
3226:
3225:
3224:
3219:
3214:
3209:
3204:
3194:
3192:Computable set
3189:
3184:
3179:
3174:
3168:
3166:
3160:
3159:
3157:
3156:
3151:
3146:
3141:
3136:
3131:
3126:
3121:
3120:
3119:
3114:
3109:
3099:
3094:
3089:
3087:Satisfiability
3084:
3079:
3074:
3073:
3072:
3062:
3061:
3060:
3050:
3049:
3048:
3043:
3038:
3033:
3028:
3018:
3017:
3016:
3011:
3004:Interpretation
3000:
2998:
2992:
2991:
2989:
2988:
2983:
2978:
2973:
2968:
2958:
2953:
2952:
2951:
2950:
2949:
2939:
2934:
2924:
2919:
2914:
2909:
2904:
2899:
2893:
2891:
2885:
2884:
2881:
2880:
2878:
2877:
2869:
2868:
2867:
2866:
2861:
2860:
2859:
2854:
2849:
2829:
2828:
2827:
2825:minimal axioms
2822:
2811:
2810:
2809:
2798:
2797:
2796:
2791:
2786:
2781:
2776:
2771:
2758:
2756:
2737:
2736:
2734:
2733:
2732:
2731:
2719:
2714:
2713:
2712:
2707:
2702:
2697:
2687:
2682:
2677:
2672:
2671:
2670:
2665:
2655:
2654:
2653:
2648:
2643:
2638:
2628:
2623:
2622:
2621:
2616:
2611:
2601:
2600:
2599:
2594:
2589:
2584:
2579:
2574:
2564:
2559:
2554:
2549:
2548:
2547:
2542:
2537:
2532:
2522:
2517:
2515:Formation rule
2512:
2507:
2506:
2505:
2500:
2490:
2489:
2488:
2478:
2473:
2468:
2463:
2457:
2451:
2434:Formal systems
2430:
2429:
2426:
2425:
2423:
2422:
2417:
2412:
2407:
2402:
2397:
2392:
2387:
2382:
2377:
2376:
2375:
2370:
2359:
2357:
2353:
2352:
2350:
2349:
2348:
2347:
2337:
2332:
2331:
2330:
2323:Large cardinal
2320:
2315:
2310:
2305:
2300:
2286:
2285:
2284:
2279:
2274:
2259:
2257:
2247:
2246:
2244:
2243:
2242:
2241:
2236:
2231:
2221:
2216:
2211:
2206:
2201:
2196:
2191:
2186:
2181:
2176:
2171:
2166:
2160:
2158:
2151:
2150:
2148:
2147:
2146:
2145:
2140:
2135:
2130:
2125:
2120:
2112:
2111:
2110:
2105:
2095:
2090:
2088:Extensionality
2085:
2083:Ordinal number
2080:
2070:
2065:
2064:
2063:
2052:
2046:
2040:
2039:
2036:
2035:
2033:
2032:
2027:
2022:
2017:
2012:
2007:
2002:
2001:
2000:
1990:
1989:
1988:
1975:
1973:
1967:
1966:
1964:
1963:
1962:
1961:
1956:
1951:
1941:
1936:
1931:
1926:
1921:
1916:
1910:
1908:
1902:
1901:
1899:
1898:
1893:
1888:
1883:
1878:
1873:
1868:
1867:
1866:
1856:
1851:
1846:
1841:
1836:
1831:
1825:
1823:
1814:
1808:
1807:
1805:
1804:
1799:
1794:
1789:
1784:
1779:
1767:Cantor's
1765:
1760:
1755:
1745:
1743:
1730:
1729:
1727:
1726:
1721:
1716:
1711:
1706:
1701:
1696:
1691:
1686:
1681:
1676:
1671:
1666:
1665:
1664:
1653:
1651:
1647:
1646:
1641:
1639:
1638:
1631:
1624:
1616:
1610:
1609:
1603:
1590:
1584:
1572:Ofer Strichman
1562:
1559:
1558:
1557:
1546:
1543:
1540:
1539:
1532:
1511:
1504:
1486:
1449:
1442:
1415:
1398:
1397:
1395:
1392:
1391:
1390:
1385:
1380:
1375:
1370:
1365:
1358:
1355:
1346:
1345:
1342:
1339:
1336:
1330:
1329:
1326:
1323:
1320:
1314:
1313:
1310:
1307:
1304:
1287:
1286:
1279:
1270:
1266:
1265:
1255:
1245:
1241:
1240:
1239:over integers
1237:
1234:
1207:
1204:
1182:For classical
1155:
1151:
1127:
1107:
1102:
1098:
1094:
1089:
1085:
1081:
1078:
1058:
1055:
1052:
1047:
1043:
1039:
1034:
1030:
1026:
1023:
1020:
1017:
1012:
1008:
1004:
999:
995:
991:
988:
976:
975:
964:
959:
955:
951:
948:
945:
942:
939:
936:
933:
923:
912:
909:
906:
903:
900:
897:
894:
891:
888:
885:
882:
879:
876:
873:
870:
867:
864:
861:
858:
855:
852:
849:
846:
843:
833:
822:
819:
816:
813:
810:
807:
804:
801:
798:
795:
792:
789:
786:
783:
780:
777:
774:
771:
768:
765:
755:
744:
739:
735:
731:
726:
722:
718:
715:
686:
682:
659:
655:
615:
612:
611:
610:
577:
576:
558:
557:
535:atomic formula
526:
523:
499:co-RE-complete
486:
483:
463:Main article:
460:
457:
453:co-NP complete
432:
429:
409:term rewriting
325:
310:interpretation
297:
294:
291:
288:
285:
265:
218:
215:
212:
209:
206:
186:
183:
180:
177:
174:
171:
168:
140:
137:
134:
131:
128:
108:
105:
102:
82:
79:
76:
56:
53:
50:
47:
44:
15:
13:
10:
9:
6:
4:
3:
2:
3558:
3547:
3544:
3542:
3539:
3537:
3536:Logical truth
3534:
3532:
3529:
3528:
3526:
3511:
3508:
3506:
3503:
3501:
3498:
3496:
3493:
3491:
3488:
3486:
3483:
3481:
3478:
3476:
3473:
3471:
3468:
3466:
3463:
3461:
3458:
3456:
3453:
3449:
3446:
3445:
3444:
3441:
3439:
3436:
3434:
3431:
3429:
3426:
3424:
3423:
3419:
3417:
3414:
3413:
3410:
3406:
3402:
3395:
3390:
3388:
3383:
3381:
3376:
3375:
3372:
3362:
3361:
3356:
3348:
3342:
3339:
3337:
3334:
3332:
3329:
3327:
3324:
3320:
3317:
3316:
3315:
3312:
3310:
3307:
3305:
3302:
3300:
3296:
3293:
3291:
3288:
3286:
3283:
3281:
3278:
3276:
3273:
3272:
3270:
3266:
3260:
3257:
3255:
3252:
3250:
3249:Recursive set
3247:
3245:
3242:
3240:
3237:
3235:
3232:
3230:
3227:
3223:
3220:
3218:
3215:
3213:
3210:
3208:
3205:
3203:
3200:
3199:
3198:
3195:
3193:
3190:
3188:
3185:
3183:
3180:
3178:
3175:
3173:
3170:
3169:
3167:
3165:
3161:
3155:
3152:
3150:
3147:
3145:
3142:
3140:
3137:
3135:
3132:
3130:
3127:
3125:
3122:
3118:
3115:
3113:
3110:
3108:
3105:
3104:
3103:
3100:
3098:
3095:
3093:
3090:
3088:
3085:
3083:
3080:
3078:
3075:
3071:
3068:
3067:
3066:
3063:
3059:
3058:of arithmetic
3056:
3055:
3054:
3051:
3047:
3044:
3042:
3039:
3037:
3034:
3032:
3029:
3027:
3024:
3023:
3022:
3019:
3015:
3012:
3010:
3007:
3006:
3005:
3002:
3001:
2999:
2997:
2993:
2987:
2984:
2982:
2979:
2977:
2974:
2972:
2969:
2966:
2965:from ZFC
2962:
2959:
2957:
2954:
2948:
2945:
2944:
2943:
2940:
2938:
2935:
2933:
2930:
2929:
2928:
2925:
2923:
2920:
2918:
2915:
2913:
2910:
2908:
2905:
2903:
2900:
2898:
2895:
2894:
2892:
2890:
2886:
2876:
2875:
2871:
2870:
2865:
2864:non-Euclidean
2862:
2858:
2855:
2853:
2850:
2848:
2847:
2843:
2842:
2840:
2837:
2836:
2834:
2830:
2826:
2823:
2821:
2818:
2817:
2816:
2812:
2808:
2805:
2804:
2803:
2799:
2795:
2792:
2790:
2787:
2785:
2782:
2780:
2777:
2775:
2772:
2770:
2767:
2766:
2764:
2760:
2759:
2757:
2752:
2746:
2741:Example
2738:
2730:
2725:
2724:
2723:
2720:
2718:
2715:
2711:
2708:
2706:
2703:
2701:
2698:
2696:
2693:
2692:
2691:
2688:
2686:
2683:
2681:
2678:
2676:
2673:
2669:
2666:
2664:
2661:
2660:
2659:
2656:
2652:
2649:
2647:
2644:
2642:
2639:
2637:
2634:
2633:
2632:
2629:
2627:
2624:
2620:
2617:
2615:
2612:
2610:
2607:
2606:
2605:
2602:
2598:
2595:
2593:
2590:
2588:
2585:
2583:
2580:
2578:
2575:
2573:
2570:
2569:
2568:
2565:
2563:
2560:
2558:
2555:
2553:
2550:
2546:
2543:
2541:
2538:
2536:
2533:
2531:
2528:
2527:
2526:
2523:
2521:
2518:
2516:
2513:
2511:
2508:
2504:
2501:
2499:
2498:by definition
2496:
2495:
2494:
2491:
2487:
2484:
2483:
2482:
2479:
2477:
2474:
2472:
2469:
2467:
2464:
2462:
2459:
2458:
2455:
2452:
2450:
2446:
2441:
2435:
2431:
2421:
2418:
2416:
2413:
2411:
2408:
2406:
2403:
2401:
2398:
2396:
2393:
2391:
2388:
2386:
2385:KripkeâPlatek
2383:
2381:
2378:
2374:
2371:
2369:
2366:
2365:
2364:
2361:
2360:
2358:
2354:
2346:
2343:
2342:
2341:
2338:
2336:
2333:
2329:
2326:
2325:
2324:
2321:
2319:
2316:
2314:
2311:
2309:
2306:
2304:
2301:
2298:
2294:
2290:
2287:
2283:
2280:
2278:
2275:
2273:
2270:
2269:
2268:
2264:
2261:
2260:
2258:
2256:
2252:
2248:
2240:
2237:
2235:
2232:
2230:
2229:constructible
2227:
2226:
2225:
2222:
2220:
2217:
2215:
2212:
2210:
2207:
2205:
2202:
2200:
2197:
2195:
2192:
2190:
2187:
2185:
2182:
2180:
2177:
2175:
2172:
2170:
2167:
2165:
2162:
2161:
2159:
2157:
2152:
2144:
2141:
2139:
2136:
2134:
2131:
2129:
2126:
2124:
2121:
2119:
2116:
2115:
2113:
2109:
2106:
2104:
2101:
2100:
2099:
2096:
2094:
2091:
2089:
2086:
2084:
2081:
2079:
2075:
2071:
2069:
2066:
2062:
2059:
2058:
2057:
2054:
2053:
2050:
2047:
2045:
2041:
2031:
2028:
2026:
2023:
2021:
2018:
2016:
2013:
2011:
2008:
2006:
2003:
1999:
1996:
1995:
1994:
1991:
1987:
1982:
1981:
1980:
1977:
1976:
1974:
1972:
1968:
1960:
1957:
1955:
1952:
1950:
1947:
1946:
1945:
1942:
1940:
1937:
1935:
1932:
1930:
1927:
1925:
1922:
1920:
1917:
1915:
1912:
1911:
1909:
1907:
1906:Propositional
1903:
1897:
1894:
1892:
1889:
1887:
1884:
1882:
1879:
1877:
1874:
1872:
1869:
1865:
1862:
1861:
1860:
1857:
1855:
1852:
1850:
1847:
1845:
1842:
1840:
1837:
1835:
1834:Logical truth
1832:
1830:
1827:
1826:
1824:
1822:
1818:
1815:
1813:
1809:
1803:
1800:
1798:
1795:
1793:
1790:
1788:
1785:
1783:
1780:
1778:
1774:
1770:
1766:
1764:
1761:
1759:
1756:
1754:
1750:
1747:
1746:
1744:
1742:
1736:
1731:
1725:
1722:
1720:
1717:
1715:
1712:
1710:
1707:
1705:
1702:
1700:
1697:
1695:
1692:
1690:
1687:
1685:
1682:
1680:
1677:
1675:
1672:
1670:
1667:
1663:
1660:
1659:
1658:
1655:
1654:
1652:
1648:
1644:
1637:
1632:
1630:
1625:
1623:
1618:
1617:
1614:
1606:
1600:
1597:. IOS Press.
1596:
1591:
1587:
1581:
1577:
1573:
1569:
1565:
1564:
1560:
1554:
1549:
1548:
1544:
1535:
1533:0-444-82949-0
1529:
1525:
1518:
1516:
1512:
1507:
1505:0-521-58713-1
1501:
1497:
1490:
1487:
1471:
1467:
1463:
1459:
1453:
1450:
1445:
1443:0-521-77920-0
1439:
1435:
1434:
1429:
1428:Tobias Nipkow
1425:
1419:
1416:
1412:
1408:
1403:
1400:
1393:
1389:
1386:
1384:
1381:
1379:
1376:
1374:
1371:
1369:
1366:
1364:
1361:
1360:
1356:
1354:
1352:
1343:
1340:
1337:
1335:
1332:
1331:
1327:
1324:
1321:
1319:
1316:
1315:
1311:
1308:
1305:
1302:
1301:
1298:
1295:
1293:
1284:
1281:undecidable (
1280:
1278:
1275:through e.g.
1274:
1271:
1268:
1267:
1263:
1259:
1256:
1253:
1249:
1246:
1243:
1242:
1238:
1235:
1232:
1231:
1228:
1226:
1217:
1213:
1205:
1203:
1201:
1197:
1193:
1189:
1185:
1180:
1178:
1174:
1169:
1153:
1149:
1140:
1125:
1100:
1096:
1092:
1087:
1083:
1076:
1056:
1053:
1045:
1041:
1037:
1032:
1028:
1021:
1018:
1010:
1006:
1002:
997:
993:
986:
957:
953:
949:
946:
940:
934:
924:
904:
901:
898:
889:
886:
883:
877:
874:
868:
865:
862:
856:
850:
847:
844:
834:
814:
811:
808:
802:
799:
787:
784:
781:
775:
769:
766:
756:
737:
733:
729:
724:
720:
713:
706:
705:
704:
702:
684:
680:
657:
653:
644:
640:
635:
633:
629:
625:
621:
613:
609:
605:
602:
601:
600:
599:, one writes
598:
594:
590:
586:
582:
574:
571:
570:
569:
567:
563:
555:
552:
551:
550:
548:
544:
540:
536:
532:
524:
522:
520:
516:
512:
508:
507:David Hilbert
504:
503:semidecidable
500:
496:
492:
484:
482:
480:
476:
472:
466:
458:
456:
454:
450:
446:
441:
438:
430:
428:
426:
425:variable-free
422:
418:
414:
410:
406:
402:
398:
394:
390:
386:
382:
378:
373:
371:
367:
363:
359:
355:
349:
347:
346:formal theory
343:
339:
323:
315:
311:
295:
292:
289:
286:
283:
263:
255:
251:
247:
243:
239:
235:
230:
216:
213:
210:
207:
204:
184:
181:
178:
175:
172:
169:
166:
158:
154:
138:
135:
132:
129:
126:
106:
103:
100:
80:
77:
74:
54:
51:
48:
45:
42:
34:
30:
26:
22:
3541:Model theory
3500:Independence
3494:
3475:Decidability
3470:Completeness
3420:
3351:
3149:Ultraproduct
3086:
2996:Model theory
2961:Independence
2897:Formal proof
2889:Proof theory
2872:
2845:
2802:real numbers
2774:second-order
2685:Substitution
2562:Metalanguage
2503:conservative
2476:Axiom schema
2420:Constructive
2390:MorseâKelley
2356:Set theories
2335:Aleph number
2328:inaccessible
2234:Grothendieck
2118:intersection
2005:Higher-order
1993:Second-order
1939:Truth tables
1896:Venn diagram
1679:Formal proof
1594:
1575:
1552:
1523:
1495:
1489:
1477:. Retrieved
1470:the original
1465:
1452:
1432:
1424:Franz Baader
1418:
1410:
1402:
1350:
1349:
1344:NP-complete
1328:NP-complete
1296:
1291:
1290:
1219:
1181:
1170:
977:
636:
623:
619:
617:
607:
603:
596:
592:
588:
584:
580:
578:
572:
565:
559:
553:
546:
542:
531:model theory
528:
488:
468:
442:
434:
374:
350:
253:
231:
156:
28:
18:
3490:Metatheorem
3448:of geometry
3433:Consistency
3259:Type theory
3207:undecidable
3139:Truth value
3026:equivalence
2705:non-logical
2318:Enumeration
2308:Isomorphism
2255:cardinality
2239:Von Neumann
2204:Ultrafilter
2169:Uncountable
2103:equivalence
2020:Quantifiers
2010:Fixed-point
1979:First-order
1859:Consistency
1844:Proposition
1821:Traditional
1792:Lindström's
1782:Compactness
1724:Type theory
1669:Cardinality
1411:satisfiable
1341:NP-complete
1258:NP-complete
1233:Constraints
1196:undecidable
643:conjunction
495:undecidable
475:NP-complete
417:unification
358:consistency
29:satisfiable
3525:Categories
3070:elementary
2763:arithmetic
2631:Quantifier
2609:functional
2481:Expression
2199:Transitive
2143:identities
2128:complement
2061:hereditary
2044:Set theory
1545:References
1269:Polynomial
1236:over reals
1190:(in class
3465:Soundness
3401:Metalogic
3341:Supertask
3244:Recursion
3202:decidable
3036:saturated
3014:of models
2937:deductive
2932:axiomatic
2852:Hilbert's
2839:Euclidean
2820:canonical
2743:axiomatic
2675:Signature
2604:Predicate
2493:Extension
2415:Ackermann
2340:Operation
2219:Universal
2209:Recursive
2184:Singleton
2179:Inhabited
2164:Countable
2154:Types of
2138:power set
2108:partition
2025:Predicate
1971:Predicate
1886:Syllogism
1876:Soundness
1849:Inference
1839:Tautology
1741:paradoxes
1306:rationals
1273:decidable
1177:decidable
1057:…
938:¬
932:∀
896:→
875:∧
842:∀
797:∃
794:→
764:∀
701:constants
539:structure
385:decidable
366:Aristotle
33:variables
3326:Logicism
3319:timeline
3295:Concrete
3154:Validity
3124:T-schema
3117:Kripke's
3112:Tarski's
3107:semantic
3097:Strength
3046:submodel
3041:spectrum
3009:function
2857:Tarski's
2846:Elements
2833:geometry
2789:Robinson
2710:variable
2695:function
2668:spectrum
2658:Sentence
2614:variable
2557:Language
2510:Relation
2471:Automata
2461:Alphabet
2445:language
2299:-jection
2277:codomain
2263:Function
2224:Universe
2194:Infinite
2098:Relation
1881:Validity
1871:Argument
1769:theorem,
1574:(2008).
1460:(2012).
1430:(1998).
1383:Validity
1357:See also
1309:integers
250:semantic
229:is not.
153:validity
3268:Related
3065:Diagram
2963: (
2942:Hilbert
2927:Systems
2922:Theorem
2800:of the
2745:systems
2525:Formula
2520:Grammar
2436: (
2380:General
2093:Forcing
2078:Element
1998:Monadic
1773:paradox
1714:Theorem
1650:General
1479:21 July
377:problem
254:meaning
25:formula
3031:finite
2794:Skolem
2747:
2722:Theory
2690:Symbol
2680:String
2663:atomic
2540:ground
2535:closed
2530:atomic
2486:ground
2449:syntax
2345:binary
2272:domain
2189:Finite
1954:finite
1812:Logics
1771:
1719:Theory
1601:
1582:
1530:
1502:
1440:
1244:Linear
1194:) and
624:finite
591:. If
421:theory
403:, and
340:. The
338:axioms
234:syntax
3021:Model
2769:Peano
2626:Proof
2466:Arity
2395:Naive
2282:image
2214:Fuzzy
2174:Empty
2123:union
2068:Class
1709:Model
1699:Lemma
1657:Axiom
1473:(PDF)
1394:Notes
1338:PTIME
1325:PTIME
1322:PTIME
1260:(see
1250:(see
1248:PTIME
1139:atoms
533:, an
314:model
157:valid
3403:and
3144:Type
2947:list
2751:list
2728:list
2717:Term
2651:rank
2545:open
2439:list
2251:Maps
2156:sets
2015:Free
1985:list
1735:list
1662:list
1599:ISBN
1580:ISBN
1528:ISBN
1500:ISBN
1481:2012
1438:ISBN
1214:and
1171:The
699:are
672:and
585:true
556:⧠Ï
489:For
435:For
415:and
375:The
312:(or
93:and
23:, a
2831:of
2813:of
2761:of
2293:Sur
2267:Map
2074:Ur-
2056:Set
1198:by
634:.
587:in
575:⧠Ï
529:In
368:'s
244:or
27:is
19:In
3527::
3217:NP
2841::
2835::
2765::
2442:),
2297:Bi
2289:In
1570:;
1514:^
1464:.
1426:;
1353:.
1294:.
1285:)
1264:)
1192:RE
1179:.
703::
606:â§
481:.
455:.
411:,
399:,
372:.
240:,
3393:e
3386:t
3379:v
3297:/
3212:P
2967:)
2753:)
2749:(
2646:â
2641:!
2636:â
2597:=
2592:â
2587:â
2582:â§
2577:âš
2572:ÂŹ
2295:/
2291:/
2265:/
2076:)
2072:(
1959:â
1949:3
1737:)
1635:e
1628:t
1621:v
1607:.
1588:.
1508:.
1483:.
1446:.
1254:)
1154:0
1150:a
1126:R
1106:)
1101:1
1097:a
1093:,
1088:0
1084:a
1080:(
1077:R
1054:,
1051:)
1046:2
1042:a
1038:,
1033:1
1029:a
1025:(
1022:R
1019:,
1016:)
1011:1
1007:a
1003:,
998:0
994:a
990:(
987:R
963:)
958:0
954:a
950:,
947:x
944:(
941:R
935:x
911:)
908:)
905:z
902:=
899:y
893:)
890:x
887:,
884:z
881:(
878:R
872:)
869:x
866:,
863:y
860:(
857:R
854:(
851:z
848:y
845:x
821:)
818:)
815:z
812:,
809:y
806:(
803:R
800:z
791:)
788:y
785:,
782:x
779:(
776:R
773:(
770:y
767:x
743:)
738:1
734:a
730:,
725:0
721:a
717:(
714:R
685:1
681:a
658:0
654:a
608:T
604:A
597:A
593:T
589:A
581:A
573:A
566:A
554:A
547:a
543:A
324:+
296:x
293:=
290:1
287:+
284:x
264:+
217:y
214:=
211:3
208:+
205:x
185:x
182:+
179:3
176:=
173:3
170:+
167:x
139:x
136:=
133:1
130:+
127:x
107:6
104:=
101:y
81:3
78:=
75:x
55:y
52:=
49:3
46:+
43:x
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.