940:
567:
In terms of models, pure theory of equality can be defined as set of those first-order sentences that are true for all (non-empty) sets, regardless of their cardinality. For example, the following is a valid formula in the pure theory of equality:
709:
534:
737:, one can expand the signature of the language while preserving the definable relations (a technique that works more generally for monadic second-order formulas). Another approach to establish decidability is to use
317:
201:
227:
574:
730:
Decidability can be shown by establishing that every sentence can be shown equivalent to a propositional combination of formulas about the cardinality of the domain.
405:
433:
169:
143:
557:
425:
378:
358:
50:
theory and is a fragment of more expressive decidable theories, including monadic class of first-order logic (which also admits unary predicates and is, via
171:
are (possibly identical) variables. Syntactically more complex formulas can be built as usual in first-order logic using propositional connectives such as
236:
interpreting such formulas is just a set with the equality relation on its elements. Isomorphic structures with such signature are thus sets of the same
981:
918:
797:
738:
66:
of a pure set (which additionally permits quantification over predicates and whose signature extends to monadic second-order logic of
1005:
838:
32:
974:
750:
254:
63:
46:
with the usual equality relation provides an interpretation making certain sentences true. It is an example of a
714:
By completeness of first-order logic, all valid formulas are provable using axioms of first-order logic and the
1000:
967:
335:
734:
559:
elements. More generally, it can constrain the domain to have a given finite set of finite cardinalities.
331:
100:, or an axiom scheme is added saying that there are infinitely many objects, then the resulting theory is
174:
704:{\displaystyle (\forall x,y,z.\ (z=x\lor z=y))\lor (\exists p,q,r.\ p\neq q\land p\neq r\land q\neq r)}
206:
116:
with equality, where the only predicate symbol is equality itself and there are no function symbols.
83:
79:
47:
947:
883:
844:
233:
51:
20:
914:
834:
793:
715:
113:
43:
28:
35:
consisting of only the equality relation symbol, and includes no non-logical axioms at all.
875:
826:
818:
755:
719:
529:{\displaystyle \exists x_{1},\ldots ,x_{k}.\ \bigwedge _{1\leq i<j\leq k}x_{i}\neq x_{j}}
59:
813:
Bachmair, L.; Ganzinger, H.; Waldmann, U. (1993). "Set constraints are the monadic class".
383:
910:
830:
789:
101:
148:
122:
951:
542:
410:
363:
343:
94:
55:
994:
903:
782:
815:[1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science
240:. Cardinality thus uniquely determines whether a sentence is true in the structure.
848:
863:
760:
340:
This theory can express the fact that the domain of interpretation has at least
237:
39:
822:
901:
Monk, J. Donald (1976). "Chapter 13: Some
Decidable Theories, Lemma 13.11".
322:
is true when the set interpreting the formula has at most two elements.
939:
887:
864:"Decidability of Second-Order Theories and Automata on Infinite Trees"
879:
539:
Using negation, it can then express that the domain has more than
780:
Monk, J. Donald (1976). "Chapter 13: Some
Decidable Theories".
89:
If an additional axiom is added saying that there are exactly
955:
577:
545:
436:
413:
386:
366:
346:
257:
209:
177:
151:
125:
119:
Consequently, the only form of an atomic formula is
909:. Graduate Texts in Mathematics. Berlin, New York:
788:. Graduate Texts in Mathematics. Berlin, New York:
902:
781:
703:
551:
528:
419:
399:
372:
352:
311:
221:
195:
163:
137:
868:Transactions of the American Mathematical Society
112:The pure theory of equality contains formulas of
975:
312:{\displaystyle \forall x,y,z.\ (z=x\lor z=y)}
78:The theory of pure equality was proven to be
8:
982:
968:
576:
544:
520:
507:
479:
463:
444:
435:
412:
391:
385:
365:
345:
256:
208:
176:
150:
124:
772:
380:using the formula that we will denote
7:
936:
934:
234:first-order structure with equality
196:{\displaystyle \land ,\lor ,\lnot }
641:
581:
437:
258:
216:
210:
190:
14:
222:{\displaystyle \forall ,\exists }
938:
862:Rabin, Michael O. (July 1969).
42:but incomplete, as a non-empty
831:11858/00-001M-0000-0014-B322-4
698:
638:
632:
629:
605:
578:
306:
282:
1:
954:. You can help Knowledge by
751:List of first-order theories
16:Decidable theory of equality
64:monadic second-order theory
1022:
933:
329:
739:Ehrenfeucht–Fraïssé games
1006:Mathematical logic stubs
823:10.1109/LICS.1993.287598
563:Definition of the theory
360:elements for a constant
108:Definition as FOL theory
336:Counting quantification
248:The following formula:
74:Historical significance
25:theory of pure equality
950:-related article is a
735:quantifier elimination
705:
553:
530:
421:
401:
374:
354:
332:Spectrum of a sentence
313:
223:
197:
165:
139:
706:
554:
531:
422:
402:
400:{\displaystyle D_{k}}
375:
355:
330:Further information:
314:
224:
198:
166:
140:
575:
543:
434:
411:
384:
364:
344:
255:
207:
175:
149:
123:
93:objects for a fixed
164:{\displaystyle x,y}
138:{\displaystyle x=y}
948:mathematical logic
905:Mathematical Logic
817:. pp. 75–83.
784:Mathematical Logic
701:
549:
526:
502:
417:
397:
370:
350:
309:
219:
193:
161:
135:
52:Skolem normal form
29:first-order theory
21:mathematical logic
963:
962:
920:978-0-387-90170-1
799:978-0-387-90170-1
664:
604:
552:{\displaystyle k}
475:
474:
420:{\displaystyle k}
373:{\displaystyle k}
353:{\displaystyle k}
281:
114:first-order logic
84:Leopold Löwenheim
1013:
984:
977:
970:
942:
935:
925:
924:
908:
898:
892:
891:
859:
853:
852:
810:
804:
803:
787:
777:
756:Equational logic
720:equational logic
710:
708:
707:
702:
662:
602:
558:
556:
555:
550:
535:
533:
532:
527:
525:
524:
512:
511:
501:
472:
468:
467:
449:
448:
426:
424:
423:
418:
406:
404:
403:
398:
396:
395:
379:
377:
376:
371:
359:
357:
356:
351:
326:Expressive power
318:
316:
315:
310:
279:
228:
226:
225:
220:
203:and quantifiers
202:
200:
199:
194:
170:
168:
167:
162:
144:
142:
141:
136:
60:program analysis
1021:
1020:
1016:
1015:
1014:
1012:
1011:
1010:
1001:Formal theories
991:
990:
989:
988:
931:
929:
928:
921:
913:. p. 241.
911:Springer-Verlag
900:
899:
895:
880:10.2307/1995086
861:
860:
856:
841:
812:
811:
807:
800:
792:. p. 240.
790:Springer-Verlag
779:
778:
774:
769:
747:
728:
716:equality axioms
573:
572:
565:
541:
540:
516:
503:
459:
440:
432:
431:
409:
408:
407:for a constant
387:
382:
381:
362:
361:
342:
341:
338:
328:
253:
252:
246:
205:
204:
173:
172:
147:
146:
121:
120:
110:
76:
56:set constraints
38:This theory is
17:
12:
11:
5:
1019:
1017:
1009:
1008:
1003:
993:
992:
987:
986:
979:
972:
964:
961:
960:
943:
927:
926:
919:
893:
854:
839:
805:
798:
771:
770:
768:
765:
764:
763:
758:
753:
746:
743:
727:
724:
712:
711:
700:
697:
694:
691:
688:
685:
682:
679:
676:
673:
670:
667:
661:
658:
655:
652:
649:
646:
643:
640:
637:
634:
631:
628:
625:
622:
619:
616:
613:
610:
607:
601:
598:
595:
592:
589:
586:
583:
580:
564:
561:
548:
537:
536:
523:
519:
515:
510:
506:
500:
497:
494:
491:
488:
485:
482:
478:
471:
466:
462:
458:
455:
452:
447:
443:
439:
416:
394:
390:
369:
349:
327:
324:
320:
319:
308:
305:
302:
299:
296:
293:
290:
287:
284:
278:
275:
272:
269:
266:
263:
260:
245:
242:
218:
215:
212:
192:
189:
186:
183:
180:
160:
157:
154:
134:
131:
128:
109:
106:
95:natural number
75:
72:
15:
13:
10:
9:
6:
4:
3:
2:
1018:
1007:
1004:
1002:
999:
998:
996:
985:
980:
978:
973:
971:
966:
965:
959:
957:
953:
949:
944:
941:
937:
932:
922:
916:
912:
907:
906:
897:
894:
889:
885:
881:
877:
873:
869:
865:
858:
855:
850:
846:
842:
840:0-8186-3140-6
836:
832:
828:
824:
820:
816:
809:
806:
801:
795:
791:
786:
785:
776:
773:
766:
762:
759:
757:
754:
752:
749:
748:
744:
742:
740:
736:
731:
725:
723:
721:
717:
695:
692:
689:
686:
683:
680:
677:
674:
671:
668:
665:
659:
656:
653:
650:
647:
644:
635:
626:
623:
620:
617:
614:
611:
608:
599:
596:
593:
590:
587:
584:
571:
570:
569:
562:
560:
546:
521:
517:
513:
508:
504:
498:
495:
492:
489:
486:
483:
480:
476:
469:
464:
460:
456:
453:
450:
445:
441:
430:
429:
428:
414:
392:
388:
367:
347:
337:
333:
325:
323:
303:
300:
297:
294:
291:
288:
285:
276:
273:
270:
267:
264:
261:
251:
250:
249:
243:
241:
239:
235:
230:
213:
187:
184:
181:
178:
158:
155:
152:
132:
129:
126:
117:
115:
107:
105:
103:
99:
96:
92:
87:
85:
81:
73:
71:
70:successors).
69:
65:
61:
57:
54:, related to
53:
49:
45:
41:
36:
34:
30:
26:
22:
956:expanding it
945:
930:
904:
896:
871:
867:
857:
814:
808:
783:
775:
732:
729:
726:Decidability
713:
566:
538:
339:
321:
247:
231:
118:
111:
97:
90:
88:
77:
67:
37:
24:
18:
761:Free theory
238:cardinality
31:. It has a
995:Categories
767:References
733:To obtain
718:(see also
86:in 1915.
40:consistent
693:≠
687:∧
681:≠
675:∧
669:≠
642:∃
636:∨
618:∨
582:∀
514:≠
496:≤
484:≤
477:⋀
454:…
438:∃
295:∨
259:∀
217:∃
211:∀
191:¬
185:∨
179:∧
80:decidable
48:decidable
33:signature
874:: 1–35.
745:See also
102:complete
888:1995086
849:2351050
244:Example
917:
886:
847:
837:
796:
663:
603:
473:
280:
145:where
62:) and
946:This
884:JSTOR
845:S2CID
27:is a
952:stub
915:ISBN
835:ISBN
794:ISBN
490:<
334:and
23:the
876:doi
872:141
827:hdl
819:doi
722:).
82:by
58:in
44:set
19:In
997::
882:.
870:.
866:.
843:.
833:.
825:.
741:.
427::
232:A
229:.
104:.
983:e
976:t
969:v
958:.
923:.
890:.
878::
851:.
829::
821::
802:.
699:)
696:r
690:q
684:r
678:p
672:q
666:p
660:.
657:r
654:,
651:q
648:,
645:p
639:(
633:)
630:)
627:y
624:=
621:z
615:x
612:=
609:z
606:(
600:.
597:z
594:,
591:y
588:,
585:x
579:(
547:k
522:j
518:x
509:i
505:x
499:k
493:j
487:i
481:1
470:.
465:k
461:x
457:,
451:,
446:1
442:x
415:k
393:k
389:D
368:k
348:k
307:)
304:y
301:=
298:z
292:x
289:=
286:z
283:(
277:.
274:z
271:,
268:y
265:,
262:x
214:,
188:,
182:,
159:y
156:,
153:x
133:y
130:=
127:x
98:m
91:m
68:k
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.