1051:
755:
of a formula is obtained similarly, except that in the second step above, we would delete quantifiers on variables that are either (1) existentially quantified and within an even number of negations, or (2) universally quantified and within an odd number of negations. Thus, considering the same
196:
Second, delete all quantifiers on variables that are either (1) universally quantified and within an even number of negation signs, or (2) existentially quantified and within an odd number of negation signs.
279:
438:
325:
902:
746:
510:
487:
633:
979:
557:
464:
774:
597:
577:
530:
345:
217:
191:
167:
140:
120:
96:
937:
Skolem, T. "Logico-combinatorial investigations in the satisfiability or provability of mathematical propositions: A simplified proof of a theorem by
51:(Skolem 1920). Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove
908:
52:
122:
contains no variable that is bound by two different quantifier occurrences, and that no variable occurs both bound and free. (That is,
988:
912:
48:
1105:
965:
1131:
972:
944:
Herbrand, J. "Investigations in proof theory: The properties of true propositions". (In van
Heijenoort 1967, 525-81.)
222:
1015:
1010:
924:
354:
997:
142:
could be relettered to ensure these conditions, in such a way that the result is an equivalent formula).
1035:
1020:
284:
32:
782:
641:
1030:
1024:
1005:
938:
947:
59:
1100:
1077:
1067:
492:
469:
1059:
602:
99:
1095:
1087:
67:
28:
535:
1050:
24:
443:
1126:
759:
582:
562:
515:
330:
202:
176:
152:
125:
105:
81:
63:
40:
1120:
36:
1040:
44:
466:
are the kind we consider for the second step, so we delete the quantifiers
327:
are the variables that are still quantified, and whose quantifiers govern
957:
941:
and generalizations of the theorem". (In van
Heijenoort 1967, 252-63.)
70:: the resulting formula is valid if and only if the original one is.
951:
From Frege to Gödel: A Source Book in
Mathematical Logic, 1879-1931
62:
961:
907:
To understand the significance of these constructions, see
440:. There are no free variables to replace. The variables
66:, Herbrandization being Skolemization's dual preserves
785:
762:
644:
605:
585:
565:
538:
518:
495:
472:
446:
357:
333:
287:
225:
205:
179:
155:
128:
108:
84:
1086:
1058:
996:
896:
768:
740:
627:
591:
571:
551:
524:
504:
481:
458:
432:
339:
319:
273:
211:
185:
161:
134:
114:
90:
559:(since there were no other quantifiers governing
43:had considered the Skolemizations of formulas in
973:
8:
980:
966:
958:
864:
824:
790:
784:
761:
714:
677:
649:
643:
610:
604:
584:
564:
543:
537:
517:
494:
471:
445:
356:
332:
311:
292:
286:
274:{\displaystyle f_{v}(x_{1},\dots ,x_{k})}
262:
243:
230:
224:
204:
178:
154:
127:
107:
83:
58:The resulting formula is not necessarily
776:from above, its Skolemization would be:
433:{\displaystyle F:=\forall y\exists x}
173:First, replace any free variables in
7:
199:Finally, replace each such variable
351:For instance, consider the formula
953:. Harvard University Press, 1967.
848:
845:
799:
695:
658:
496:
473:
403:
400:
370:
364:
320:{\displaystyle x_{1},\dots ,x_{k}}
14:
1049:
897:{\displaystyle F^{S}=\forall y.}
741:{\displaystyle F^{H}=\exists x.}
98:be a formula in the language of
1106:Normal form (natural deduction)
888:
885:
876:
870:
857:
839:
836:
830:
811:
805:
732:
729:
726:
720:
701:
689:
670:
664:
622:
616:
427:
424:
412:
394:
382:
376:
268:
236:
1:
169:is then obtained as follows:
512:. Finally, we then replace
47:as part of his proof of the
31:) is a construction that is
16:Proof of Herbrand's theorem
1148:
1047:
505:{\displaystyle \exists z}
482:{\displaystyle \forall y}
913:Löwenheim–Skolem theorem
628:{\displaystyle f_{z}(x)}
49:Löwenheim–Skolem theorem
1016:Disjunctive normal form
1011:Conjunctive normal form
925:Predicate functor logic
599:with a function symbol
219:with a function symbol
74:Definition and examples
898:
770:
742:
629:
593:
573:
553:
526:
506:
483:
460:
434:
341:
321:
275:
213:
187:
163:
136:
116:
102:. We may assume that
92:
1036:Canonical normal form
1021:Algebraic normal form
899:
771:
743:
630:
594:
574:
554:
552:{\displaystyle c_{y}}
527:
507:
484:
461:
435:
342:
322:
276:
214:
188:
164:
137:
117:
93:
1132:Normal forms (logic)
1031:Blake canonical form
1025:Zhegalkin polynomial
1006:Negation normal form
783:
760:
642:
603:
583:
563:
536:
516:
493:
470:
444:
355:
331:
285:
223:
203:
193:by constant symbols.
177:
153:
126:
106:
82:
998:Propositional logic
459:{\displaystyle y,z}
1101:Modal clausal form
1078:Prenex normal form
1068:Skolem normal form
948:van Heijenoort, J.
909:Herbrand's theorem
894:
766:
738:
625:
589:
579:), and we replace
569:
549:
522:
502:
479:
456:
430:
337:
317:
271:
209:
183:
159:
132:
112:
88:
53:Herbrand's theorem
1114:
1113:
769:{\displaystyle F}
592:{\displaystyle z}
572:{\displaystyle y}
525:{\displaystyle y}
340:{\displaystyle v}
212:{\displaystyle v}
186:{\displaystyle F}
162:{\displaystyle F}
135:{\displaystyle F}
115:{\displaystyle F}
100:first-order logic
91:{\displaystyle F}
55:(Herbrand 1930).
1139:
1096:Beta normal form
1053:
982:
975:
968:
959:
903:
901:
900:
895:
869:
868:
829:
828:
795:
794:
775:
773:
772:
767:
747:
745:
744:
739:
719:
718:
682:
681:
654:
653:
634:
632:
631:
626:
615:
614:
598:
596:
595:
590:
578:
576:
575:
570:
558:
556:
555:
550:
548:
547:
532:with a constant
531:
529:
528:
523:
511:
509:
508:
503:
488:
486:
485:
480:
465:
463:
462:
457:
439:
437:
436:
431:
346:
344:
343:
338:
326:
324:
323:
318:
316:
315:
297:
296:
280:
278:
277:
272:
267:
266:
248:
247:
235:
234:
218:
216:
215:
210:
192:
190:
189:
184:
168:
166:
165:
160:
141:
139:
138:
133:
121:
119:
118:
113:
97:
95:
94:
89:
29:Jacques Herbrand
1147:
1146:
1142:
1141:
1140:
1138:
1137:
1136:
1117:
1116:
1115:
1110:
1082:
1073:Herbrandization
1060:Predicate logic
1054:
1045:
992:
986:
956:
933:
921:
860:
820:
786:
781:
780:
758:
757:
710:
673:
645:
640:
639:
606:
601:
600:
581:
580:
561:
560:
539:
534:
533:
514:
513:
491:
490:
468:
467:
442:
441:
353:
352:
329:
328:
307:
288:
283:
282:
258:
239:
226:
221:
220:
201:
200:
175:
174:
151:
150:
147:Herbrandization
124:
123:
104:
103:
80:
79:
76:
39:of a formula.
25:logical formula
21:Herbrandization
17:
12:
11:
5:
1145:
1143:
1135:
1134:
1129:
1119:
1118:
1112:
1111:
1109:
1108:
1103:
1098:
1092:
1090:
1084:
1083:
1081:
1080:
1075:
1070:
1064:
1062:
1056:
1055:
1048:
1046:
1044:
1043:
1038:
1033:
1028:
1018:
1013:
1008:
1002:
1000:
994:
993:
987:
985:
984:
977:
970:
962:
955:
954:
945:
942:
934:
932:
929:
928:
927:
920:
917:
905:
904:
893:
890:
887:
884:
881:
878:
875:
872:
867:
863:
859:
856:
853:
850:
847:
844:
841:
838:
835:
832:
827:
823:
819:
816:
813:
810:
807:
804:
801:
798:
793:
789:
765:
749:
748:
737:
734:
731:
728:
725:
722:
717:
713:
709:
706:
703:
700:
697:
694:
691:
688:
685:
680:
676:
672:
669:
666:
663:
660:
657:
652:
648:
624:
621:
618:
613:
609:
588:
568:
546:
542:
521:
501:
498:
478:
475:
455:
452:
449:
429:
426:
423:
420:
417:
414:
411:
408:
405:
402:
399:
396:
393:
390:
387:
384:
381:
378:
375:
372:
369:
366:
363:
360:
349:
348:
336:
314:
310:
306:
303:
300:
295:
291:
270:
265:
261:
257:
254:
251:
246:
242:
238:
233:
229:
208:
197:
194:
182:
158:
131:
111:
87:
75:
72:
64:satisfiability
41:Thoralf Skolem
15:
13:
10:
9:
6:
4:
3:
2:
1144:
1133:
1130:
1128:
1125:
1124:
1122:
1107:
1104:
1102:
1099:
1097:
1094:
1093:
1091:
1089:
1085:
1079:
1076:
1074:
1071:
1069:
1066:
1065:
1063:
1061:
1057:
1052:
1042:
1039:
1037:
1034:
1032:
1029:
1026:
1022:
1019:
1017:
1014:
1012:
1009:
1007:
1004:
1003:
1001:
999:
995:
990:
983:
978:
976:
971:
969:
964:
963:
960:
952:
949:
946:
943:
940:
936:
935:
930:
926:
923:
922:
918:
916:
914:
910:
891:
882:
879:
873:
865:
861:
854:
851:
842:
833:
825:
821:
817:
814:
808:
802:
796:
791:
787:
779:
778:
777:
763:
754:
753:Skolemization
735:
723:
715:
711:
707:
704:
698:
692:
686:
683:
678:
674:
667:
661:
655:
650:
646:
638:
637:
636:
619:
611:
607:
586:
566:
544:
540:
519:
499:
476:
453:
450:
447:
421:
418:
415:
409:
406:
397:
391:
388:
385:
379:
373:
367:
361:
358:
334:
312:
308:
304:
301:
298:
293:
289:
263:
259:
255:
252:
249:
244:
240:
231:
227:
206:
198:
195:
180:
172:
171:
170:
156:
148:
143:
129:
109:
101:
85:
73:
71:
69:
65:
61:
56:
54:
50:
46:
42:
38:
37:Skolemization
34:
30:
27:(named after
26:
22:
1072:
989:Normal forms
950:
939:L. Löwenheim
906:
752:
750:
350:
146:
144:
77:
57:
20:
18:
1041:Horn clause
45:prenex form
1121:Categories
931:References
60:equivalent
849:∃
846:¬
843:∧
800:∀
696:¬
693:∧
659:∃
497:∃
474:∀
404:∃
401:¬
398:∧
371:∃
365:∀
302:…
253:…
991:in logic
919:See also
281:, where
68:validity
911:or the
35:to the
1127:Logic
1088:Other
23:of a
751:The
489:and
145:The
78:Let
33:dual
19:The
149:of
1123::
915:.
635::
362::=
1027:)
1023:(
981:e
974:t
967:v
892:.
889:]
886:)
883:z
880:,
877:)
874:y
871:(
866:x
862:f
858:(
855:S
852:z
840:)
837:)
834:y
831:(
826:x
822:f
818:,
815:y
812:(
809:R
806:[
803:y
797:=
792:S
788:F
764:F
736:.
733:]
730:)
727:)
724:x
721:(
716:z
712:f
708:,
705:x
702:(
699:S
690:)
687:x
684:,
679:y
675:c
671:(
668:R
665:[
662:x
656:=
651:H
647:F
623:)
620:x
617:(
612:z
608:f
587:z
567:y
545:y
541:c
520:y
500:z
477:y
454:z
451:,
448:y
428:]
425:)
422:z
419:,
416:x
413:(
410:S
407:z
395:)
392:x
389:,
386:y
383:(
380:R
377:[
374:x
368:y
359:F
347:.
335:v
313:k
309:x
305:,
299:,
294:1
290:x
269:)
264:k
260:x
256:,
250:,
245:1
241:x
237:(
232:v
228:f
207:v
181:F
157:F
130:F
110:F
86:F
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.