84:
74:
53:
22:
703:
The whole article seem to miss many definitions or assume to get them from lambda calculus. When terms are defined, variables are not at all introduced. At a first look at the freely available paper, one sees no way to fully reconcile the article with the paper (in particular, it is not sufficient to
176:
From the freely online accessible paper, I see no special care about this, even if the proof is not given. However, it does not seem that strong normalization is equivalent to consistency; they are both stated as corollaries of the same, rather technical theorem (whose proof is not included - the
776:
I removed the claim that the CoC was equiconsistent with ZFC because the paper cited ("Sets in types, types in sets") doesn't prove this. It uses a stronger type theory with inductive types, the calculus of inductive constructions. If ZFC is ZFC with
502:). I can't find the deduction rule you would like to have, but it should be surely a theorem, not a rule (even because typing judgements are introduced before conversion rules; conversion rules is the equivalent of beta-conversion in that article).--
682:. In the paper, the rule of conversion is the one asked for by Chinju, and does not need that side condition. However, that side condition is often needed (depending on the details of the formalization), for instance it is needed in
756:
A note: I know lambda-calculus and have read about Curry-Howard isomorphism, but I'm not at all an expert in the subject (particularly, in the calculus of constructions - I've just tried browsing the article to make sense of it).
192:
1089:
140:
680:
500:
452:
411:
248:
740:
908:
871:
1186:
1129:
1009:
989:
516:
I retract my previous comment. The article has been changed significantly, and it now indeed includes a conversion typing rule, that is, "a rule allowing one to derive
370:
1166:
1109:
969:
632:
566:
540:
300:
274:
834:
606:
586:
340:
320:
791:, then the paper constructs a model of CIC (plus choice and excluded middle axioms) in ZFC and a model of ZFC in CIC (plus choice and excluded middle axioms.)
1256:
130:
1251:
106:
352:
The online article (Coquand and Huet, 1986) states an obvious inference rule to prove typing for variables (they have the type declared in
1210:
These terms are not defined on this page, nor anywhere else on
Knowledge as far as I can tell. They should either be defined or removed.
1228:
196:
97:
58:
213:
The inference rules presented in this article seem deficient. In particular, there is no way to prove anything of the form
918:
33:
742:). The rules of conversion are omitted from the article; and so on. I'm marking this with the {{expert}} template.--
1022:
634:
for whatever technical reasons — but that might need a citation). I even misquoted Lemma 5 above: it should read
637:
457:
21:
1232:
1215:
914:
416:
375:
762:
747:
691:
507:
182:
216:
1193:
1136:
935:
930:
They represent function application, lambda-abstraction, and dependent product formation, respectively.
796:
39:
1211:
83:
342:, or something like that. Hopefully, someone more familiar with this material can clear things up. -
167:
1132:
707:
1016:
878:
841:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
163:
89:
781:
inaccessible cardinals and CIC is the calculus of inductive constructions with sorts Prop, Type
73:
52:
758:
743:
687:
503:
178:
1171:
1114:
994:
974:
1189:
931:
792:
683:
355:
1151:
1094:
954:
611:
545:
519:
279:
253:
816:
1236:
1219:
1197:
1140:
939:
922:
800:
766:
751:
695:
591:
571:
511:
346:
325:
305:
200:
186:
170:
1245:
948:
343:
102:
79:
1012:
166:, right? So, in what system is the strong normalization theory proved?
250:
from them. I imagine what's missing is a rule allowing one to derive
15:
1111:
operator is more general. Does this need to be fixed, or is
177:
full reference given there is a PhD thesis in French). --
191:
Exаmine mу results, this is the extent of my earnings.
1148:
In this context, there is not much difference between
372:), and states as a lemma (lemma 5 on page 7) that "if
1174:
1154:
1117:
1097:
1025:
997:
977:
957:
881:
844:
819:
710:
640:
614:
608:", as Chinju wrote. (It has the extra condition that
594:
574:
548:
522:
460:
419:
378:
358:
328:
308:
282:
256:
219:
101:, a collaborative effort to improve the coverage of
913:mean? The are not defined anywhere in the article.
1180:
1160:
1123:
1103:
1083:
1003:
983:
963:
902:
865:
828:
734:
674:
626:
600:
580:
560:
534:
494:
446:
405:
364:
334:
314:
294:
268:
242:
162:CoC can represent all functions provably total in
704:assume that M and N are terms to form the term
1091:, i.e. "for all types X, T is a type", so the
1084:{\displaystyle \forall X.T:=\Pi _{X:\ast }.T}
8:
675:{\displaystyle {\Gamma \vdash N_{1}=N_{2}}}
495:{\displaystyle {\Gamma \vdash N_{1}:N_{2}}}
19:
47:
1173:
1153:
1116:
1096:
1054:
1024:
996:
991:. It's my understanding that the use of
976:
956:
951:, the calculus of constructions uses the
880:
843:
818:
709:
665:
652:
641:
639:
613:
593:
573:
547:
521:
485:
472:
461:
459:
437:
420:
418:
396:
379:
377:
357:
327:
307:
281:
255:
220:
218:
1206:Definition of "small" and "large" types
447:{\displaystyle {\Gamma \vdash M:N_{2}}}
406:{\displaystyle {\Gamma \vdash M:N_{1}}}
49:
1188:. You can use whichever you prefer.
193:2A0D:3344:1402:E10:AB91:8D9F:819D:DCE
7:
243:{\displaystyle {\Gamma \vdash x:MN}}
95:This article is within the scope of
38:It is of interest to the following
1175:
1155:
1118:
1098:
1051:
1026:
998:
978:
958:
882:
642:
462:
421:
380:
359:
221:
14:
1257:Low-priority mathematics articles
806:Clarification needed for notation
115:Knowledge:WikiProject Mathematics
1252:Start-Class mathematics articles
118:Template:WikiProject Mathematics
82:
72:
51:
20:
1131:being used in a "punning" way?
135:This article has been rated as
1078:
1072:
1044:
1038:
735:{\displaystyle (\lambda x:M)N}
726:
711:
1:
923:22:20, 24 February 2023 (UTC)
903:{\displaystyle \forall x:A.B}
866:{\displaystyle \lambda x:A.B}
109:and see a list of open tasks.
801:03:17, 3 February 2022 (UTC)
347:17:41, 2 November 2005 (UTC)
1220:01:49, 6 January 2024 (UTC)
696:21:59, 10 August 2014 (UTC)
209:Deficiencies in the article
171:08:03, 19 August 2005 (UTC)
1273:
940:19:24, 17 April 2023 (UTC)
1237:11:56, 7 April 2024 (UTC)
1198:17:35, 31 July 2023 (UTC)
767:01:14, 20 June 2008 (UTC)
752:00:46, 20 June 2008 (UTC)
568:and the beta-equality of
512:01:14, 20 June 2008 (UTC)
302:and the beta-equality of
201:09:07, 20 July 2024 (UTC)
187:01:14, 20 June 2008 (UTC)
134:
67:
46:
1181:{\displaystyle \forall }
1141:16:06, 24 May 2023 (UTC)
1124:{\displaystyle \forall }
1004:{\displaystyle \forall }
984:{\displaystyle \forall }
772:Equiconsistency with ZFC
141:project's priority scale
810:What do the notations
365:{\displaystyle \Gamma }
98:WikiProject Mathematics
1182:
1162:
1125:
1105:
1085:
1005:
985:
965:
904:
867:
830:
736:
676:
628:
602:
582:
562:
536:
496:
448:
407:
366:
336:
316:
296:
270:
244:
28:This article is rated
1183:
1163:
1126:
1106:
1086:
1019:, gets translated as
1006:
986:
966:
905:
868:
831:
737:
677:
629:
603:
583:
563:
542:from a derivation of
537:
497:
449:
408:
367:
337:
317:
297:
276:from a derivation of
271:
245:
1172:
1161:{\displaystyle \Pi }
1152:
1115:
1104:{\displaystyle \Pi }
1095:
1023:
995:
975:
971:operator instead of
964:{\displaystyle \Pi }
955:
879:
842:
817:
708:
638:
612:
592:
572:
546:
520:
458:
417:
376:
356:
326:
306:
280:
254:
217:
121:mathematics articles
627:{\displaystyle A:K}
561:{\displaystyle x:B}
535:{\displaystyle x:A}
295:{\displaystyle x:B}
269:{\displaystyle x:A}
1178:
1158:
1121:
1101:
1081:
1001:
981:
961:
915:The-erinaceous-one
900:
863:
829:{\displaystyle AB}
826:
732:
672:
624:
598:
578:
558:
532:
492:
444:
403:
362:
332:
312:
292:
266:
240:
164:higher-order logic
90:Mathematics portal
34:content assessment
684:pure type systems
601:{\displaystyle B}
581:{\displaystyle A}
335:{\displaystyle B}
315:{\displaystyle A}
155:
154:
151:
150:
147:
146:
1264:
1187:
1185:
1184:
1179:
1167:
1165:
1164:
1159:
1130:
1128:
1127:
1122:
1110:
1108:
1107:
1102:
1090:
1088:
1087:
1082:
1065:
1064:
1010:
1008:
1007:
1002:
990:
988:
987:
982:
970:
968:
967:
962:
909:
907:
906:
901:
872:
870:
869:
864:
835:
833:
832:
827:
741:
739:
738:
733:
681:
679:
678:
673:
671:
670:
669:
657:
656:
633:
631:
630:
625:
607:
605:
604:
599:
587:
585:
584:
579:
567:
565:
564:
559:
541:
539:
538:
533:
501:
499:
498:
493:
491:
490:
489:
477:
476:
453:
451:
450:
445:
443:
442:
441:
412:
410:
409:
404:
402:
401:
400:
371:
369:
368:
363:
341:
339:
338:
333:
321:
319:
318:
313:
301:
299:
298:
293:
275:
273:
272:
267:
249:
247:
246:
241:
239:
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
1272:
1271:
1267:
1266:
1265:
1263:
1262:
1261:
1242:
1241:
1208:
1170:
1169:
1150:
1149:
1113:
1112:
1093:
1092:
1050:
1021:
1020:
993:
992:
973:
972:
953:
952:
877:
876:
840:
839:
815:
814:
808:
790:
784:
774:
706:
705:
661:
648:
636:
635:
610:
609:
590:
589:
570:
569:
544:
543:
518:
517:
481:
468:
456:
455:
433:
415:
414:
392:
374:
373:
354:
353:
324:
323:
304:
303:
278:
277:
252:
251:
215:
214:
211:
160:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
1270:
1268:
1260:
1259:
1254:
1244:
1243:
1240:
1239:
1207:
1204:
1203:
1202:
1201:
1200:
1177:
1157:
1120:
1100:
1080:
1077:
1074:
1071:
1068:
1063:
1060:
1057:
1053:
1049:
1046:
1043:
1040:
1037:
1034:
1031:
1028:
1017:Hindley–Milner
1000:
980:
960:
945:
944:
943:
942:
911:
910:
899:
896:
893:
890:
887:
884:
874:
862:
859:
856:
853:
850:
847:
837:
825:
822:
807:
804:
786:
782:
773:
770:
731:
728:
725:
722:
719:
716:
713:
701:
700:
699:
698:
668:
664:
660:
655:
651:
647:
644:
623:
620:
617:
597:
577:
557:
554:
551:
531:
528:
525:
488:
484:
480:
475:
471:
467:
464:
440:
436:
432:
429:
426:
423:
399:
395:
391:
388:
385:
382:
361:
331:
311:
291:
288:
285:
265:
262:
259:
238:
235:
232:
229:
226:
223:
210:
207:
206:
205:
204:
203:
159:
156:
153:
152:
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:
1269:
1258:
1255:
1253:
1250:
1249:
1247:
1238:
1234:
1230:
1227:
1224:
1223:
1222:
1221:
1217:
1213:
1205:
1199:
1195:
1191:
1147:
1146:
1145:
1144:
1143:
1142:
1138:
1134:
1075:
1069:
1066:
1061:
1058:
1055:
1047:
1041:
1035:
1032:
1029:
1018:
1014:
950:
941:
937:
933:
929:
928:
927:
926:
925:
924:
920:
916:
897:
894:
891:
888:
885:
875:
860:
857:
854:
851:
848:
845:
838:
823:
820:
813:
812:
811:
805:
803:
802:
798:
794:
789:
780:
771:
769:
768:
764:
760:
754:
753:
749:
745:
729:
723:
720:
717:
714:
697:
693:
689:
685:
666:
662:
658:
653:
649:
645:
621:
618:
615:
595:
575:
555:
552:
549:
529:
526:
523:
515:
514:
513:
509:
505:
486:
482:
478:
473:
469:
465:
438:
434:
430:
427:
424:
397:
393:
389:
386:
383:
351:
350:
349:
348:
345:
329:
309:
289:
286:
283:
263:
260:
257:
236:
233:
230:
227:
224:
208:
202:
198:
194:
190:
189:
188:
184:
180:
175:
174:
173:
172:
169:
165:
157:
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:
1229:5.139.227.97
1225:
1212:Ablueberry87
1209:
947:On the page
946:
912:
809:
787:
778:
775:
759:Blaisorblade
755:
744:Blaisorblade
702:
688:Blaisorblade
504:Blaisorblade
212:
179:Blaisorblade
161:
137:Low-priority
136:
96:
62:Low‑priority
40:WikiProjects
1190:Spacepotato
949:Lambda cube
932:Spacepotato
793:Spacepotato
785:, ..., Type
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
1246:Categories
1011:in, e.g.
168:Jim Apple
1133:Metaweta
1013:System F
454:, then
139:on the
344:Chinju
36:scale.
873:, and
158:Total
1233:talk
1226:Bold
1216:talk
1194:talk
1168:and
1137:talk
936:talk
919:talk
797:talk
763:talk
748:talk
692:talk
686:. --
588:and
508:talk
413:and
322:and
197:talk
183:talk
1015:or
131:Low
1248::
1235:)
1218:)
1196:)
1176:∀
1156:Π
1139:)
1119:∀
1099:Π
1062:∗
1052:Π
1048::=
1027:∀
999:∀
979:∀
959:Π
938:)
921:)
883:∀
846:λ
799:)
765:)
757:--
750:)
715:λ
694:)
646:⊢
643:Γ
510:)
466:⊢
463:Γ
425:⊢
422:Γ
384:⊢
381:Γ
360:Γ
225:⊢
222:Γ
199:)
185:)
1231:(
1214:(
1192:(
1135:(
1079:]
1076:X
1073:[
1070:T
1067:.
1059::
1056:X
1045:]
1042:X
1039:[
1036:T
1033:.
1030:X
934:(
917:(
898:B
895:.
892:A
889::
886:x
861:B
858:.
855:A
852::
849:x
836:,
824:B
821:A
795:(
788:i
783:1
779:i
761:(
746:(
730:N
727:)
724:M
721::
718:x
712:(
690:(
667:2
663:N
659:=
654:1
650:N
622:K
619::
616:A
596:B
576:A
556:B
553::
550:x
530:A
527::
524:x
506:(
487:2
483:N
479::
474:1
470:N
439:2
435:N
431::
428:M
398:1
394:N
390::
387:M
330:B
310:A
290:B
287::
284:x
264:A
261::
258:x
237:N
234:M
231::
228:x
195:(
181:(
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
