418:|-for all x P(x) and talk about the using of deduction theorem because when we prove P(x) for arbitrary x we get (for all x P(x)) which is the generalization so there is no point of talking about using deduction theorem. So it is better to use the gen abbrv and use it as a mere rule of inference. And if there is a restriction of using deduction theorem the restriction is not quite clear in the article including the example proof it is bit confusing when reading the proof and the restriction said above in the article. so it will be better if someone who knows about this clarify this to me. And please let me know if there are any restrictions for deduction thm (not only in this case)
738:
and won't capture the dependency of those constants on variables in the ei-introduced formulas and later generalization can go awry (as in the example shown in an earlier section of the talk page, closely related to the broken example on the current public page, which I discuss next). Versions of predicate logic lacking function symbols will have this issue and will need a restriction on ug like "the line being generalized cannot contain (even transitively) depend on an ei line containing the variable being generalized", as in the
Gersting text cited. More complex restrictions can be formulated that allow more proofs, this one is over-restricting for simplicity.
84:
74:
53:
283:
22:
742:
That section, as discussed by others above in this talk page, is badly broken, and has been for 9 years. It can be fixed by changing so that the ei usage shown introduces a Skolem function in the first use of ei, using y(w) instead of just y. With this fix it will get along with the restrictions shown on ug but it will no longer be an example of why they are needed.
185:
158:
195:
741:
HOWEVER, the current public page goes on to discuss an example disallowed proof supposedly motivating the restrictions on the rule and that example actually uses ei to introduce a constant symbol that would need to be a functional Skolem term in order to get along with the ug rule restrictions shown.
729:
If the logic allows/requires Skolem functions (applied to the variables remaining) to be introduced by ei then the ui restrictions shown are adequate, assuming ei always introduces such terms. (We only need to prevent premises about the variable we are generalizing and avoid variable capture; we have
526:
The sources are just partial names, with no page references. I've heard of a Copi and of Morley (Cornell), but both are long of tooth.... Why not provide references to a recent source. What about all the fundamental works about the lambda calculus (Scott-Strachey, Lambek, combinators, etc.)? I cannot
725:
The real issue is how universal generalization (ug) restrictions combine with the existential instantiation (ei) rule. Correctness of ug restrictions also depends on whether the logic involved allows function symbols to properly execute the ei rule. The ug rule alone needs restrictions that depend
640:
Under "Generalization with hypotheses" an example of what can go wrong if the "second restriction" (x not occur in φ) is not followed. It seems to me that this is not a good example to demonstrate the need for the restriction, because if it is corrected so that step 4. uses a variable that does not
737:
So the rule shown on the page is fine if we assume ei does not introduce variables and further assume that function symbols are allowed and used by ei as needed. But many students learn predicate logic with no function symbols (cf. Gersting text). In that setting, ei can only introduce constants,
552:, for example). The rule can also be called "∀ introduction". "Existential generalization" is the matching rule to add an existential quantifier. The thing I have always thought was strange about this article is that there are two generalization rules but this article only talks about one. — Carl
661:
Without the second restriction, one could make the following deduction:\\ {\displaystyle \exists z\,\exists w\,(z\not =w)} {\displaystyle \exists z\,\exists w\,(z\not =w)} (Hypothesis)\\ {\displaystyle \exists w\,(y\not =w)} {\displaystyle \exists w\,(y\not =w)} (Existential instantiation)\\
436:
I'm not an expert on this subject but I happen to be studying this subject now, and it seems it is more apt to split this article into universal generalization and existential generalization, as they are two very different rules of inference for quantified statements.
733:
The example leading this talk section is easily disallowed, as it introduces x by ei, and x is a variable. The restrictions on ug shown in the page would appear to assume that ei cannot introduce variables.
140:
368:
To make this more accessible to laypeople (like your's truly), lets try an example: Suppose t=2, and x is defined on the real numbers. Suppose further that P(x) is only true if x=2. so
662:{\displaystyle y\not =x} y \not = x (Existential instantiation)\\ {\displaystyle \forall x\,(x\not =x)} {\displaystyle \forall x\,(x\not =x)} (Faulty universal generalization)\\
658:
The second restriction needs a new example where the only error is overloading the bound variable name, e.g.,\\ Let x be arbitrary\\ Assume ∀z P(z,y)\\ P(x,y)\\ ∀y P(y,y)\\
348:
II) Mendelson and
Detlovs/Podniak have (2) . However, they have a Restricted Deduction Theorem which does not apply to (2). Please correct me if I am misreading something.
216:
on
Knowledge. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the
527:
remember reading about the term "universal generalization". What about abstraction? Have you asked at the
Computer Science and Logic and Philosophy WikiProjects?
641:
occur in φ, e.g. 4. were rewritten as "(ForEvery V) V is not equal to x", the second restriction would be respected but the deduction would still be unsound.
683:
In the example given, the last two lines are redundant, because the question was asking to prove A is derivable from B and C, which line 9 establishes that.
829:
253:
243:
819:
130:
814:
824:
839:
345:
I) Enderton has (1) as a
Metatheorem and has Unrestricted Deduction Metatheorem If (1) gives (2) then these combine to give the false (3).
106:
218:
709:
The first restriction needs to be restated because it seems to allow the following invalid reasoning:\\ Assume ∃z P(z) \\ P(x)\\ ∀y P(y)
834:
394:
354:
844:
792:
97:
58:
351:(It is clear that (2) gives (1). Starting with a deduction of P(x) one attaches the deduction (2) to get a deduction of AllxP(x).)
208:
163:
33:
629:
Subsequent comments should be made in a new section on this talk page. No further edits should be made to this section.
471:
Subsequent comments should be made in a new section on the talk page. No further edits should be made to this section.
770:
290:
168:
580:
538:
726:
on the logic it is part of and the ei rule it is combining with. The page does not handle this and is broken.
602:
500:
21:
358:
796:
398:
598:
496:
646:
548:"Universal generalization" is the usual term for the inference rule that adds a universal quantifier (in
572:
530:
485:
39:
749:
83:
688:
426:
694:
642:
414:
I am not a expert on this area but I need knowledge in this area to pursue my
Mathematical studies.
745:
440:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
712:
684:
665:
610:
508:
422:
89:
73:
52:
549:
444:
378:
P(t) (from 1 and 2, by one of the axioms, we call it L12, not sure what anyone else calls it)
320:
200:
716:
669:
481:
791:(I kid you not.) How is the reader supposed to know what works are being referred to?
282:
808:
606:
559:
504:
800:
753:
720:
698:
673:
650:
585:
564:
543:
512:
489:
448:
430:
402:
362:
324:
771:
https://amazon.com/Mathematical-Structures-Computer-Science-Gersting/dp/1429215100/
620:
462:
417:
I feel that it is not a good idea to consider the generalization as a |-P(x) -: -->
316:
315:
It is not explained why the deduction theorem does not apply in this case. ----
102:
213:
190:
79:
388:
so, that would mean any number is equal to 2, so long as 2 actualy exists.
555:
212:, a collaborative effort to improve the coverage of content related to
184:
157:
15:
655:
Wow. 9 years later the example still hasn't been repaired.
281:
461:
The following discussion is an archived discussion of a
601:
will still be useful as a redirect after this move but
619:
The above discussion is preserved as an archive of a
101:, a collaborative effort to improve the coverage of
391:(Something is rotten in the kingdom of Denmark...)
264:
503:– This is the more common term for this concept.
381:P(t)|-VxP(x) (form 3 according to Gen, right?)
8:
19:
692:
261:
152:
47:
788:Copi and Cohen Hurley Moore and Parker
763:
154:
49:
222:about philosophy content on Knowledge.
7:
476:The result of the move request was:
411:Supems(17:03, 16 April 2008 (UTC)
206:This article is within the scope of
95:This article is within the scope of
605:is definitely the common term now.
38:It is of interest to the following
830:Mid-importance Philosophy articles
333:Let 1) If |-P(x) then |- AllxP(x)
14:
820:Low-priority mathematics articles
115:Knowledge:WikiProject Mathematics
815:Start-Class mathematics articles
228:Knowledge:WikiProject Philosophy
193:
183:
156:
118:Template:WikiProject Mathematics
82:
72:
51:
20:
825:Start-Class Philosophy articles
342:I think (1) does not give (2).
248:This article has been rated as
231:Template:WikiProject Philosophy
135:This article has been rated as
449:04:31, 12 September 2010 (UTC)
1:
840:Mid-importance logic articles
699:02:49, 21 November 2017 (UTC)
569:Carl's word suffices for me.
363:22:35, 22 November 2007 (UTC)
325:18:13, 16 November 2007 (UTC)
109:and see a list of open tasks.
754:21:44, 1 February 2021 (UTC)
651:11:32, 9 November 2012 (UTC)
403:15:05, 12 January 2011 (UTC)
861:
835:Start-Class logic articles
801:15:42, 23 March 2019 (UTC)
721:21:06, 22 March 2019 (UTC)
674:21:06, 22 March 2019 (UTC)
586:13:32, 13 March 2012 (UTC)
565:12:57, 13 March 2012 (UTC)
544:12:22, 13 March 2012 (UTC)
513:22:23, 10 March 2012 (UTC)
490:21:05, 17 March 2012 (UTC)
431:17:09, 16 April 2008 (UTC)
254:project's importance scale
845:Logic task force articles
289:
260:
247:
178:
134:
67:
46:
626:Please do not modify it.
603:Universal generalization
501:Universal generalization
468:Please do not modify it.
141:project's priority scale
375:P(x)) (by definition).
265:Associated task forces:
98:WikiProject Mathematics
730:no worries about ei.)
599:Generalization (logic)
497:Generalization (logic)
330:(I am not a logician)
286:
209:WikiProject Philosophy
28:This article is rated
705:The First Restriction
285:
785:The references are
636:Example is not good?
384:thus t=2|-P(t)-: -->
121:mathematics articles
385:VxP(x) (deduction)
234:Philosophy articles
679:Example of a Proof
336:2) P(x)|-AllxP(x)
287:
219:general discussion
90:Mathematics portal
34:content assessment
701:
584:
563:
550:natural deduction
542:
371:t=2 (hypothesys)
308:
307:
304:
303:
300:
299:
296:
295:
201:Philosophy portal
151:
150:
147:
146:
852:
773:
768:
628:
583:
577:
570:
553:
541:
535:
528:
470:
272:
262:
236:
235:
232:
229:
226:
203:
198:
197:
196:
187:
180:
179:
174:
171:
160:
153:
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
860:
859:
855:
854:
853:
851:
850:
849:
805:
804:
783:
778:
777:
776:
769:
765:
707:
681:
638:
633:
624:
573:
571:
531:
529:
466:
456:
313:
270:
233:
230:
227:
224:
223:
199:
194:
192:
172:
166:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
858:
856:
848:
847:
842:
837:
832:
827:
822:
817:
807:
806:
782:
779:
775:
774:
762:
761:
757:
706:
703:
697:comment added
680:
677:
637:
634:
632:
631:
621:requested move
615:
614:
592:
591:
590:
589:
588:
495:
493:
474:
473:
463:requested move
457:
455:
452:
435:
410:
407:
329:
312:
311:Generalization
309:
306:
305:
302:
301:
298:
297:
294:
293:
288:
278:
277:
275:
273:
267:
266:
258:
257:
250:Mid-importance
246:
240:
239:
237:
205:
204:
188:
176:
175:
173:Mid‑importance
161:
149:
148:
145:
144:
133:
127:
126:
124:
107:the discussion
94:
93:
77:
65:
64:
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
857:
846:
843:
841:
838:
836:
833:
831:
828:
826:
823:
821:
818:
816:
813:
812:
810:
803:
802:
798:
794:
789:
786:
780:
772:
767:
764:
760:
756:
755:
751:
747:
743:
739:
735:
731:
727:
723:
722:
718:
714:
710:
704:
702:
700:
696:
690:
686:
678:
676:
675:
671:
667:
663:
659:
656:
653:
652:
648:
644:
635:
630:
627:
622:
617:
616:
612:
608:
604:
600:
596:
593:
587:
582:
578:
576:
568:
567:
566:
561:
557:
551:
547:
546:
545:
540:
536:
534:
525:
522:
521:
517:
516:
515:
514:
510:
506:
502:
498:
492:
491:
487:
483:
479:
472:
469:
464:
459:
458:
454:Move proposal
453:
451:
450:
446:
442:
438:
433:
432:
428:
424:
419:
415:
412:
408:
405:
404:
400:
396:
395:195.13.158.11
392:
389:
386:
382:
379:
376:
374:Vx (x=2-: -->
372:
369:
366:
364:
360:
356:
355:128.241.40.80
352:
349:
346:
343:
340:
339:3)|- False
337:
334:
331:
327:
326:
322:
318:
310:
292:
284:
280:
279:
276:
274:
269:
268:
263:
259:
255:
251:
245:
242:
241:
238:
221:
220:
215:
211:
210:
202:
191:
189:
186:
182:
181:
177:
170:
165:
162:
159:
155:
142:
138:
132:
129:
128:
125:
108:
104:
100:
99:
91:
85:
80:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
793:31.50.156.39
790:
787:
784:
766:
758:
744:
740:
736:
732:
728:
724:
711:
708:
682:
664:
660:
657:
654:
639:
625:
618:
594:
574:
532:
523:
519:
518:
494:
477:
475:
467:
460:
439:
434:
420:
416:
413:
409:
406:
393:
390:
387:
383:
380:
377:
373:
370:
367:
353:
350:
347:
344:
341:
338:
335:
332:
328:
314:
249:
217:
207:
137:Low-priority
136:
96:
62:Low‑priority
40:WikiProjects
693:—Preceding
482:Vegaswikian
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
809:Categories
781:References
759:References
478:page moved
365:A. Reader
225:Philosophy
214:philosophy
164:Philosophy
643:Tom Cohoe
607:Mark Hurd
581:Wolfowitz
539:Wolfowitz
505:Greg Bard
746:Rgivan1
695:undated
595:Support
441:Vsaraph
421:Thanks
317:NoizHed
252:on the
139:on the
713:ProfRB
685:LoMaPh
666:ProfRB
575:Kiefer
533:Kiefer
423:Supems
36:scale.
291:Logic
169:Logic
797:talk
750:talk
717:talk
689:talk
670:talk
647:talk
611:talk
560:talk
524:Okay
520:Hold
509:talk
486:talk
445:talk
427:talk
399:talk
359:talk
321:talk
691:)
623:.
556:CBM
244:Mid
131:Low
811::
799:)
752:)
719:)
672:)
649:)
597:.
558:·
511:)
499:→
488:)
480:.
465:.
447:)
429:)
401:)
361:)
323:)
271:/
167::
795:(
748:(
715:(
687:(
668:(
645:(
613:)
609:(
579:.
562:)
554:(
537:.
507:(
484:(
443:(
425:(
397:(
357:(
319:(
256:.
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
