84:
74:
53:
22:
162:
1183:
or how the Goedel number of a number can be constructed. For example, it seems like for these tasks, the operation 10^n for every n must be defined (if the Goedel numbers are concatenated in their decimal representation, as in the article), and I can't see how this can be done without additional symbols.
1182:
It seems to me that a minimal suitable formal arithmetic should include additional symbols, such as either a "member of" and "s" for a set, or alternatively a "F" for a formula. Otherwise, it's hard to see how for example the fact that a formula is well-formed can be expressed within the arithmetics,
989:
2. S will prove that the value of f(f(f(...f(M))))=M' where M is any initial memory state and M' is the state after a finite number N of steps. (The equivalent condition in Godel is that S will determine the value of any primitive recursive function). For the corollary, it is also necessary to assume
1139:
1- The goal of this page is not to provide content for a course on logic. I consider that it has rather a historical importance, as it allows to understand the original proof of Gödel. The proof you propose, though maybe clearer, is not the proof that was shown in 1930 by Gödel in front of a few of
985:
1. S is capable of stating any theorem about the memory state of a computer program. Each clock cycle of a computer takes a certain memory state M to M'=f(M), where the memory contents M can be viewed as a big integer and f is a simple computable function which does one processor step. The theorems
689:
Note that for every specific number n and formula F(y), q(n,G(F)) is a straightforward (though complicated) arithmetical relation between two numbers n and G(F), building on the relation PF defined earlier. Further, q(n,G(F)) is provable if the finite list of formulas encoded by n is not a proof of
654:
As it is the article is very vague about exactly what theory is being considered. The article assumes that the language is that of Peano arithmetic, but doesn't go into detail about the inference rules, etc. If you would rather specialize the article to just consider Peano arithmetic, I wouldn't
592:
I started working on the article this afternoon. Terms like "statement" and "statement form" ought to be replaced with the standard terminology - "sentences" or "well formed formulas". I tried to integrate the coding by
Hofstadter from higher on this page, although I'm not sure about the variable
979:
because they avoid using the idea of a computer program. Since all modern readers know what a computer program is, a proof today should be completely trivial. I have tried to include such a discussion in the past, but I have been censured for it. I include it here, for the benefit of new editors.
617:
The new section on Godel numbers isn't right (because it is copied from the WP article on Godel numbers that also isn't right). It makes no sense to say that a Godel nubering function is computable. Moreover, the numbering must have important properties, so not just any assignment will do. I'll
1186:
If additional symbols are indeed necessary, this should be noted somewhere. If not, can someone please explain how to construct the above examples without aditional symbols? (with the "member of" and "s" for a set it is clear to me how this can be done, assuming that the deduction rules and some
265:
I feel that "definability of provability" is quite an important requirement to the proof, and probably technically a bit difficult to handle. This can't be addressed in just a few lines of text. I would appreciate a concrete example of how to write down a proof as a formula, using only the given
978:
My often stated opinion, although not on this talk page so I repeat it, is that there is a problem with this type of discussion. It follows Godel's original work too closely. The arithmetization of syntax and the construction of a proposition which asserts its own unprovability are complicated,
884:
Now consider formula Q(x) with free variable x, with Godel number G(Q). There is a function f that maps G(Q) to G(Q(G(Q))). For example, let Q(x) be "400+x=3020". Let G(Q)=21300. Then, Q(G(Q)) is "400+21300=3020". Let the Godel number of this new formula G(Q(G(Q)))=619483. Then, f maps 21300 to
767:"For all natural numbers n, q(n,G(P)) is provable." says: q(1, 21300), q(2, 21300), q(3, 21300), ... , are all provable. (This is so because none of the numbers 1,2,3, ... , is the Godel number of a proof of the formula P(G(P)) ("400+21300=3020").) However, this does not imply that the formula "
1146:
3- The formulation you prodive does not underline the universality of Gödel's result. Computers only exist in our era, while Gödel's theorem is a statement about the first-order logic which has been an implicit framework for mathematics during centuries. For a universal theorem, the universal
417:
As it stands, this article needs a lot of work, so you may want to consult a print reference for details. The idea is that the functions stand for inference rules, and P is the smallest set of Godel numbers containing the Godel numbers of the axioms and closed under the inference rules.
209:
This looks like a good start; I haven't read it in detail, but I see that certain things that need to be proved are currently just asserted, such as the definability of provability. There are a few things that could be done easily to improve the article. Feel free to
698:
2) The 9 th paragraph of "Self-referential formula" states that "P(G(P)) is not provable." while the 10 th paragraph state that P(G(P)) is provable ("for all natural numbers n, q(n,G(P)) is provable."), can someone explain if there is any contradiction?
990:
that S can prove property 2 is true of itself, S needs to prove that S proves these theorems for all N and some special M. In arithmetic this holds when S has at least enough mathematical induction to prove theorems with one (forall X) in front.
304:
of a statement S is of the form (P_1, P_2, ..., P_n), where P_n=S, each P_i is either an axiom or a statement provable from (some statements chosen from) P_1, P_2, ..., P_{i-1}. (For example, P_2, P_4 proves P_8, by deduction rule
986:
that S should be able to state are of the form "for all N, f iterated N times on M does not have the k-th bit zero" (The equivalent condition in Godel is that S can state an arbitrary first-order theorem of Peano
Arithmetic).
720:
For every number n and every formula F(y), where y is a free variable, we define q(n,G(F)), a relation between two numbers n and G(F), such that it corresponds to the statement "n is not the Gödel number of a proof of
456:
Paras. 5 and 6. Although it is possible to replace the deduction rules with partial functions, this just adds complexity to the situation. The deduction rules are more naturally viewed as relations of some sort than
452:
Para. 1: "First, every mathematical statement is written in a fully formal manner," This isn't quite right; arithmetic has a particular formal language and the proof is about particular well formed formulas of that
1143:
2- A precise verification of the equivalence between your statement and that of Gödel requires some time. The pedagogical simplification is only effective once we are really convinced it is the same theorem.
746:
q(n,G(F)) (but not both) is provable. (The preceding statement requires a lengthy proof that relies on the properties of Godel numbering, and of proofs in the formal system. This lengthy proof is omitted
823:
How PF contributes to the proof in the part "Self-referential formula"? I only see it appears in the 3rd paragraph of the part "Self-referential formula" once and it seems that no proof is built on PF.
690:
F(G(F)), and \lnot q(n,G(F)) is provable if the finite list of formulas encoded by n is a proof of F(G(F)). Given any numbers n and G(F), either q(n,G(F)) or \lnotq(n,G(F)) (but not both) is provable
861:
PF(n, G(P)), but not both (assuming the consistency of the formal system), is provable. PF(n, G(P)) is provable if and only if n is the Godel number of (encodes) a proof of formula P. So, if
841:
Consider a formula (in our formal system of arithmetic) P, with Godel number G(P). Let n be a natural number. There exists a formula PF(n, G(P)) such that either this formula, or its negation
140:
641:
Using the word "hypothesis" in this context seems unconventional. I am unsure what it refers to. Isn't the purpose of the section to define the formal system, and the formal theory?
1059:
does not halt, the previous argument shows that S is inconsistent. So if S proves itself consistent, and if the previous argument can be formalized in S, then S also proves that
757:
2)There is no contradiction. Consider an example. Let P(x) be "400+x=3020", where x is a free variable. Let G(P)=21300, the Godel number of P(x). P(G(P)) is "400+21300=3020".
785:
383:
One may now define a set of numbers, which we will denote P, which consists of all numbers in AX (representing axioms) and all numbers which can be derived from them by
658:
When I edited the article earlier, I tried to find a compromise by adding back some of the deleted material by hand without completely undoing everything you had done.
949:
929:
906:
879:
859:
744:
1235:
130:
1028:
halts. By assumption, S eventually proves all theorems about the finite time behavior of computer programs, so S would also eventually prove that
397:
314:
Since there is a finite number of statements preceding P_i, a finite number of axiom schemas, and a finite number of deduction rules, there is an
106:
1123:
1230:
448:
The list above was all formatting and style issues. Here are some content issues. They aren't really errors so much as terminology issues.
401:
1154:
1216:
1198:
1162:
968:
959:
828:
800:
709:
668:
645:
628:
607:
582:
569:
487:
478:
438:
428:
409:
366:
289:
260:
224:
97:
58:
387:. The set P represents the set of provable statements. That is, the members of P are the Gödel numbers of the provable statements.
911:
Let n be a number. As just seen, PF(n, 619483) is provable if and only if n encodes a proof of "400+21300=3020". q(n, 21300) =
597:. I will keep working on other sections. My goal is to smooth out some of the rough edges and make the article more WP-like.
256:
You're absolutely correct, I hope to get some time to do all that soon... (just saw that now). a little help will be great.
33:
982:
The theorems talk about a formal system S, which is sufficiently strong. The precise assumptions on S are as follows:
497:
I offered to provide the coding used by
Douglas Hofstadter in his monumental work "Godel, Escher, Bach". Here it is.
405:
1158:
187:
285:
694:
Why "if n = G( proof of F(G(F)) ), then q(n,G(F)) is not provable", is it related to the property of PF?
664:
624:
603:
474:
424:
220:
39:
83:
681:
Hi all, this wiki entry is a great work~!I understand most of the points but not all, please help me.
1150:
21:
1212:
1194:
659:
619:
598:
469:
419:
215:
195:
999:: There are true theorems about the asymptotic behavior of computer programs that S cannot prove.
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
465:
89:
318:
procedure to decide whether each P_i is either an axiom or provable from P_1, P_2, ..., P_{i-1}.
73:
52:
1119:
1082:
1008:
566:
194:
Please help fix the broken anchors. You can remove this template after fixing the problems. |
770:
578:
20:35, 12 April 2007 (UTC) OK, I just saw your answer on this elsewhere. I'll do the changes
276:
P(G(P))... so maybe we need a mechanism to exclude some "proofs" that are not "interesting"?
174:
934:
914:
891:
864:
844:
729:
394:
What inputs are applied to the functions? The leading comments suggest the numbers in AX.
281:
951:
PF(n, 619483) is provable if and only if n does not encode a proof of "400+21300=3020".--
274:
Any statement can be proven from itself or from any false statement. Think P(G(P)) -: -->
243:
Use wiki formatting for math expressions, use display style for some formulas and numbers
233:
break it into sections (Godel numbering, derivation of the Bew(x) predicate, conclusion),
1085:
into a variable R, then deduce all consequences of S looking for either the theorem 1.
1208:
1204:
1190:
952:
793:
642:
579:
575:
484:
435:
359:
257:
1224:
635:
336:
However, for greater ease of understanding, introducing the deduction rules into the
266:
symbols. See below for two questions that should be easy to answer from the article.
483:
Well, it seems that you have better qualifications than me to make these changes...
349:(2) (S0=0, T) is not a proof of T, since "S0=0" is not an axiom of Peano arithmetic.
1115:
468:
finishes. The more I read this sketch the more I like it, modulo the terminology.
379:
Good summary and a very clear explanation for the most part, but I got lost here:
1070:: S is incomplete, meaning there is a statement that it cannot prove or disprove.
327:
Thus, a proof need not explicitly state the deduction rule invoked at each step.
102:
965:
825:
706:
79:
1011:
into a variable R, then deduce all consequences of S looking for the theorem
464:
I will be glad to make these changes myself, once the current discussion at
434:
Thanks. I've tried to clarify this point in the article, is it clearer now?
618:
edit both of this article and the Godel number article later this evening.
340:, and encoding them as numbers, is also acceptable, although not necessary.
993:
3. S is consistent, meaning it never proves a statement and its negation.
358:(3) (T,T) is not a proof of T, if T is not an axiom of Peano arithmetic.--
752:
The answer to your question should be contained in the facts just stated.
182:
This article links to one or more target anchors that no longer exist.
246:
Add additional references to introductory books that explain the proof
762:"P(G(P)) is not provable" says that "400+21300=3020" is not provable.
685:
1) In the 3rd paragraph of "Self-referential formula" 3rd paragraph,
838:
You're welcome. PF(x,y) is a building block of q(x,y), as follows.
271:
Don't we need an extra symbol for each "deduction rule" relation?
156:
15:
715:
1) We defined (in the first paragraph) q(n, G(F)) as follows:
565:
Please correct the above if there are mistakes or omissions.
638:
should be referenced and quoted in the "Hypothesis" section.
385:
applying the functions F1, F2,F3... a finite number of times
235:
and add wikilinks to help integrate it into the encyclopedia
186:] The anchor (#First-order theory of arithmetic) has been
1207:
an example if anyone else encounters the same difficulty.
881:
PF(n, G(P)) is provable, n does not encode a proof of P.
726:
In our formal system of arithmetic, either q(n,G(F)) or
812:
Thanks a lot
Palaeovia~! But I still have a questions :
655:
object. Linking to formal systems would be a good idea.
937:
917:
894:
867:
847:
773:
732:
101:, a collaborative effort to improve the coverage of
1140:the most important mathematicians of this century.
943:
923:
900:
873:
853:
779:
738:
214:these as they are completed and add more items.
1136:I disagree with this post for several reasons
1203:No, it's OK. I sorted that out. I will write
8:
1187:deduction symbols are also incorporated).
1148:
1097:prints "Hello" and halts . If it finds 2,
47:
936:
916:
893:
866:
846:
772:
731:
537:163 ' prime (used to make more variables)
460:Para 7. This terminology is nonstandard.
239:Give an outline of the proof at the top
49:
19:
1048:: S cannot prove its own consistency.
1041:does not halt and S does not prove it.
1003:Proof: construct the computer program
7:
1101:halts without printing out anything.
1015:. If it finds this theorem it halts.
95:This article is within the scope of
1063:does not halt, which is impossible.
38:It is of interest to the following
1112:ROSSER does not print anything out
1032:halts, so S would be inconsistent.
938:
918:
895:
868:
848:
774:
733:
14:
1236:Low-priority mathematics articles
115:Knowledge:WikiProject Mathematics
160:
118:Template:WikiProject Mathematics
82:
72:
51:
20:
1106:Now S cannot prove either that
135:This article has been rated as
1:
1147:formulation is preferable.
1087:R does not print anything out
574:Is there no copyright issue?
513:236 . multiplication operator
367:16:17, 30 December 2009 (UTC)
290:15:06, 30 December 2009 (UTC)
109:and see a list of open tasks.
1231:C-Class mathematics articles
1217:19:45, 3 February 2010 (UTC)
1199:21:37, 2 February 2010 (UTC)
1163:11:11, 26 October 2019 (UTC)
1124:01:01, 10 January 2008 (UTC)
964:Thx for the explaination~!--
792:Does this clarify matters?--
225:14:28, 27 January 2007 (UTC)
1108:ROSSER prints something out
787:n, q(n,21300)" is provable.
1252:
669:01:16, 27 April 2007 (UTC)
646:00:53, 27 April 2007 (UTC)
629:22:34, 26 April 2007 (UTC)
608:19:39, 18 April 2007 (UTC)
583:20:38, 12 April 2007 (UTC)
488:20:36, 12 April 2007 (UTC)
960:11:17, 29 June 2007 (UTC)
829:09:19, 29 June 2007 (UTC)
801:00:21, 29 June 2007 (UTC)
710:17:02, 28 June 2007 (UTC)
570:18:03, 9 April 2007 (UTC)
479:20:12, 6 April 2007 (UTC)
439:20:06, 5 April 2007 (UTC)
429:21:47, 4 April 2007 (UTC)
410:21:06, 4 April 2007 (UTC)
261:20:08, 5 April 2007 (UTC)
205:Good start and to do list
134:
67:
46:
974:Proof Of Godel's Theorem
969:00:52, 2 July 2007 (UTC)
780:{\displaystyle \forall }
510:112 + addition operator:
504:123 S successor function
493:GEB coding for reference
275:P(G(P)) or S0 = 0 -: -->
141:project's priority scale
973:
507:111 = equality relation
98:WikiProject Mathematics
1091:R prints something out
945:
944:{\displaystyle \lnot }
925:
924:{\displaystyle \lnot }
902:
901:{\displaystyle \lnot }
875:
874:{\displaystyle \lnot }
855:
854:{\displaystyle \lnot }
781:
740:
739:{\displaystyle \lnot }
392:
279:
254:
231:"wikify" the article:
188:deleted by other users
28:This article is rated
946:
926:
903:
876:
856:
782:
741:
400:comment was added by
381:
268:
228:
1077:: construct program
935:
915:
892:
888:Define q(x,y) to be
865:
845:
771:
730:
121:mathematics articles
1055:: If S proves that
534:262 a variable name
375:Unclear on one part
1083:print its own code
1009:print its own code
941:
921:
898:
871:
851:
777:
736:
552:333 there exists
90:Mathematics portal
34:content assessment
1165:
1153:comment added by
1110:nor the negation
1093:. If it finds 1,
1020:If S proves that
885:f(21300)=619483.
667:
627:
606:
561:611 . punctuation
558:636 : punctuation
549:223 ~ logical not
540:161 ^ logical and
477:
427:
413:
223:
202:
201:
177:in most browsers.
155:
154:
151:
150:
147:
146:
1243:
1178:Missing symbols?
957:
950:
948:
947:
942:
931:PF(n, f(21300))=
930:
928:
927:
922:
907:
905:
904:
899:
880:
878:
877:
872:
860:
858:
857:
852:
798:
786:
784:
783:
778:
745:
743:
742:
737:
663:
623:
602:
543:616 v logical or
473:
423:
395:
389:(Emphasis added)
364:
219:
196:Reporting errors
164:
163:
157:
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
1251:
1250:
1246:
1245:
1244:
1242:
1241:
1240:
1221:
1220:
1180:
1024:does not halt,
1013:R does not halt
976:
953:
933:
932:
913:
912:
890:
889:
863:
862:
843:
842:
794:
769:
768:
728:
727:
679:
634:Great! I think
615:
590:
495:
446:
402:207.171.180.101
396:—The preceding
377:
360:
207:
198:
180:
179:
178:
161:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
1249:
1247:
1239:
1238:
1233:
1223:
1222:
1179:
1176:
1175:
1174:
1173:
1172:
1171:
1170:
1169:
1168:
1167:
1166:
1155:92.129.159.234
1144:
1141:
1127:
1126:
1103:
1102:
1065:
1064:
1043:
1042:
1034:
1033:
1017:
1016:
975:
972:
940:
920:
897:
870:
850:
836:
835:
834:
833:
832:
831:
816:
815:
814:
813:
806:
804:
803:
789:
788:
776:
764:
763:
759:
758:
754:
753:
749:
748:
735:
723:
722:
717:
716:
697:
684:
678:
677:Some questions
675:
674:
673:
672:
671:
656:
649:
648:
639:
614:
611:
589:
586:
563:
562:
559:
556:
553:
550:
547:
546:633 contains
544:
541:
538:
535:
532:
529:
526:
523:
520:
517:
514:
511:
508:
505:
502:
494:
491:
462:
461:
458:
454:
445:
444:Content issues
442:
432:
431:
376:
373:
372:
371:
370:
369:
353:
352:
351:
350:
344:
343:
342:
341:
331:
330:
329:
328:
322:
321:
320:
319:
309:
308:
307:
306:
294:
278:
277:
272:
253:
252:
250:Add categories
247:
244:
241:
236:
206:
203:
200:
199:
193:
192:
191:
175:case-sensitive
169:
168:
167:
165:
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:
1248:
1237:
1234:
1232:
1229:
1228:
1226:
1219:
1218:
1214:
1210:
1206:
1201:
1200:
1196:
1192:
1188:
1184:
1177:
1164:
1160:
1156:
1152:
1145:
1142:
1138:
1137:
1135:
1134:
1133:
1132:
1131:
1130:
1129:
1128:
1125:
1121:
1117:
1113:
1109:
1105:
1104:
1100:
1096:
1092:
1088:
1084:
1080:
1076:
1073:
1072:
1071:
1069:
1062:
1058:
1054:
1051:
1050:
1049:
1047:
1040:
1036:
1035:
1031:
1027:
1023:
1019:
1018:
1014:
1010:
1006:
1002:
1001:
1000:
998:
994:
991:
987:
983:
980:
971:
970:
967:
962:
961:
958:
956:
909:
908:PF(x,f(y)).
886:
882:
839:
830:
827:
822:
821:
820:
819:
818:
817:
811:
810:
809:
808:
807:
802:
799:
797:
791:
790:
766:
765:
761:
760:
756:
755:
751:
750:
725:
724:
719:
718:
714:
713:
712:
711:
708:
703:
700:
695:
692:
691:
686:
682:
676:
670:
666:
661:
657:
653:
652:
651:
650:
647:
644:
640:
637:
636:Formal system
633:
632:
631:
630:
626:
621:
612:
610:
609:
605:
600:
596:
587:
585:
584:
581:
577:
572:
571:
568:
560:
557:
555:626 for all
554:
551:
548:
545:
542:
539:
536:
533:
530:
527:
524:
521:
518:
515:
512:
509:
506:
503:
500:
499:
498:
492:
490:
489:
486:
481:
480:
476:
471:
467:
459:
455:
451:
450:
449:
443:
441:
440:
437:
430:
426:
421:
416:
415:
414:
411:
407:
403:
399:
391:
390:
386:
380:
374:
368:
365:
363:
357:
356:
355:
354:
348:
347:
346:
345:
339:
335:
334:
333:
332:
326:
325:
324:
323:
317:
313:
312:
311:
310:
303:
299:
298:
297:
296:
295:
292:
291:
287:
283:
273:
270:
269:
267:
263:
262:
259:
251:
248:
245:
242:
240:
237:
234:
230:
229:
227:
226:
222:
217:
213:
204:
197:
189:
185:
184:
183:
176:
172:
166:
159:
158:
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:
1202:
1189:
1185:
1181:
1149:— Preceding
1111:
1107:
1098:
1094:
1090:
1086:
1078:
1074:
1067:
1066:
1060:
1056:
1052:
1045:
1044:
1038:
1029:
1025:
1021:
1012:
1004:
996:
995:
992:
988:
984:
981:
977:
963:
954:
910:
887:
883:
840:
837:
805:
795:
704:
702:Thz a lot~!
701:
696:
693:
688:
687:
683:
680:
616:
594:
591:
573:
567:Geometry guy
564:
496:
482:
463:
447:
433:
393:
388:
384:
382:
378:
361:
337:
315:
301:
293:
280:
264:
255:
249:
238:
232:
211:
208:
181:
173:Anchors are
170:
137:Low-priority
136:
96:
62:Low‑priority
40:WikiProjects
112:Mathematics
103:mathematics
59:Mathematics
1225:Categories
501:666 0 zero
457:functions.
282:Illegal604
212:strike out
1209:Dan Gluck
1191:Dan Gluck
1068:Theorem 2
1046:Corollary
997:Theorem 1
955:Palaeovia
796:Palaeovia
721:F(G(F))".
643:Palaeovia
613:2007-4-26
588:2007-4-18
580:Dan Gluck
576:Dan Gluck
525:213 : -->
485:Dan Gluck
453:language.
436:Dan Gluck
362:Palaeovia
316:effective
258:Dan Gluck
1151:unsigned
660:CMummert
620:CMummert
599:CMummert
522:212 <
470:CMummert
420:CMummert
398:unsigned
216:CMummert
1116:Likebox
190:before.
139:on the
30:C-class
1099:ROSSER
1095:ROSSER
1089:or 2.
1079:ROSSER
1061:DEDUCE
1057:DEDUCE
1039:DEDUCE
1030:DEDUCE
1026:DEDUCE
1022:DEDUCE
1005:DEDUCE
747:here.)
466:WT:WPM
300:(1) A
36:scale.
1075:Proof
1053:Proof
966:Hokit
826:Hokit
707:Hokit
531:313 ]
528:312 [
519:323 )
516:362 (
338:proof
305:D_5.)
302:proof
1213:talk
1205:here
1195:talk
1159:talk
1120:talk
665:talk
625:talk
604:talk
475:talk
425:talk
406:talk
286:talk
221:talk
171:Tip:
1081:to
1037:So
1007:to
131:Low
1227::
1215:)
1197:)
1161:)
1122:)
939:¬
919:¬
896:¬
869:¬
849:¬
824:--
775:∀
734:¬
705:--
662:·
622:·
601:·
472:·
422:·
408:)
288:)
218:·
1211:(
1193:(
1157:(
1118:(
1114:.
595:x
412:.
404:(
284:(
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
