6027:
configuration-like things (of Turing-machines), and specifically if we want to encode the significant part of the tape of a running Turing machine, then we have to represent sequences together with their length. We can mimic dynamically stretching sequences by representing sequence concatenation (or at least, augmenting a sequence with one more element) with a totally recursive function.
6810:
22:
167:
Any such representation of sequences should contain all the information as in the original sequence—most importantly, each individual member must be retrievable. However, the length does not have to match directly; even if we want to handle sequences of different length, we can store length data as a
6026:
To illustrate both cases: if we form the Gödel numbering of a Turing machine, then the each row in the matrix of the “program” can be represented with tuples, sequences of fixed length (thus, without storing the length), because the number of the columns is fixed. But if we want to reason about
6586:
5486:
plays a role here of a more general notion (“special function”). The importance of this notion is that it enables us to split off the (sub)class of (total) recursive functions from the (super)class of partial recursive functions. In brief, the specification says that a function
2589:
1153:
5626:
2724:
3937:
2442:
2224:
1426:
function, we shall use several lemmas. These have their own assumptions. Now we try to find out these assumptions, calibrating and tuning their strength carefully: they should not be said in an either superfluously sharp, or unsatisfactorily weak form.
986:
5773:
4997:
1365:
4589:
6255:
5481:
5254:
3130:
2089:
1553:
5990:
93:
is surely possible, the emphasis is on the effectiveness of the functions manipulating such representations of sequences: the operations on sequences (accessing individual members, concatenation) can be "implemented" using
6805:{\displaystyle f\left(a_{0},\dots ,a_{n-1},s\right)={\begin{cases}0&\mathrm {if} \;\forall i<n\;\left(\beta (s,i)=a_{i}\right)\\1&\mathrm {if} \;\exists i<n\;\left(\beta (s,i)\neq a_{i}\right)\end{cases}}}
3345:
4181:
5098:
3240:
2458:
5335:
4873:
4784:
4660:
1616:
1918:
6580:
711:
652:
4266:
4225:
3611:
477:
240:
6074:
5847:
1672:
4470:
4096:
3709:
3187:
1025:
3806:
4004:
3435:
2783:
1978:
1798:
5497:
2604:
6311:
3822:
2931:
2324:
2109:
3049:
873:
825:
775:
2313:
1250:
5645:
4377:
1477:
175:
We expect that there is an effective way for this information retrieval process in form of an appropriate total recursive function. We want to find a totally recursive function
2986:
2832:
529:
4298:
1840:
286:
6008:
If we use the above scheme for encoding sequences only in contexts where the length of the sequences is fixed, then no problem arises. In other words, we can use them in an
4707:
2256:
1193:
159:
into natural numbers and thereby prove that the expressive power of recursive function theory is no less than that of the former machine-like formalizations of algorithms.
5259:
is met. Although proving this was most important for establishing an encoding scheme for sequences, we have to fill in some gaps yet. These are related notions similar to
1739:
334:
4890:
3511:
1258:
50:
3383:
3272:
4025:
3749:
3543:
3464:
5801:
5371:
5144:
5020:
1710:
1424:
1009:
865:
407:
383:
339:
There are effective functions which can retrieve each member of the original sequence from a Gödel number of the sequence. Moreover, we can define some of them in a
4404:
4379:
are pairwise comprime as proven in the previous sections, so we can refer to the solution ensured by the
Chinese remainder theorem. Thus, from now on we can regard
4328:
3645:
2867:
2005:
1396:
4486:
575:
6080:
5379:
5152:
3066:
2025:
1489:
545:
Our specific solution will depend on a pairing function—there are several ways to implement the pairing function, so one method must be selected. Now, we can
6316:
to the system of simultaneous congruences (provided that the surplus member index is chosen to be 0). Also, the assumptions have to be modified accordingly.
5853:
2452:
We know what “coprime” relation means (in a lucky way, its negation can be formulated in a concise form); thus, let us substitute in the appropriate way:
43:
3292:
4107:
1692:
The second assumption does not concern the
Chinese remainder theorem in any way. It will have importance in proving that the specification for
7025:
6990:
6968:
6866:
5353:, and the totality of the resulting function is ensured by everything we have proven till now (i.e. the correctness of the definition of
5025:
2584:{\displaystyle \exists i<n,j<n\;\left(i\neq j\land \exists p\in \mathrm {Prime} \;\left(p\mid m_{i}\land p\mid m_{j}\right)\right)}
3192:
5278:
6942:
68:
109:” in arithmetic-based formalizations of some fundamental notions of mathematics. It is a specific case of the more general idea of
89:
provides an effective way to represent each finite sequence of natural numbers as a single natural number. While a set theoretical
4804:
4715:
6899:
6443:
4602:
1559:
1851:
151:
with the sequences), we can use it to encode whole “architectures” of sophisticated “machines”. For example, we can encode
7044:
6536:
658:
599:
4230:
4189:
3555:
427:
190:
143:
Besides using Gödel numbering to encode unique sequences of symbols into unique natural numbers (i.e. place numbers into
6036:
5809:
5267:(although on uniqueness, “at most one” should be meant here, and the conjunction of both is delayed as a final result).
1627:
1148:{\displaystyle \beta \left(\pi \left(x_{0},m\right),i\right)=\mathrm {rem} \left(x_{0},\left(i+1\right)\cdot m+1\right)}
554:
410:
99:
37:
6499:
4412:
4033:
3653:
3142:
356:
5621:{\displaystyle f\left(a_{0},\dots ,a_{n-1},s\right)=0\leftrightarrow \forall i<n\;\left(\beta (s,i)=a_{i}\right)}
6483:
5260:
3768:
2719:{\displaystyle \exists i<n,j<n,p\in \mathrm {Prime} \;\left(i\neq j\land p\mid m_{i}\land p\mid m_{j}\right)}
3953:
3396:
2736:
1931:
1747:
6015:
But sometimes we need dynamically stretching sequences, or we need to deal with sequences whose length cannot be
5264:
3932:{\displaystyle \forall i<n,j<n\;\left(i\neq j\rightarrow \mathrm {coprime} \left(m_{i},m_{j}\right)\right)}
2437:{\displaystyle \exists i<n,j<n\;\left(i\neq j\land \lnot \mathrm {coprime} \left(m_{i},m_{j}\right)\right)}
2219:{\displaystyle \forall i<n,j<n\;\left(i\neq j\rightarrow \mathrm {coprime} \left(m_{i},m_{j}\right)\right)}
844:
385:(using simple number-theoretical functions, all of which can be defined in a total recursive way) fulfilling the
362:
148:
4227:". To achieve a more ergonomic treatment, from now on all statements should be read as being in the scope of an
6479:
1159:
586:
95:
6267:
2872:
981:{\displaystyle \beta (s,i)=\mathrm {rem} \left(K\left(s\right),\left(i+1\right)\cdot L\left(s\right)+1\right)}
3136:
The assumption was chosen carefully to be as weak as possible, but strong enough to enable us to use it now.
7013:
6854:
6463:
5768:{\displaystyle \forall a_{0},\dots ,a_{n-1}\;\exists s\;\left(f\left(a_{0},\dots ,a_{n-1},s\right)=0\right)}
5337:? The specification declares only an existential quantification, not yet a functional connection. We want a
3139:
The assumed negation of the original statement contains an appropriate existential statement using indices
3010:
781:
731:
5108:
4795:
3762:
3719:
3283:
2934:
2261:
1198:
6016:
4333:
1433:
2947:
344:
114:
2791:
486:
4271:
1807:
253:
122:
6652:
4992:{\displaystyle \beta \left(\pi \left(x_{0},m\right),i\right)=\mathrm {rem} \left(x_{0},m_{i}\right)}
4672:
2232:
1360:{\displaystyle \beta \left(\pi \left(x_{0},m\right),i\right)=\mathrm {rem} \left(x_{0},m_{i}\right)}
1169:
32:
5631:
is a special function; that is, for each fixed combination of all-but-last arguments, the function
5104:
4791:
3715:
3386:
3001:
2938:
1715:
291:
5636:
5338:
4477:
3483:
2595:
1682:
340:
144:
90:
138:
110:
3356:
3245:
7021:
6986:
6964:
6938:
6862:
1012:
4584:{\displaystyle \mathrm {rem} \left(x_{0},m_{i}\right)=\mathrm {rem} \left(a_{i},m_{i}\right)}
4010:
3728:
3522:
3443:
6978:
6952:
6911:
6877:
6250:{\displaystyle \left\langle a_{0},\dots ,a_{n-1},a_{n}\right\rangle \longmapsto \mu a.\left}
6020:
5786:
5356:
5129:
5005:
1695:
1677:
It is needed to meet an assumption of the
Chinese remainder theorem (that of being pairwise
1409:
1016:
994:
850:
540:
392:
368:
169:
152:
126:
5783:
Thus, let us choose the minimal possible number that fits well in the specification of the
4382:
4306:
3623:
2845:
1983:
1374:
6447:
5476:{\displaystyle \forall a_{0},\dots ,a_{n-1}\;\exists s\;\forall i<n\;\beta (s,i)=a_{i}}
5249:{\displaystyle \forall a_{0},\dots ,a_{n-1}\;\exists s\;\forall i<n\;\beta (s,i)=a_{i}}
3125:{\displaystyle \forall i\in {\overline {n}}\setminus \left\{0\right\}\left(i\mid m\right)}
2084:{\displaystyle \forall i\in {\overline {n}}\setminus \left\{0\right\}\left(i\mid m\right)}
1548:{\displaystyle \forall i\in {\overline {n}}\setminus \left\{0\right\}\left(i\mid m\right)}
560:
3816:
By reaching contradiction with its negation, we have just proven the original statement:
6957:
1681:). In the literature, sometimes this requirement is replaced with a stronger one, e.g.
550:
409:
function using the
Chinese remainder theorem in his article written in 1931. This is a
156:
6921:
6440:
5985:{\displaystyle \left\langle a_{0},\dots ,a_{n-1}\right\rangle \longmapsto \mu a.\left}
4330:
for the system of simultaneous congruences. At least one solution must exist, because
7038:
6931:
5341:
and algorithmic connection: a (total) recursive function that performs the encoding.
2997:
590:
386:
6261:
The corresponding modification of the proof is straightforward, by adding a surplus
42:
the article should be edited for tone, length, and to meet the other conventions of
6507:
6503:
6937:. Graduate Texts in Mathematics. New York • Heidelberg • Berlin: Springer-Verlag.
6495:
6019:
in a static way. In other words, we may encode sequences in an analogous way to
5350:
5275:
Our ultimate question is: what number should stand for the encoding of sequence
830:
It can be proven that this function can be implemented as a recursive function.
546:
82:
4662:”, and remember that we are now in the scope of an implicit quantification for
3617:
2839:
2318:
The proof is by contradiction; assume the negation of the original statement:
1163:
6916:
3437:. Thus (as equality axioms postulate identity to be a congruence relation )
3340:{\displaystyle \left(A\land \left(A\rightarrow B\right)\right)\rightarrow B}
1686:
722:
118:
106:
6881:
6838:
6400:
6353:
4176:{\displaystyle \forall i<n\;\left(x\equiv a_{i}{\pmod {m_{i}}}\right)}
1980:
automatically satisfies the second assumption (if we define the notation
2011:
Proof that (coprimality) assumption for
Chinese remainder theorem is met
6888:(postscript + gzip) (in Hungarian). Budapest: Eötvös Loránd University.
6009:
3390:
2730:
2092:
1678:
2091:. What we want to prove is that we can produce a sequence of pairwise
129:
by encoding a sequence of natural numbers in a single natural number.
168:
surplus member, or as the other member of an ordered pair by using a
5996:
It can be proven (using the notions of the previous section ) that
5345:
Totality, because minimalization is restricted to special functions
5093:{\displaystyle \beta \left(\pi \left(x_{0},m\right),i\right)=a_{i}}
1689:
function, but the stronger premise is not required for this proof.
5779:
The Gödel numbering function g can be chosen to be total recursive
3278:
Using an (object) theorem of the propositional calculus as a lemma
6891:
3235:{\displaystyle i-j\in {\overline {n}}\setminus \left\{0\right\}}
5330:{\displaystyle \left\langle a_{0},\dots ,a_{n-1}\right\rangle }
5002:
is good for achieving what we declared in the specification of
2598:(but note allowing a constraint-like notation in quantifiers):
5349:
This gap can be filled in a straightforward way: we shall use
721:
We shall use another auxiliary function that will compute the
15:
1166:(as these notions are used in computer science): by defining
246:, called the Gödel number of the sequence, such that for all
4868:{\displaystyle \mathrm {rem} \left(x_{0},m_{i}\right)=a_{i}}
4779:{\displaystyle \mathrm {rem} \left(a_{i},m_{i}\right)=a_{i}}
4666:, so we don't repeat its quantification for each statement.
6798:
4655:{\displaystyle \forall i<n\;\left(a_{i}<m_{i}\right)}
1406:
For proving the correctness of the above definition of the
5373:
by meeting its specification). In fact, the specification
3808:. This establishes the contradiction we wanted to reach.
365:, we can constructively define such a recursive function
5126:
We have just proven the correctness of the definition of
2095:
numbers in a way that will turn out to correspond to the
1611:{\displaystyle \forall i<n\left(a_{i}<m_{i}\right)}
4186:
Many statements will be said below, all beginning with "
1913:{\displaystyle a_{i}=\mathrm {rem} ({\tilde {x}},m_{i})}
6494:
either proof theoretic (algebraic steps); or semantic (
117:
can be regarded as a formalization of the notion of an
6589:
6539:
6270:
6083:
6039:
5856:
5812:
5789:
5648:
5500:
5382:
5359:
5281:
5155:
5132:
5028:
5008:
4893:
4807:
4718:
4675:
4605:
4489:
4415:
4385:
4336:
4309:
4274:
4233:
4192:
4110:
4036:
4013:
3956:
3825:
3771:
3731:
3656:
3626:
3558:
3525:
3486:
3446:
3399:
3359:
3295:
3248:
3195:
3145:
3069:
3013:
2950:
2875:
2848:
2794:
2739:
2607:
2461:
2327:
2264:
2235:
2112:
2096:
2028:
1986:
1934:
1854:
1810:
1750:
1718:
1698:
1630:
1562:
1492:
1436:
1412:
1377:
1261:
1201:
1172:
1028:
997:
876:
853:
784:
734:
661:
602:
563:
489:
430:
395:
371:
294:
256:
193:
6575:{\displaystyle f:\mathbb {N} ^{n+1}\to \mathbb {N} }
6478:
see also related notions, e.g. “equals for equals” (
991:
will work, according to the specification we expect
706:{\displaystyle L\left(\pi \left(x,y\right)\right)=y}
647:{\displaystyle K\left(\pi \left(x,y\right)\right)=x}
553:
of the pairing function. We need only to know its “
483:, called the Gödel number of the sequence such that
4884:Our original goal was to prove that the definition
4261:{\displaystyle \forall i<n\;\left(\dots \right)}
4220:{\displaystyle \forall i<n\;\left(\dots \right)}
3757:However, in the negation of the original statement
3606:{\displaystyle p\mid m_{i}-\left(i+1\right)\cdot m}
3242:, thus the mentioned assumption can be applied, so
472:{\displaystyle \langle a_{0},\dots a_{n-1}\rangle }
235:{\displaystyle \langle a_{0},\dots a_{n-1}\rangle }
6956:
6930:
6804:
6574:
6345:
6343:
6305:
6249:
6069:{\displaystyle g:\mathbb {N} ^{*}\to \mathbb {N} }
6068:
5984:
5842:{\displaystyle g:\mathbb {N} ^{n}\to \mathbb {N} }
5841:
5795:
5767:
5620:
5475:
5365:
5329:
5271:Uniqueness of encoding, achieved by minimalization
5248:
5138:
5092:
5014:
4991:
4867:
4778:
4701:
4654:
4583:
4464:
4398:
4371:
4322:
4292:
4260:
4219:
4175:
4090:
4019:
3998:
3931:
3800:
3743:
3703:
3639:
3605:
3537:
3505:
3458:
3429:
3377:
3339:
3266:
3234:
3181:
3124:
3043:
2980:
2925:
2861:
2826:
2777:
2718:
2583:
2436:
2307:
2250:
2218:
2083:
1999:
1972:
1912:
1834:
1792:
1733:
1704:
1667:{\displaystyle 1\mid m\land \dots \land n-1\mid m}
1666:
1610:
1547:
1471:
1418:
1390:
1359:
1244:
1187:
1147:
1003:
980:
859:
819:
769:
705:
646:
569:
523:
471:
401:
377:
328:
280:
234:
6330:
6328:
6030:Length can be stored simply as a surplus member:
3714:Thus, summarizing the above three statements, by
1011:to satisfy. We can use a more concise form by an
4465:{\displaystyle x_{0}\equiv a_{i}{\pmod {m_{i}}}}
4091:{\displaystyle x\equiv a_{n-1}{\pmod {m_{n-1}}}}
3704:{\displaystyle m_{i}-\left(i+1\right)\cdot m=1}
3182:{\displaystyle i<n\land j<n\land i\neq j}
1741:solution of the simultaneous congruence system
6482:), and another related notion Leibniz's law /
3947:We build a system of simultaneous congruences
4595:Resorting to the second hand-tuned assumption
3801:{\displaystyle \exists p\in \mathrm {Prime} }
3616:should also hold. But after substituting the
3477:The negation of original statement contained
1158:Let us achieve even more readability by more
479:, there exists an appropriate natural number
242:, there exists an appropriate natural number
8:
3999:{\displaystyle x\equiv a_{0}{\pmod {m_{0}}}}
3430:{\displaystyle p\mid i-j\rightarrow p\mid m}
3056:Resorting to the first hand-tuned assumption
2778:{\displaystyle p\mid m_{i}\land p\mid m_{j}}
1973:{\displaystyle \forall i<n\;(a_{i}<m)}
1793:{\displaystyle x\equiv a_{i}{\pmod {m_{i}}}}
466:
431:
229:
194:
2016:
44:Knowledge (XXG):Manual of Style/Mathematics
7018:Logic for Mathematics and Computer Science
6859:Logic for Mathematics and Computer Science
6753:
6740:
6681:
6668:
6190:
5931:
5694:
5687:
5576:
5441:
5428:
5421:
5214:
5201:
5194:
4618:
4246:
4205:
4123:
3850:
2658:
2530:
2486:
2352:
2137:
1947:
6915:
6890:Each chapter is downloadable verbatim on
6784:
6732:
6712:
6660:
6647:
6621:
6602:
6588:
6568:
6567:
6552:
6548:
6547:
6538:
6474:
6472:
6293:
6280:
6269:
6231:
6163:
6131:
6112:
6093:
6082:
6062:
6061:
6052:
6048:
6047:
6038:
5966:
5885:
5866:
5855:
5835:
5834:
5825:
5821:
5820:
5811:
5788:
5731:
5712:
5675:
5656:
5647:
5607:
5532:
5513:
5499:
5467:
5409:
5390:
5381:
5358:
5310:
5291:
5280:
5240:
5182:
5163:
5154:
5131:
5084:
5049:
5027:
5007:
4978:
4965:
4945:
4914:
4892:
4859:
4841:
4828:
4808:
4806:
4770:
4752:
4739:
4719:
4717:
4693:
4680:
4674:
4641:
4628:
4604:
4570:
4557:
4537:
4523:
4510:
4490:
4488:
4452:
4439:
4433:
4420:
4414:
4390:
4384:
4357:
4341:
4335:
4314:
4308:
4273:
4232:
4191:
4158:
4145:
4139:
4109:
4072:
4059:
4047:
4035:
4012:
3986:
3973:
3967:
3955:
3913:
3900:
3868:
3824:
3781:
3770:
3730:
3661:
3655:
3631:
3625:
3569:
3557:
3524:
3497:
3485:
3445:
3398:
3358:
3294:
3247:
3208:
3194:
3144:
3079:
3068:
3012:
2949:
2893:
2880:
2874:
2853:
2847:
2818:
2805:
2793:
2769:
2750:
2738:
2705:
2686:
2641:
2606:
2565:
2546:
2513:
2460:
2418:
2405:
2373:
2326:
2269:
2263:
2234:
2200:
2187:
2155:
2111:
2038:
2027:
1991:
1985:
1955:
1933:
1901:
1883:
1882:
1868:
1859:
1853:
1809:
1780:
1767:
1761:
1749:
1720:
1719:
1717:
1697:
1629:
1597:
1584:
1561:
1502:
1491:
1457:
1441:
1435:
1411:
1382:
1376:
1346:
1333:
1313:
1282:
1260:
1206:
1200:
1171:
1100:
1080:
1049:
1027:
996:
898:
875:
852:
785:
783:
735:
733:
660:
601:
562:
515:
488:
454:
438:
429:
394:
370:
320:
293:
255:
217:
201:
192:
69:Learn how and when to remove this message
6306:{\displaystyle x\equiv n{\pmod {m_{0}}}}
5111:, looking at the above three equations.
3282:We can prove by several means known in
2926:{\displaystyle m_{i}-m_{j}=(i-j)\cdot m}
585:denote the pairing function and its two
105:It is usually used to build sequential “
6324:
6012:way as arrays are used in programming.
4101:We can write it in a more concise way:
3218:
3089:
2048:
1712:is met eventually. It ensures that an
1512:
3943:The system of simultaneous congruences
1479:be a sequence of natural numbers. Let
6392:
6390:
6388:
6386:
3060:Now we must resort to our assumption
3044:{\displaystyle p\mid i-j\lor p\mid m}
820:{\displaystyle \mathrm {rem} (7,2)=1}
770:{\displaystyle \mathrm {rem} (5,3)=2}
7:
6900:"Why Functional Programming Matters"
6837:: 101 (=Thm 10.7, Conseq 10.8), see
2308:{\displaystyle m_{i}=(i+1)\cdot m+1}
1245:{\displaystyle m_{i}=(i+1)\cdot m+1}
589:functions, respectively, satisfying
424:-length sequence of natural numbers
187:-length sequence of natural numbers
6985:(in Hungarian). Budapest: Typotex.
6288:
4447:
4372:{\displaystyle m_{0},\dots m_{n-1}}
4153:
4067:
3981:
2937:axioms postulate identity to be a
1775:
1472:{\displaystyle a_{0},\dots a_{n-1}}
834:Using the Chinese remainder theorem
343:way, so we can go well beyond mere
7014:"Supplementary Text, Arithmetic I"
6855:"Supplementary Text, Arithmetic I"
6741:
6736:
6733:
6669:
6664:
6661:
6178:
5919:
5688:
5649:
5564:
5429:
5422:
5383:
5202:
5195:
5156:
4952:
4949:
4946:
4815:
4812:
4809:
4726:
4723:
4720:
4606:
4544:
4541:
4538:
4497:
4494:
4491:
4275:
4234:
4193:
4111:
3887:
3884:
3881:
3878:
3875:
3872:
3869:
3826:
3794:
3791:
3788:
3785:
3782:
3772:
3070:
2981:{\displaystyle p\mid (i-j)\cdot m}
2654:
2651:
2648:
2645:
2642:
2608:
2526:
2523:
2520:
2517:
2514:
2504:
2462:
2392:
2389:
2386:
2383:
2380:
2377:
2374:
2370:
2328:
2236:
2174:
2171:
2168:
2165:
2162:
2159:
2156:
2113:
2029:
1935:
1875:
1872:
1869:
1563:
1493:
1320:
1317:
1314:
1173:
1087:
1084:
1081:
905:
902:
899:
792:
789:
786:
742:
739:
736:
14:
2827:{\displaystyle p\mid m_{i}-m_{j}}
1621:The first assumption is meant as
847:, we can prove that implementing
524:{\displaystyle \beta (a,i)=a_{i}}
4599:Recall the second assumption, “
2097:Implementation of the β function
839:Implementation of the β function
350:
20:
6959:Gödel's Incompleteness Theorems
6281:
4440:
4293:{\displaystyle \forall i<n(}
4146:
4060:
3974:
1835:{\displaystyle 0\leq i\leq n-1}
1768:
389:given above. Gödel defined the
281:{\displaystyle 0\leq i\leq n-1}
179:with the property that for all
6774:
6762:
6702:
6690:
6564:
6299:
6282:
6142:
6058:
5902:
5831:
5597:
5585:
5561:
5457:
5445:
5230:
5218:
5146:: its specification requiring
4702:{\displaystyle a_{i}<m_{i}}
4476:which means (by definition of
4458:
4441:
4287:
4164:
4147:
4084:
4061:
3992:
3975:
3865:
3415:
3331:
3315:
2969:
2957:
2914:
2902:
2290:
2278:
2251:{\displaystyle \forall i<n}
2152:
1967:
1948:
1907:
1888:
1879:
1786:
1769:
1725:
1227:
1215:
1188:{\displaystyle \forall i<n}
892:
880:
808:
796:
758:
746:
505:
493:
310:
298:
1:
6508:Veitch diagram / Karnaugh map
6415:: 56 (= Chpt IV, § 5, note 1)
5491:satisfying the specification
723:remainder for natural numbers
717:Remainder for natural numbers
100:primitive recursive functions
87:Gödel numbering for sequences
3213:
3084:
2043:
1734:{\displaystyle {\tilde {x}}}
1507:
411:primitive recursive function
329:{\displaystyle f(a,i)=a_{i}}
7012:Burris, Stanley N. (1998).
6983:Gödel nemteljességi tételei
6963:. Oxford University Press.
6853:Burris, Stanley N. (1998).
6834:
6825:: 53 (= Def 3.20, Lem 3.21)
6500:method of analytic tableaux
6436:
6396:
6349:
3812:End of reductio ad absurdum
3506:{\displaystyle p\mid m_{i}}
2869:-sequence notation, we get
361:By an ingenious use of the
121:, and can be regarded as a
40:. The specific problem is:
7061:
6998:
6822:
6519:
6484:identity of indiscernibles
6459:
6424:
6412:
6377:
6365:
6334:
3473:Reaching the contradiction
3004:property is used), we get
1924:A stronger assumption for
538:
354:
136:
36:to meet Knowledge (XXG)'s
6979:Smullyan, Raymond Merrill
6953:Smullyan, Raymond Merrill
3765:and restricted to primes
3378:{\displaystyle i-j\mid m}
3267:{\displaystyle i-j\mid m}
845:Chinese remainder theorem
363:Chinese remainder theorem
149:one-to-one correspondence
115:recursive function theory
96:total recursive functions
6929:Monk, J. Donald (1976).
6480:referential transparency
5122:Existence and uniqueness
5103:This can be seen now by
4303:Let us chose a solution
3763:existentially quantified
3516:and we have just proved
2729:Because of a theorem on
1015:(constituting a sort of
549:from the details of the
535:Using a pairing function
351:Gödel's β-function lemma
4020:{\displaystyle \vdots }
3744:{\displaystyle p\mid 1}
3538:{\displaystyle p\mid m}
3459:{\displaystyle p\mid m}
1398:notation in the proof.
6917:10.1093/comjnl/32.2.98
6806:
6576:
6462:: Supplementary Text,
6307:
6251:
6070:
6000:is (total) recursive.
5986:
5843:
5797:
5796:{\displaystyle \beta }
5769:
5639:in its last argument:
5622:
5477:
5367:
5366:{\displaystyle \beta }
5331:
5250:
5140:
5139:{\displaystyle \beta }
5094:
5016:
5015:{\displaystyle \beta }
4993:
4869:
4780:
4703:
4669:The second assumption
4656:
4585:
4466:
4400:
4373:
4324:
4294:
4268:quantification. Thus,
4262:
4221:
4177:
4092:
4021:
4000:
3933:
3802:
3745:
3705:
3641:
3607:
3539:
3507:
3460:
3431:
3379:
3341:
3284:propositional calculus
3268:
3236:
3183:
3126:
3045:
2982:
2927:
2863:
2828:
2785:allows us to also say
2779:
2720:
2585:
2438:
2309:
2252:
2220:
2085:
2017:Hand-tuned assumptions
2001:
1974:
1914:
1836:
1794:
1735:
1706:
1705:{\displaystyle \beta }
1668:
1612:
1549:
1473:
1420:
1419:{\displaystyle \beta }
1402:Hand-tuned assumptions
1392:
1361:
1246:
1189:
1149:
1005:
1004:{\displaystyle \beta }
982:
861:
860:{\displaystyle \beta }
821:
771:
707:
648:
571:
525:
473:
403:
402:{\displaystyle \beta }
379:
378:{\displaystyle \beta }
330:
282:
236:
6898:Hughes, John (1989).
6882:"Rekurzív függvények"
6807:
6577:
6308:
6252:
6071:
5987:
5844:
5798:
5770:
5623:
5478:
5368:
5332:
5251:
5141:
5095:
5017:
4994:
4870:
4781:
4704:
4657:
4586:
4467:
4401:
4399:{\displaystyle x_{0}}
4374:
4325:
4323:{\displaystyle x_{0}}
4295:
4263:
4222:
4178:
4093:
4022:
4001:
3934:
3803:
3746:
3706:
3642:
3640:{\displaystyle m_{i}}
3608:
3540:
3508:
3461:
3432:
3380:
3342:
3269:
3237:
3184:
3127:
3046:
2983:
2928:
2864:
2862:{\displaystyle m_{k}}
2829:
2780:
2721:
2586:
2439:
2310:
2253:
2221:
2086:
2002:
2000:{\displaystyle m_{i}}
1975:
1915:
1837:
1795:
1736:
1707:
1669:
1613:
1550:
1483:be chosen to satisfy
1474:
1421:
1393:
1391:{\displaystyle m_{i}}
1362:
1247:
1190:
1150:
1006:
983:
862:
822:
772:
708:
649:
572:
526:
474:
404:
380:
331:
283:
237:
7045:Computability theory
6924:on December 8, 2006.
6587:
6537:
6268:
6081:
6037:
5854:
5810:
5787:
5646:
5498:
5380:
5357:
5279:
5153:
5130:
5114:(The large scope of
5026:
5006:
4891:
4805:
4716:
4673:
4603:
4487:
4413:
4383:
4334:
4307:
4272:
4231:
4190:
4108:
4034:
4011:
3954:
3823:
3769:
3729:
3654:
3624:
3556:
3523:
3484:
3444:
3397:
3357:
3293:
3246:
3193:
3143:
3067:
3011:
2948:
2873:
2846:
2792:
2737:
2605:
2459:
2325:
2262:
2233:
2110:
2026:
1984:
1932:
1852:
1808:
1748:
1716:
1696:
1628:
1560:
1490:
1434:
1410:
1375:
1259:
1199:
1170:
1026:
995:
874:
851:
782:
732:
659:
600:
570:{\displaystyle \pi }
561:
487:
428:
393:
369:
292:
254:
191:
123:programming language
51:improve this article
3002:irreducible element
2939:congruence relation
2019:, we required that
345:proofs of existence
6933:Mathematical Logic
6886:Matematikai logika
6802:
6797:
6572:
6446:2006-12-08 at the
6303:
6247:
6066:
5982:
5839:
5793:
5765:
5618:
5473:
5363:
5327:
5246:
5136:
5090:
5012:
4989:
4865:
4776:
4699:
4652:
4581:
4478:modular arithmetic
4462:
4396:
4369:
4320:
4290:
4258:
4217:
4173:
4088:
4017:
3996:
3929:
3798:
3754:should also hold.
3741:
3701:
3637:
3603:
3535:
3503:
3456:
3427:
3375:
3337:
3264:
3232:
3179:
3122:
3041:
2978:
2923:
2859:
2824:
2775:
2716:
2596:prenex normal form
2581:
2434:
2305:
2248:
2216:
2081:
1997:
1970:
1910:
1832:
1790:
1731:
1702:
1664:
1608:
1545:
1469:
1416:
1388:
1371:We shall use this
1357:
1242:
1185:
1145:
1001:
978:
857:
817:
767:
703:
644:
567:
521:
469:
399:
375:
357:Gödel's β function
326:
278:
232:
145:mutually exclusive
7027:978-0-13-285974-5
7020:. Prentice Hall.
6992:978-963-9326-99-6
6970:978-0-19-504672-4
6876:Csirmaz, László;
6868:978-0-13-285974-5
6861:. Prentice Hall.
6522:: 45 (= Def 3.1.)
6427:: 58 (= Thm 3.46)
3216:
3087:
2838:Substituting the
2229:remembering that
2046:
1891:
1728:
1510:
1013:abuse of notation
163:Accessing members
153:Markov algorithms
98:, and in fact by
79:
78:
71:
38:quality standards
29:This article may
7052:
7031:
6996:
6974:
6962:
6948:
6936:
6925:
6920:. Archived from
6919:
6904:Computer Journal
6889:
6872:
6841:
6832:
6826:
6820:
6814:
6811:
6809:
6808:
6803:
6801:
6800:
6794:
6790:
6789:
6788:
6739:
6722:
6718:
6717:
6716:
6667:
6643:
6639:
6632:
6631:
6607:
6606:
6581:
6579:
6578:
6573:
6571:
6563:
6562:
6551:
6531:E.g. defined by
6529:
6523:
6517:
6511:
6492:
6486:
6476:
6467:
6457:
6451:
6434:
6428:
6422:
6416:
6410:
6404:
6394:
6381:
6375:
6369:
6363:
6357:
6347:
6338:
6332:
6312:
6310:
6309:
6304:
6302:
6298:
6297:
6256:
6254:
6253:
6248:
6246:
6242:
6241:
6237:
6236:
6235:
6223:
6219:
6168:
6167:
6141:
6137:
6136:
6135:
6123:
6122:
6098:
6097:
6075:
6073:
6072:
6067:
6065:
6057:
6056:
6051:
6023:in programming.
6004:Access of length
5991:
5989:
5988:
5983:
5981:
5977:
5976:
5972:
5971:
5970:
5958:
5954:
5901:
5897:
5896:
5895:
5871:
5870:
5848:
5846:
5845:
5840:
5838:
5830:
5829:
5824:
5802:
5800:
5799:
5794:
5774:
5772:
5771:
5766:
5764:
5760:
5753:
5749:
5742:
5741:
5717:
5716:
5686:
5685:
5661:
5660:
5627:
5625:
5624:
5619:
5617:
5613:
5612:
5611:
5554:
5550:
5543:
5542:
5518:
5517:
5482:
5480:
5479:
5474:
5472:
5471:
5420:
5419:
5395:
5394:
5372:
5370:
5369:
5364:
5336:
5334:
5333:
5328:
5326:
5322:
5321:
5320:
5296:
5295:
5255:
5253:
5252:
5247:
5245:
5244:
5193:
5192:
5168:
5167:
5145:
5143:
5142:
5137:
5099:
5097:
5096:
5091:
5089:
5088:
5076:
5072:
5065:
5061:
5054:
5053:
5021:
5019:
5018:
5013:
4998:
4996:
4995:
4990:
4988:
4984:
4983:
4982:
4970:
4969:
4955:
4941:
4937:
4930:
4926:
4919:
4918:
4874:
4872:
4871:
4866:
4864:
4863:
4851:
4847:
4846:
4845:
4833:
4832:
4818:
4785:
4783:
4782:
4777:
4775:
4774:
4762:
4758:
4757:
4756:
4744:
4743:
4729:
4708:
4706:
4705:
4700:
4698:
4697:
4685:
4684:
4661:
4659:
4658:
4653:
4651:
4647:
4646:
4645:
4633:
4632:
4590:
4588:
4587:
4582:
4580:
4576:
4575:
4574:
4562:
4561:
4547:
4533:
4529:
4528:
4527:
4515:
4514:
4500:
4471:
4469:
4468:
4463:
4461:
4457:
4456:
4438:
4437:
4425:
4424:
4405:
4403:
4402:
4397:
4395:
4394:
4378:
4376:
4375:
4370:
4368:
4367:
4346:
4345:
4329:
4327:
4326:
4321:
4319:
4318:
4299:
4297:
4296:
4291:
4267:
4265:
4264:
4259:
4257:
4226:
4224:
4223:
4218:
4216:
4182:
4180:
4179:
4174:
4172:
4168:
4167:
4163:
4162:
4144:
4143:
4097:
4095:
4094:
4089:
4087:
4083:
4082:
4058:
4057:
4026:
4024:
4023:
4018:
4005:
4003:
4002:
3997:
3995:
3991:
3990:
3972:
3971:
3938:
3936:
3935:
3930:
3928:
3924:
3923:
3919:
3918:
3917:
3905:
3904:
3890:
3807:
3805:
3804:
3799:
3797:
3750:
3748:
3747:
3742:
3710:
3708:
3707:
3702:
3688:
3684:
3666:
3665:
3646:
3644:
3643:
3638:
3636:
3635:
3612:
3610:
3609:
3604:
3596:
3592:
3574:
3573:
3544:
3542:
3541:
3536:
3512:
3510:
3509:
3504:
3502:
3501:
3465:
3463:
3462:
3457:
3436:
3434:
3433:
3428:
3389:property of the
3384:
3382:
3381:
3376:
3346:
3344:
3343:
3338:
3330:
3326:
3325:
3321:
3273:
3271:
3270:
3265:
3241:
3239:
3238:
3233:
3231:
3217:
3209:
3188:
3186:
3185:
3180:
3131:
3129:
3128:
3123:
3121:
3117:
3102:
3088:
3080:
3050:
3048:
3047:
3042:
2987:
2985:
2984:
2979:
2932:
2930:
2929:
2924:
2898:
2897:
2885:
2884:
2868:
2866:
2865:
2860:
2858:
2857:
2833:
2831:
2830:
2825:
2823:
2822:
2810:
2809:
2784:
2782:
2781:
2776:
2774:
2773:
2755:
2754:
2725:
2723:
2722:
2717:
2715:
2711:
2710:
2709:
2691:
2690:
2657:
2590:
2588:
2587:
2582:
2580:
2576:
2575:
2571:
2570:
2569:
2551:
2550:
2529:
2443:
2441:
2440:
2435:
2433:
2429:
2428:
2424:
2423:
2422:
2410:
2409:
2395:
2314:
2312:
2311:
2306:
2274:
2273:
2257:
2255:
2254:
2249:
2225:
2223:
2222:
2217:
2215:
2211:
2210:
2206:
2205:
2204:
2192:
2191:
2177:
2090:
2088:
2087:
2082:
2080:
2076:
2061:
2047:
2039:
2006:
2004:
2003:
1998:
1996:
1995:
1979:
1977:
1976:
1971:
1960:
1959:
1919:
1917:
1916:
1911:
1906:
1905:
1893:
1892:
1884:
1878:
1864:
1863:
1841:
1839:
1838:
1833:
1799:
1797:
1796:
1791:
1789:
1785:
1784:
1766:
1765:
1740:
1738:
1737:
1732:
1730:
1729:
1721:
1711:
1709:
1708:
1703:
1673:
1671:
1670:
1665:
1617:
1615:
1614:
1609:
1607:
1603:
1602:
1601:
1589:
1588:
1554:
1552:
1551:
1546:
1544:
1540:
1525:
1511:
1503:
1478:
1476:
1475:
1470:
1468:
1467:
1446:
1445:
1425:
1423:
1422:
1417:
1397:
1395:
1394:
1389:
1387:
1386:
1366:
1364:
1363:
1358:
1356:
1352:
1351:
1350:
1338:
1337:
1323:
1309:
1305:
1298:
1294:
1287:
1286:
1251:
1249:
1248:
1243:
1211:
1210:
1194:
1192:
1191:
1186:
1154:
1152:
1151:
1146:
1144:
1140:
1127:
1123:
1105:
1104:
1090:
1076:
1072:
1065:
1061:
1054:
1053:
1017:pattern matching
1010:
1008:
1007:
1002:
987:
985:
984:
979:
977:
973:
966:
949:
945:
927:
908:
866:
864:
863:
858:
826:
824:
823:
818:
795:
776:
774:
773:
768:
745:
712:
710:
709:
704:
696:
692:
691:
687:
653:
651:
650:
645:
637:
633:
632:
628:
576:
574:
573:
568:
541:Pairing function
530:
528:
527:
522:
520:
519:
478:
476:
475:
470:
465:
464:
443:
442:
408:
406:
405:
400:
384:
382:
381:
376:
335:
333:
332:
327:
325:
324:
287:
285:
284:
279:
241:
239:
238:
233:
228:
227:
206:
205:
170:pairing function
74:
67:
63:
60:
54:
24:
23:
16:
7060:
7059:
7055:
7054:
7053:
7051:
7050:
7049:
7035:
7034:
7028:
7011:
7008:
6997:Translation of
6993:
6977:
6971:
6951:
6945:
6928:
6897:
6875:
6869:
6852:
6849:
6844:
6833:
6829:
6821:
6817:
6796:
6795:
6780:
6758:
6754:
6730:
6724:
6723:
6708:
6686:
6682:
6658:
6648:
6617:
6598:
6597:
6593:
6585:
6584:
6546:
6535:
6534:
6530:
6526:
6518:
6514:
6493:
6489:
6477:
6470:
6458:
6454:
6448:Wayback Machine
6435:
6431:
6423:
6419:
6411:
6407:
6395:
6384:
6376:
6372:
6364:
6360:
6348:
6341:
6333:
6326:
6322:
6289:
6266:
6265:
6227:
6203:
6199:
6195:
6191:
6159:
6158:
6154:
6127:
6108:
6089:
6088:
6084:
6079:
6078:
6046:
6035:
6034:
6006:
5962:
5944:
5940:
5936:
5932:
5918:
5914:
5881:
5862:
5861:
5857:
5852:
5851:
5819:
5808:
5807:
5785:
5784:
5781:
5727:
5708:
5707:
5703:
5699:
5695:
5671:
5652:
5644:
5643:
5603:
5581:
5577:
5528:
5509:
5508:
5504:
5496:
5495:
5463:
5405:
5386:
5378:
5377:
5355:
5354:
5347:
5306:
5287:
5286:
5282:
5277:
5276:
5273:
5236:
5178:
5159:
5151:
5150:
5128:
5127:
5124:
5080:
5045:
5044:
5040:
5036:
5032:
5024:
5023:
5004:
5003:
4974:
4961:
4960:
4956:
4910:
4909:
4905:
4901:
4897:
4889:
4888:
4882:
4855:
4837:
4824:
4823:
4819:
4803:
4802:
4766:
4748:
4735:
4734:
4730:
4714:
4713:
4689:
4676:
4671:
4670:
4637:
4624:
4623:
4619:
4601:
4600:
4597:
4566:
4553:
4552:
4548:
4519:
4506:
4505:
4501:
4485:
4484:
4448:
4429:
4416:
4411:
4410:
4386:
4381:
4380:
4353:
4337:
4332:
4331:
4310:
4305:
4304:
4270:
4269:
4247:
4229:
4228:
4206:
4188:
4187:
4154:
4135:
4128:
4124:
4106:
4105:
4068:
4043:
4032:
4031:
4009:
4008:
3982:
3963:
3952:
3951:
3945:
3909:
3896:
3895:
3891:
3855:
3851:
3821:
3820:
3814:
3767:
3766:
3727:
3726:
3674:
3670:
3657:
3652:
3651:
3627:
3622:
3621:
3582:
3578:
3565:
3554:
3553:
3521:
3520:
3493:
3482:
3481:
3475:
3469:can be proven.
3442:
3441:
3395:
3394:
3355:
3354:
3311:
3307:
3300:
3296:
3291:
3290:
3280:
3244:
3243:
3221:
3191:
3190:
3189:; this entails
3141:
3140:
3107:
3103:
3092:
3065:
3064:
3058:
3009:
3008:
3000:(note that the
2946:
2945:
2889:
2876:
2871:
2870:
2849:
2844:
2843:
2814:
2801:
2790:
2789:
2765:
2746:
2735:
2734:
2701:
2682:
2663:
2659:
2603:
2602:
2594:Using a “more”
2561:
2542:
2535:
2531:
2491:
2487:
2457:
2456:
2450:
2414:
2401:
2400:
2396:
2357:
2353:
2323:
2322:
2265:
2260:
2259:
2231:
2230:
2196:
2183:
2182:
2178:
2142:
2138:
2108:
2107:
2066:
2062:
2051:
2024:
2023:
2015:In the section
2013:
1987:
1982:
1981:
1951:
1930:
1929:
1897:
1855:
1850:
1849:
1845:also satisfies
1806:
1805:
1776:
1757:
1746:
1745:
1714:
1713:
1694:
1693:
1685:built with the
1626:
1625:
1593:
1580:
1579:
1575:
1558:
1557:
1530:
1526:
1515:
1488:
1487:
1453:
1437:
1432:
1431:
1408:
1407:
1404:
1378:
1373:
1372:
1342:
1329:
1328:
1324:
1278:
1277:
1273:
1269:
1265:
1257:
1256:
1252:, we can write
1202:
1197:
1196:
1168:
1167:
1113:
1109:
1096:
1095:
1091:
1045:
1044:
1040:
1036:
1032:
1024:
1023:
993:
992:
956:
935:
931:
917:
913:
909:
872:
871:
849:
848:
841:
836:
780:
779:
730:
729:
719:
677:
673:
669:
665:
657:
656:
618:
614:
610:
606:
598:
597:
559:
558:
543:
537:
511:
485:
484:
450:
434:
426:
425:
391:
390:
367:
366:
359:
353:
316:
290:
289:
252:
251:
213:
197:
189:
188:
165:
157:Turing machines
141:
139:Gödel numbering
135:
133:Gödel numbering
113:. For example,
111:Gödel numbering
75:
64:
58:
55:
48:
25:
21:
12:
11:
5:
7058:
7056:
7048:
7047:
7037:
7036:
7033:
7032:
7026:
7007:
7006:External links
7004:
7003:
7002:
6991:
6975:
6969:
6949:
6943:
6926:
6895:
6878:Hajnal, András
6873:
6867:
6848:
6845:
6843:
6842:
6827:
6815:
6813:
6812:
6799:
6793:
6787:
6783:
6779:
6776:
6773:
6770:
6767:
6764:
6761:
6757:
6752:
6749:
6746:
6743:
6738:
6735:
6731:
6729:
6726:
6725:
6721:
6715:
6711:
6707:
6704:
6701:
6698:
6695:
6692:
6689:
6685:
6680:
6677:
6674:
6671:
6666:
6663:
6659:
6657:
6654:
6653:
6651:
6646:
6642:
6638:
6635:
6630:
6627:
6624:
6620:
6616:
6613:
6610:
6605:
6601:
6596:
6592:
6582:
6570:
6566:
6561:
6558:
6555:
6550:
6545:
6542:
6524:
6512:
6487:
6468:
6452:
6429:
6417:
6405:
6382:
6370:
6358:
6352:: 99–100 (see
6339:
6323:
6321:
6318:
6314:
6313:
6301:
6296:
6292:
6287:
6284:
6279:
6276:
6273:
6259:
6258:
6245:
6240:
6234:
6230:
6226:
6222:
6218:
6215:
6212:
6209:
6206:
6202:
6198:
6194:
6189:
6186:
6183:
6180:
6177:
6174:
6171:
6166:
6162:
6157:
6153:
6150:
6147:
6144:
6140:
6134:
6130:
6126:
6121:
6118:
6115:
6111:
6107:
6104:
6101:
6096:
6092:
6087:
6076:
6064:
6060:
6055:
6050:
6045:
6042:
6005:
6002:
5994:
5993:
5980:
5975:
5969:
5965:
5961:
5957:
5953:
5950:
5947:
5943:
5939:
5935:
5930:
5927:
5924:
5921:
5917:
5913:
5910:
5907:
5904:
5900:
5894:
5891:
5888:
5884:
5880:
5877:
5874:
5869:
5865:
5860:
5849:
5837:
5833:
5828:
5823:
5818:
5815:
5792:
5780:
5777:
5776:
5775:
5763:
5759:
5756:
5752:
5748:
5745:
5740:
5737:
5734:
5730:
5726:
5723:
5720:
5715:
5711:
5706:
5702:
5698:
5693:
5690:
5684:
5681:
5678:
5674:
5670:
5667:
5664:
5659:
5655:
5651:
5629:
5628:
5616:
5610:
5606:
5602:
5599:
5596:
5593:
5590:
5587:
5584:
5580:
5575:
5572:
5569:
5566:
5563:
5560:
5557:
5553:
5549:
5546:
5541:
5538:
5535:
5531:
5527:
5524:
5521:
5516:
5512:
5507:
5503:
5484:
5483:
5470:
5466:
5462:
5459:
5456:
5453:
5450:
5447:
5444:
5440:
5437:
5434:
5431:
5427:
5424:
5418:
5415:
5412:
5408:
5404:
5401:
5398:
5393:
5389:
5385:
5362:
5351:minimalization
5346:
5343:
5325:
5319:
5316:
5313:
5309:
5305:
5302:
5299:
5294:
5290:
5285:
5272:
5269:
5257:
5256:
5243:
5239:
5235:
5232:
5229:
5226:
5223:
5220:
5217:
5213:
5210:
5207:
5204:
5200:
5197:
5191:
5188:
5185:
5181:
5177:
5174:
5171:
5166:
5162:
5158:
5135:
5123:
5120:
5087:
5083:
5079:
5075:
5071:
5068:
5064:
5060:
5057:
5052:
5048:
5043:
5039:
5035:
5031:
5011:
5000:
4999:
4987:
4981:
4977:
4973:
4968:
4964:
4959:
4954:
4951:
4948:
4944:
4940:
4936:
4933:
4929:
4925:
4922:
4917:
4913:
4908:
4904:
4900:
4896:
4881:
4878:
4877:
4876:
4862:
4858:
4854:
4850:
4844:
4840:
4836:
4831:
4827:
4822:
4817:
4814:
4811:
4788:
4787:
4773:
4769:
4765:
4761:
4755:
4751:
4747:
4742:
4738:
4733:
4728:
4725:
4722:
4696:
4692:
4688:
4683:
4679:
4650:
4644:
4640:
4636:
4631:
4627:
4622:
4617:
4614:
4611:
4608:
4596:
4593:
4592:
4591:
4579:
4573:
4569:
4565:
4560:
4556:
4551:
4546:
4543:
4540:
4536:
4532:
4526:
4522:
4518:
4513:
4509:
4504:
4499:
4496:
4493:
4474:
4473:
4460:
4455:
4451:
4446:
4443:
4436:
4432:
4428:
4423:
4419:
4406:as satisfying
4393:
4389:
4366:
4363:
4360:
4356:
4352:
4349:
4344:
4340:
4317:
4313:
4289:
4286:
4283:
4280:
4277:
4256:
4253:
4250:
4245:
4242:
4239:
4236:
4215:
4212:
4209:
4204:
4201:
4198:
4195:
4184:
4183:
4171:
4166:
4161:
4157:
4152:
4149:
4142:
4138:
4134:
4131:
4127:
4122:
4119:
4116:
4113:
4099:
4098:
4086:
4081:
4078:
4075:
4071:
4066:
4063:
4056:
4053:
4050:
4046:
4042:
4039:
4029:
4028:
4027:
4016:
3994:
3989:
3985:
3980:
3977:
3970:
3966:
3962:
3959:
3944:
3941:
3940:
3939:
3927:
3922:
3916:
3912:
3908:
3903:
3899:
3894:
3889:
3886:
3883:
3880:
3877:
3874:
3871:
3867:
3864:
3861:
3858:
3854:
3849:
3846:
3843:
3840:
3837:
3834:
3831:
3828:
3813:
3810:
3796:
3793:
3790:
3787:
3784:
3780:
3777:
3774:
3752:
3751:
3740:
3737:
3734:
3712:
3711:
3700:
3697:
3694:
3691:
3687:
3683:
3680:
3677:
3673:
3669:
3664:
3660:
3634:
3630:
3614:
3613:
3602:
3599:
3595:
3591:
3588:
3585:
3581:
3577:
3572:
3568:
3564:
3561:
3547:
3546:
3534:
3531:
3528:
3514:
3513:
3500:
3496:
3492:
3489:
3474:
3471:
3467:
3466:
3455:
3452:
3449:
3426:
3423:
3420:
3417:
3414:
3411:
3408:
3405:
3402:
3374:
3371:
3368:
3365:
3362:
3348:
3347:
3336:
3333:
3329:
3324:
3320:
3317:
3314:
3310:
3306:
3303:
3299:
3279:
3276:
3263:
3260:
3257:
3254:
3251:
3230:
3227:
3224:
3220:
3215:
3212:
3207:
3204:
3201:
3198:
3178:
3175:
3172:
3169:
3166:
3163:
3160:
3157:
3154:
3151:
3148:
3134:
3133:
3120:
3116:
3113:
3110:
3106:
3101:
3098:
3095:
3091:
3086:
3083:
3078:
3075:
3072:
3057:
3054:
3053:
3052:
3040:
3037:
3034:
3031:
3028:
3025:
3022:
3019:
3016:
2990:
2989:
2977:
2974:
2971:
2968:
2965:
2962:
2959:
2956:
2953:
2922:
2919:
2916:
2913:
2910:
2907:
2904:
2901:
2896:
2892:
2888:
2883:
2879:
2856:
2852:
2836:
2835:
2821:
2817:
2813:
2808:
2804:
2800:
2797:
2772:
2768:
2764:
2761:
2758:
2753:
2749:
2745:
2742:
2727:
2726:
2714:
2708:
2704:
2700:
2697:
2694:
2689:
2685:
2681:
2678:
2675:
2672:
2669:
2666:
2662:
2656:
2653:
2650:
2647:
2644:
2640:
2637:
2634:
2631:
2628:
2625:
2622:
2619:
2616:
2613:
2610:
2592:
2591:
2579:
2574:
2568:
2564:
2560:
2557:
2554:
2549:
2545:
2541:
2538:
2534:
2528:
2525:
2522:
2519:
2516:
2512:
2509:
2506:
2503:
2500:
2497:
2494:
2490:
2485:
2482:
2479:
2476:
2473:
2470:
2467:
2464:
2449:
2446:
2445:
2444:
2432:
2427:
2421:
2417:
2413:
2408:
2404:
2399:
2394:
2391:
2388:
2385:
2382:
2379:
2376:
2372:
2369:
2366:
2363:
2360:
2356:
2351:
2348:
2345:
2342:
2339:
2336:
2333:
2330:
2304:
2301:
2298:
2295:
2292:
2289:
2286:
2283:
2280:
2277:
2272:
2268:
2247:
2244:
2241:
2238:
2227:
2226:
2214:
2209:
2203:
2199:
2195:
2190:
2186:
2181:
2176:
2173:
2170:
2167:
2164:
2161:
2158:
2154:
2151:
2148:
2145:
2141:
2136:
2133:
2130:
2127:
2124:
2121:
2118:
2115:
2101:
2100:
2079:
2075:
2072:
2069:
2065:
2060:
2057:
2054:
2050:
2045:
2042:
2037:
2034:
2031:
2012:
2009:
1994:
1990:
1969:
1966:
1963:
1958:
1954:
1950:
1946:
1943:
1940:
1937:
1922:
1921:
1909:
1904:
1900:
1896:
1890:
1887:
1881:
1877:
1874:
1871:
1867:
1862:
1858:
1843:
1842:
1831:
1828:
1825:
1822:
1819:
1816:
1813:
1788:
1783:
1779:
1774:
1771:
1764:
1760:
1756:
1753:
1727:
1724:
1701:
1683:constructively
1675:
1674:
1663:
1660:
1657:
1654:
1651:
1648:
1645:
1642:
1639:
1636:
1633:
1619:
1618:
1606:
1600:
1596:
1592:
1587:
1583:
1578:
1574:
1571:
1568:
1565:
1555:
1543:
1539:
1536:
1533:
1529:
1524:
1521:
1518:
1514:
1509:
1506:
1501:
1498:
1495:
1466:
1463:
1460:
1456:
1452:
1449:
1444:
1440:
1415:
1403:
1400:
1385:
1381:
1369:
1368:
1355:
1349:
1345:
1341:
1336:
1332:
1327:
1322:
1319:
1316:
1312:
1308:
1304:
1301:
1297:
1293:
1290:
1285:
1281:
1276:
1272:
1268:
1264:
1241:
1238:
1235:
1232:
1229:
1226:
1223:
1220:
1217:
1214:
1209:
1205:
1184:
1181:
1178:
1175:
1156:
1155:
1143:
1139:
1136:
1133:
1130:
1126:
1122:
1119:
1116:
1112:
1108:
1103:
1099:
1094:
1089:
1086:
1083:
1079:
1075:
1071:
1068:
1064:
1060:
1057:
1052:
1048:
1043:
1039:
1035:
1031:
1000:
989:
988:
976:
972:
969:
965:
962:
959:
955:
952:
948:
944:
941:
938:
934:
930:
926:
923:
920:
916:
912:
907:
904:
901:
897:
894:
891:
888:
885:
882:
879:
856:
840:
837:
835:
832:
828:
827:
816:
813:
810:
807:
804:
801:
798:
794:
791:
788:
777:
766:
763:
760:
757:
754:
751:
748:
744:
741:
738:
718:
715:
714:
713:
702:
699:
695:
690:
686:
683:
680:
676:
672:
668:
664:
654:
643:
640:
636:
631:
627:
624:
621:
617:
613:
609:
605:
566:
551:implementation
539:Main article:
536:
533:
518:
514:
510:
507:
504:
501:
498:
495:
492:
468:
463:
460:
457:
453:
449:
446:
441:
437:
433:
416:Thus, for all
398:
387:specifications
374:
352:
349:
323:
319:
315:
312:
309:
306:
303:
300:
297:
277:
274:
271:
268:
265:
262:
259:
231:
226:
223:
220:
216:
212:
209:
204:
200:
196:
164:
161:
137:Main article:
134:
131:
77:
76:
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
7057:
7046:
7043:
7042:
7040:
7029:
7023:
7019:
7015:
7010:
7009:
7005:
7000:
6999:Smullyan 1992
6994:
6988:
6984:
6980:
6976:
6972:
6966:
6961:
6960:
6954:
6950:
6946:
6944:9780387901701
6940:
6935:
6934:
6927:
6923:
6918:
6913:
6910:(2): 98–107.
6909:
6905:
6901:
6896:
6893:
6892:author's page
6887:
6883:
6879:
6874:
6870:
6864:
6860:
6856:
6851:
6850:
6846:
6840:
6836:
6831:
6828:
6824:
6819:
6816:
6791:
6785:
6781:
6777:
6771:
6768:
6765:
6759:
6755:
6750:
6747:
6744:
6727:
6719:
6713:
6709:
6705:
6699:
6696:
6693:
6687:
6683:
6678:
6675:
6672:
6655:
6649:
6644:
6640:
6636:
6633:
6628:
6625:
6622:
6618:
6614:
6611:
6608:
6603:
6599:
6594:
6590:
6583:
6559:
6556:
6553:
6543:
6540:
6533:
6532:
6528:
6525:
6521:
6516:
6513:
6509:
6505:
6501:
6497:
6491:
6488:
6485:
6481:
6475:
6473:
6469:
6465:
6461:
6456:
6453:
6449:
6445:
6442:
6438:
6433:
6430:
6426:
6421:
6418:
6414:
6413:Smullyan 2003
6409:
6406:
6402:
6398:
6393:
6391:
6389:
6387:
6383:
6379:
6374:
6371:
6367:
6362:
6359:
6355:
6351:
6346:
6344:
6340:
6336:
6331:
6329:
6325:
6319:
6317:
6294:
6290:
6285:
6277:
6274:
6271:
6264:
6263:
6262:
6243:
6238:
6232:
6228:
6224:
6220:
6216:
6213:
6210:
6207:
6204:
6200:
6196:
6192:
6187:
6184:
6181:
6175:
6172:
6169:
6164:
6160:
6155:
6151:
6148:
6145:
6138:
6132:
6128:
6124:
6119:
6116:
6113:
6109:
6105:
6102:
6099:
6094:
6090:
6085:
6077:
6053:
6043:
6040:
6033:
6032:
6031:
6028:
6024:
6022:
6018:
6013:
6011:
6003:
6001:
5999:
5978:
5973:
5967:
5963:
5959:
5955:
5951:
5948:
5945:
5941:
5937:
5933:
5928:
5925:
5922:
5915:
5911:
5908:
5905:
5898:
5892:
5889:
5886:
5882:
5878:
5875:
5872:
5867:
5863:
5858:
5850:
5826:
5816:
5813:
5806:
5805:
5804:
5790:
5778:
5761:
5757:
5754:
5750:
5746:
5743:
5738:
5735:
5732:
5728:
5724:
5721:
5718:
5713:
5709:
5704:
5700:
5696:
5691:
5682:
5679:
5676:
5672:
5668:
5665:
5662:
5657:
5653:
5642:
5641:
5640:
5638:
5634:
5614:
5608:
5604:
5600:
5594:
5591:
5588:
5582:
5578:
5573:
5570:
5567:
5558:
5555:
5551:
5547:
5544:
5539:
5536:
5533:
5529:
5525:
5522:
5519:
5514:
5510:
5505:
5501:
5494:
5493:
5492:
5490:
5468:
5464:
5460:
5454:
5451:
5448:
5442:
5438:
5435:
5432:
5425:
5416:
5413:
5410:
5406:
5402:
5399:
5396:
5391:
5387:
5376:
5375:
5374:
5360:
5352:
5344:
5342:
5340:
5323:
5317:
5314:
5311:
5307:
5303:
5300:
5297:
5292:
5288:
5283:
5270:
5268:
5266:
5262:
5241:
5237:
5233:
5227:
5224:
5221:
5215:
5211:
5208:
5205:
5198:
5189:
5186:
5183:
5179:
5175:
5172:
5169:
5164:
5160:
5149:
5148:
5147:
5133:
5121:
5119:
5117:
5112:
5110:
5106:
5101:
5085:
5081:
5077:
5073:
5069:
5066:
5062:
5058:
5055:
5050:
5046:
5041:
5037:
5033:
5029:
5009:
4985:
4979:
4975:
4971:
4966:
4962:
4957:
4942:
4938:
4934:
4931:
4927:
4923:
4920:
4915:
4911:
4906:
4902:
4898:
4894:
4887:
4886:
4885:
4879:
4860:
4856:
4852:
4848:
4842:
4838:
4834:
4829:
4825:
4820:
4801:
4800:
4799:
4797:
4793:
4771:
4767:
4763:
4759:
4753:
4749:
4745:
4740:
4736:
4731:
4712:
4711:
4710:
4709:implies that
4694:
4690:
4686:
4681:
4677:
4667:
4665:
4648:
4642:
4638:
4634:
4629:
4625:
4620:
4615:
4612:
4609:
4594:
4577:
4571:
4567:
4563:
4558:
4554:
4549:
4534:
4530:
4524:
4520:
4516:
4511:
4507:
4502:
4483:
4482:
4481:
4479:
4453:
4449:
4444:
4434:
4430:
4426:
4421:
4417:
4409:
4408:
4407:
4391:
4387:
4364:
4361:
4358:
4354:
4350:
4347:
4342:
4338:
4315:
4311:
4301:
4300:begins here.
4284:
4281:
4278:
4254:
4251:
4248:
4243:
4240:
4237:
4213:
4210:
4207:
4202:
4199:
4196:
4169:
4159:
4155:
4150:
4140:
4136:
4132:
4129:
4125:
4120:
4117:
4114:
4104:
4103:
4102:
4079:
4076:
4073:
4069:
4064:
4054:
4051:
4048:
4044:
4040:
4037:
4030:
4014:
4007:
4006:
3987:
3983:
3978:
3968:
3964:
3960:
3957:
3950:
3949:
3948:
3942:
3925:
3920:
3914:
3910:
3906:
3901:
3897:
3892:
3862:
3859:
3856:
3852:
3847:
3844:
3841:
3838:
3835:
3832:
3829:
3819:
3818:
3817:
3811:
3809:
3778:
3775:
3764:
3760:
3755:
3738:
3735:
3732:
3725:
3724:
3723:
3721:
3717:
3698:
3695:
3692:
3689:
3685:
3681:
3678:
3675:
3671:
3667:
3662:
3658:
3650:
3649:
3648:
3632:
3628:
3619:
3600:
3597:
3593:
3589:
3586:
3583:
3579:
3575:
3570:
3566:
3562:
3559:
3552:
3551:
3550:
3532:
3529:
3526:
3519:
3518:
3517:
3498:
3494:
3490:
3487:
3480:
3479:
3478:
3472:
3470:
3453:
3450:
3447:
3440:
3439:
3438:
3424:
3421:
3418:
3412:
3409:
3406:
3403:
3400:
3392:
3388:
3372:
3369:
3366:
3363:
3360:
3351:
3334:
3327:
3322:
3318:
3312:
3308:
3304:
3301:
3297:
3289:
3288:
3287:
3285:
3277:
3275:
3261:
3258:
3255:
3252:
3249:
3228:
3225:
3222:
3210:
3205:
3202:
3199:
3196:
3176:
3173:
3170:
3167:
3164:
3161:
3158:
3155:
3152:
3149:
3146:
3137:
3118:
3114:
3111:
3108:
3104:
3099:
3096:
3093:
3081:
3076:
3073:
3063:
3062:
3061:
3055:
3038:
3035:
3032:
3029:
3026:
3023:
3020:
3017:
3014:
3007:
3006:
3005:
3003:
2999:
2998:prime element
2995:
2975:
2972:
2966:
2963:
2960:
2954:
2951:
2944:
2943:
2942:
2940:
2936:
2920:
2917:
2911:
2908:
2905:
2899:
2894:
2890:
2886:
2881:
2877:
2854:
2850:
2841:
2819:
2815:
2811:
2806:
2802:
2798:
2795:
2788:
2787:
2786:
2770:
2766:
2762:
2759:
2756:
2751:
2747:
2743:
2740:
2732:
2712:
2706:
2702:
2698:
2695:
2692:
2687:
2683:
2679:
2676:
2673:
2670:
2667:
2664:
2660:
2638:
2635:
2632:
2629:
2626:
2623:
2620:
2617:
2614:
2611:
2601:
2600:
2599:
2597:
2577:
2572:
2566:
2562:
2558:
2555:
2552:
2547:
2543:
2539:
2536:
2532:
2510:
2507:
2501:
2498:
2495:
2492:
2488:
2483:
2480:
2477:
2474:
2471:
2468:
2465:
2455:
2454:
2453:
2447:
2430:
2425:
2419:
2415:
2411:
2406:
2402:
2397:
2367:
2364:
2361:
2358:
2354:
2349:
2346:
2343:
2340:
2337:
2334:
2331:
2321:
2320:
2319:
2316:
2302:
2299:
2296:
2293:
2287:
2284:
2281:
2275:
2270:
2266:
2245:
2242:
2239:
2212:
2207:
2201:
2197:
2193:
2188:
2184:
2179:
2149:
2146:
2143:
2139:
2134:
2131:
2128:
2125:
2122:
2119:
2116:
2106:
2105:
2104:
2098:
2094:
2077:
2073:
2070:
2067:
2063:
2058:
2055:
2052:
2040:
2035:
2032:
2022:
2021:
2020:
2018:
2010:
2008:
1992:
1988:
1964:
1961:
1956:
1952:
1944:
1941:
1938:
1927:
1902:
1898:
1894:
1885:
1865:
1860:
1856:
1848:
1847:
1846:
1829:
1826:
1823:
1820:
1817:
1814:
1811:
1803:
1781:
1777:
1772:
1762:
1758:
1754:
1751:
1744:
1743:
1742:
1722:
1699:
1690:
1688:
1684:
1680:
1661:
1658:
1655:
1652:
1649:
1646:
1643:
1640:
1637:
1634:
1631:
1624:
1623:
1622:
1604:
1598:
1594:
1590:
1585:
1581:
1576:
1572:
1569:
1566:
1556:
1541:
1537:
1534:
1531:
1527:
1522:
1519:
1516:
1504:
1499:
1496:
1486:
1485:
1484:
1482:
1464:
1461:
1458:
1454:
1450:
1447:
1442:
1438:
1428:
1413:
1401:
1399:
1383:
1379:
1353:
1347:
1343:
1339:
1334:
1330:
1325:
1310:
1306:
1302:
1299:
1295:
1291:
1288:
1283:
1279:
1274:
1270:
1266:
1262:
1255:
1254:
1253:
1239:
1236:
1233:
1230:
1224:
1221:
1218:
1212:
1207:
1203:
1195:the sequence
1182:
1179:
1176:
1165:
1161:
1141:
1137:
1134:
1131:
1128:
1124:
1120:
1117:
1114:
1110:
1106:
1101:
1097:
1092:
1077:
1073:
1069:
1066:
1062:
1058:
1055:
1050:
1046:
1041:
1037:
1033:
1029:
1022:
1021:
1020:
1018:
1014:
998:
974:
970:
967:
963:
960:
957:
953:
950:
946:
942:
939:
936:
932:
928:
924:
921:
918:
914:
910:
895:
889:
886:
883:
877:
870:
869:
868:
854:
846:
838:
833:
831:
814:
811:
805:
802:
799:
778:
764:
761:
755:
752:
749:
728:
727:
726:
724:
716:
700:
697:
693:
688:
684:
681:
678:
674:
670:
666:
662:
655:
641:
638:
634:
629:
625:
622:
619:
615:
611:
607:
603:
596:
595:
594:
592:
591:specification
588:
584:
580:
564:
556:
552:
548:
542:
534:
532:
516:
512:
508:
502:
499:
496:
490:
482:
461:
458:
455:
451:
447:
444:
439:
435:
423:
419:
414:
412:
396:
388:
372:
364:
358:
348:
346:
342:
337:
321:
317:
313:
307:
304:
301:
295:
275:
272:
269:
266:
263:
260:
257:
249:
245:
224:
221:
218:
214:
210:
207:
202:
198:
186:
182:
178:
173:
171:
162:
160:
158:
154:
150:
146:
140:
132:
130:
128:
124:
120:
116:
112:
108:
103:
101:
97:
92:
88:
84:
73:
70:
62:
52:
47:
45:
39:
35:
34:
27:
18:
17:
7017:
6982:
6958:
6932:
6922:the original
6907:
6903:
6885:
6858:
6835:Csirmaz 1994
6830:
6818:
6527:
6515:
6504:Venn diagram
6490:
6464:Arithmetic I
6455:
6432:
6420:
6408:
6397:Csirmaz 1994
6373:
6361:
6350:Csirmaz 1994
6315:
6260:
6029:
6025:
6014:
6007:
5997:
5995:
5782:
5632:
5630:
5488:
5485:
5348:
5339:constructive
5274:
5258:
5125:
5118:ends here.)
5115:
5113:
5105:transitivity
5102:
5001:
4883:
4792:transitivity
4789:
4668:
4663:
4598:
4475:
4302:
4185:
4100:
3946:
3815:
3758:
3756:
3753:
3716:transitivity
3713:
3615:
3548:
3515:
3476:
3468:
3391:divisibility
3387:transitivity
3352:
3349:
3281:
3138:
3135:
3059:
2993:
2991:
2837:
2731:divisibility
2728:
2593:
2451:
2317:
2228:
2102:
2014:
1925:
1923:
1844:
1801:
1691:
1676:
1620:
1480:
1429:
1405:
1370:
1157:
990:
842:
829:
725:. Examples:
720:
582:
578:
544:
480:
421:
420:and for any
417:
415:
360:
341:constructive
338:
247:
243:
184:
183:and for any
180:
176:
174:
166:
142:
104:
86:
80:
65:
59:January 2017
56:
49:Please help
41:
30:
6496:truth table
6460:Burris 1998
6437:Hughes 1989
6399:: 100 (see
2933:, thus (as
2840:definitions
2448:First steps
2258:we defined
2103:In detail:
2007:as above).
83:mathematics
53:if you can.
6847:References
5803:function:
5265:uniqueness
5022:: we want
3618:definition
3393:relation,
1928:requiring
1160:modularity
843:Using the
587:projection
355:See also:
107:data types
6823:Monk 1976
6778:≠
6760:β
6742:∃
6688:β
6670:∀
6626:−
6612:…
6565:→
6520:Monk 1976
6466:, Lemma 4
6425:Monk 1976
6378:Monk 1976
6366:Monk 1976
6335:Monk 1976
6275:≡
6197:β
6179:∀
6176:∧
6146:μ
6143:⟼
6117:−
6103:…
6059:→
6054:∗
6010:analogous
5938:β
5920:∀
5906:μ
5903:⟼
5890:−
5876:…
5832:→
5791:β
5736:−
5722:…
5689:∃
5680:−
5666:…
5650:∀
5583:β
5565:∀
5562:↔
5537:−
5523:…
5443:β
5430:∀
5423:∃
5414:−
5400:…
5384:∀
5361:β
5315:−
5301:…
5261:existence
5216:β
5203:∀
5196:∃
5187:−
5173:…
5157:∀
5134:β
5100:to hold.
5038:π
5030:β
5010:β
4903:π
4895:β
4607:∀
4427:≡
4362:−
4351:…
4276:∀
4252:…
4235:∀
4211:…
4194:∀
4133:≡
4112:∀
4077:−
4052:−
4041:≡
4015:⋮
3961:≡
3866:→
3860:≠
3827:∀
3779:∈
3773:∃
3736:∣
3690:⋅
3668:−
3598:⋅
3576:−
3563:∣
3530:∣
3491:∣
3451:∣
3422:∣
3416:→
3410:−
3404:∣
3385:, by the
3370:∣
3364:−
3332:→
3316:→
3305:∧
3259:∣
3253:−
3219:∖
3214:¯
3206:∈
3200:−
3174:≠
3168:∧
3156:∧
3112:∣
3090:∖
3085:¯
3077:∈
3071:∀
3036:∣
3030:∨
3024:−
3018:∣
2973:⋅
2964:−
2955:∣
2941:) we get
2918:⋅
2909:−
2887:−
2812:−
2799:∣
2763:∣
2757:∧
2744:∣
2699:∣
2693:∧
2680:∣
2674:∧
2668:≠
2639:∈
2609:∃
2559:∣
2553:∧
2540:∣
2511:∈
2505:∃
2502:∧
2496:≠
2463:∃
2371:¬
2368:∧
2362:≠
2329:∃
2294:⋅
2237:∀
2153:→
2147:≠
2114:∀
2071:∣
2049:∖
2044:¯
2036:∈
2030:∀
1936:∀
1889:~
1827:−
1821:≤
1815:≤
1800:for each
1755:≡
1726:~
1700:β
1687:factorial
1659:∣
1653:−
1647:∧
1644:⋯
1641:∧
1635:∣
1564:∀
1535:∣
1513:∖
1508:¯
1500:∈
1494:∀
1462:−
1451:…
1414:β
1271:π
1263:β
1231:⋅
1174:∀
1129:⋅
1038:π
1030:β
999:β
951:⋅
878:β
855:β
671:π
612:π
565:π
555:interface
491:β
467:⟩
459:−
448:…
432:⟨
397:β
373:β
273:−
267:≤
261:≤
230:⟩
222:−
211:…
195:⟨
125:to mimic
119:algorithm
91:embedding
7039:Category
6981:(2003).
6955:(1992).
6880:(1994).
6444:Archived
6139:⟩
6086:⟨
5899:⟩
5859:⟨
5324:⟩
5284:⟨
5109:equality
4796:equality
3720:equality
2935:equality
547:abstract
31:require
6380:: 52–55
6368:: 72–74
6337:: 56–58
4798:we get
4790:Now by
4480:) that
3718:of the
3350:holds.
3274:holds.
2093:coprime
1679:coprime
557:”: let
33:cleanup
7024:
6989:
6967:
6941:
6865:
6839:online
6441:online
6401:online
6354:online
3549:Thus,
3353:Since
2992:Since
1804:where
581:, and
250:where
6439:(see
6320:Notes
6021:lists
6017:typed
3286:that
2996:is a
1164:reuse
155:, or
127:lists
7022:ISBN
6987:ISBN
6965:ISBN
6939:ISBN
6863:ISBN
6748:<
6676:<
6185:<
5926:<
5637:root
5635:has
5571:<
5436:<
5263:and
5209:<
4687:<
4635:<
4613:<
4282:<
4241:<
4200:<
4118:<
3845:<
3833:<
3162:<
3150:<
2627:<
2615:<
2481:<
2469:<
2347:<
2335:<
2243:<
2132:<
2120:<
1962:<
1942:<
1591:<
1570:<
1430:Let
1180:<
1162:and
85:, a
6912:doi
6286:mod
5107:of
4880:QED
4794:of
4445:mod
4151:mod
4065:mod
3979:mod
3761:is
3620:of
2842:of
1773:mod
1019:):
867:as
147:or
81:In
7041::
7016:.
6908:32
6906:.
6902:.
6884:.
6857:.
6506:,
6502:,
6498:,
6471:^
6385:^
6342:^
6327:^
3722:,
3647:,
2733:,
2315:.
593::
577:,
531:.
413:.
347:.
336:.
288:,
172:.
102:.
7030:.
7001:.
6995:.
6973:.
6947:.
6914::
6894:.
6871:.
6792:)
6786:i
6782:a
6775:)
6772:i
6769:,
6766:s
6763:(
6756:(
6751:n
6745:i
6737:f
6734:i
6728:1
6720:)
6714:i
6710:a
6706:=
6703:)
6700:i
6697:,
6694:s
6691:(
6684:(
6679:n
6673:i
6665:f
6662:i
6656:0
6650:{
6645:=
6641:)
6637:s
6634:,
6629:1
6623:n
6619:a
6615:,
6609:,
6604:0
6600:a
6595:(
6591:f
6569:N
6560:1
6557:+
6554:n
6549:N
6544::
6541:f
6510:)
6450:)
6403:)
6356:)
6300:)
6295:0
6291:m
6283:(
6278:n
6272:x
6257:.
6244:]
6239:)
6233:i
6229:a
6225:=
6221:)
6217:1
6214:+
6211:i
6208:,
6205:a
6201:(
6193:(
6188:n
6182:i
6173:n
6170:=
6165:0
6161:a
6156:[
6152:.
6149:a
6133:n
6129:a
6125:,
6120:1
6114:n
6110:a
6106:,
6100:,
6095:0
6091:a
6063:N
6049:N
6044::
6041:g
5998:g
5992:.
5979:]
5974:)
5968:i
5964:a
5960:=
5956:)
5952:i
5949:,
5946:a
5942:(
5934:(
5929:n
5923:i
5916:[
5912:.
5909:a
5893:1
5887:n
5883:a
5879:,
5873:,
5868:0
5864:a
5836:N
5827:n
5822:N
5817::
5814:g
5762:)
5758:0
5755:=
5751:)
5747:s
5744:,
5739:1
5733:n
5729:a
5725:,
5719:,
5714:0
5710:a
5705:(
5701:f
5697:(
5692:s
5683:1
5677:n
5673:a
5669:,
5663:,
5658:0
5654:a
5633:f
5615:)
5609:i
5605:a
5601:=
5598:)
5595:i
5592:,
5589:s
5586:(
5579:(
5574:n
5568:i
5559:0
5556:=
5552:)
5548:s
5545:,
5540:1
5534:n
5530:a
5526:,
5520:,
5515:0
5511:a
5506:(
5502:f
5489:f
5469:i
5465:a
5461:=
5458:)
5455:i
5452:,
5449:s
5446:(
5439:n
5433:i
5426:s
5417:1
5411:n
5407:a
5403:,
5397:,
5392:0
5388:a
5318:1
5312:n
5308:a
5304:,
5298:,
5293:0
5289:a
5242:i
5238:a
5234:=
5231:)
5228:i
5225:,
5222:s
5219:(
5212:n
5206:i
5199:s
5190:1
5184:n
5180:a
5176:,
5170:,
5165:0
5161:a
5116:i
5086:i
5082:a
5078:=
5074:)
5070:i
5067:,
5063:)
5059:m
5056:,
5051:0
5047:x
5042:(
5034:(
4986:)
4980:i
4976:m
4972:,
4967:0
4963:x
4958:(
4953:m
4950:e
4947:r
4943:=
4939:)
4935:i
4932:,
4928:)
4924:m
4921:,
4916:0
4912:x
4907:(
4899:(
4875:.
4861:i
4857:a
4853:=
4849:)
4843:i
4839:m
4835:,
4830:0
4826:x
4821:(
4816:m
4813:e
4810:r
4786:.
4772:i
4768:a
4764:=
4760:)
4754:i
4750:m
4746:,
4741:i
4737:a
4732:(
4727:m
4724:e
4721:r
4695:i
4691:m
4682:i
4678:a
4664:i
4649:)
4643:i
4639:m
4630:i
4626:a
4621:(
4616:n
4610:i
4578:)
4572:i
4568:m
4564:,
4559:i
4555:a
4550:(
4545:m
4542:e
4539:r
4535:=
4531:)
4525:i
4521:m
4517:,
4512:0
4508:x
4503:(
4498:m
4495:e
4492:r
4472:,
4459:)
4454:i
4450:m
4442:(
4435:i
4431:a
4422:0
4418:x
4392:0
4388:x
4365:1
4359:n
4355:m
4348:,
4343:0
4339:m
4316:0
4312:x
4288:(
4285:n
4279:i
4255:)
4249:(
4244:n
4238:i
4214:)
4208:(
4203:n
4197:i
4170:)
4165:)
4160:i
4156:m
4148:(
4141:i
4137:a
4130:x
4126:(
4121:n
4115:i
4085:)
4080:1
4074:n
4070:m
4062:(
4055:1
4049:n
4045:a
4038:x
3993:)
3988:0
3984:m
3976:(
3969:0
3965:a
3958:x
3926:)
3921:)
3915:j
3911:m
3907:,
3902:i
3898:m
3893:(
3888:e
3885:m
3882:i
3879:r
3876:p
3873:o
3870:c
3863:j
3857:i
3853:(
3848:n
3842:j
3839:,
3836:n
3830:i
3795:e
3792:m
3789:i
3786:r
3783:P
3776:p
3759:p
3739:1
3733:p
3699:1
3696:=
3693:m
3686:)
3682:1
3679:+
3676:i
3672:(
3663:i
3659:m
3633:i
3629:m
3601:m
3594:)
3590:1
3587:+
3584:i
3580:(
3571:i
3567:m
3560:p
3545:.
3533:m
3527:p
3499:i
3495:m
3488:p
3454:m
3448:p
3425:m
3419:p
3413:j
3407:i
3401:p
3373:m
3367:j
3361:i
3335:B
3328:)
3323:)
3319:B
3313:A
3309:(
3302:A
3298:(
3262:m
3256:j
3250:i
3229:}
3226:0
3223:{
3211:n
3203:j
3197:i
3177:j
3171:i
3165:n
3159:j
3153:n
3147:i
3132:.
3119:)
3115:m
3109:i
3105:(
3100:}
3097:0
3094:{
3082:n
3074:i
3051:.
3039:m
3033:p
3027:j
3021:i
3015:p
2994:p
2988:.
2976:m
2970:)
2967:j
2961:i
2958:(
2952:p
2921:m
2915:)
2912:j
2906:i
2903:(
2900:=
2895:j
2891:m
2882:i
2878:m
2855:k
2851:m
2834:.
2820:j
2816:m
2807:i
2803:m
2796:p
2771:j
2767:m
2760:p
2752:i
2748:m
2741:p
2713:)
2707:j
2703:m
2696:p
2688:i
2684:m
2677:p
2671:j
2665:i
2661:(
2655:e
2652:m
2649:i
2646:r
2643:P
2636:p
2633:,
2630:n
2624:j
2621:,
2618:n
2612:i
2578:)
2573:)
2567:j
2563:m
2556:p
2548:i
2544:m
2537:p
2533:(
2527:e
2524:m
2521:i
2518:r
2515:P
2508:p
2499:j
2493:i
2489:(
2484:n
2478:j
2475:,
2472:n
2466:i
2431:)
2426:)
2420:j
2416:m
2412:,
2407:i
2403:m
2398:(
2393:e
2390:m
2387:i
2384:r
2381:p
2378:o
2375:c
2365:j
2359:i
2355:(
2350:n
2344:j
2341:,
2338:n
2332:i
2303:1
2300:+
2297:m
2291:)
2288:1
2285:+
2282:i
2279:(
2276:=
2271:i
2267:m
2246:n
2240:i
2213:)
2208:)
2202:j
2198:m
2194:,
2189:i
2185:m
2180:(
2175:e
2172:m
2169:i
2166:r
2163:p
2160:o
2157:c
2150:j
2144:i
2140:(
2135:n
2129:j
2126:,
2123:n
2117:i
2099:.
2078:)
2074:m
2068:i
2064:(
2059:}
2056:0
2053:{
2041:n
2033:i
1993:i
1989:m
1968:)
1965:m
1957:i
1953:a
1949:(
1945:n
1939:i
1926:m
1920:.
1908:)
1903:i
1899:m
1895:,
1886:x
1880:(
1876:m
1873:e
1870:r
1866:=
1861:i
1857:a
1830:1
1824:n
1818:i
1812:0
1802:i
1787:)
1782:i
1778:m
1770:(
1763:i
1759:a
1752:x
1723:x
1662:m
1656:1
1650:n
1638:m
1632:1
1605:)
1599:i
1595:m
1586:i
1582:a
1577:(
1573:n
1567:i
1542:)
1538:m
1532:i
1528:(
1523:}
1520:0
1517:{
1505:n
1497:i
1481:m
1465:1
1459:n
1455:a
1448:,
1443:0
1439:a
1384:i
1380:m
1367:.
1354:)
1348:i
1344:m
1340:,
1335:0
1331:x
1326:(
1321:m
1318:e
1315:r
1311:=
1307:)
1303:i
1300:,
1296:)
1292:m
1289:,
1284:0
1280:x
1275:(
1267:(
1240:1
1237:+
1234:m
1228:)
1225:1
1222:+
1219:i
1216:(
1213:=
1208:i
1204:m
1183:n
1177:i
1142:)
1138:1
1135:+
1132:m
1125:)
1121:1
1118:+
1115:i
1111:(
1107:,
1102:0
1098:x
1093:(
1088:m
1085:e
1082:r
1078:=
1074:)
1070:i
1067:,
1063:)
1059:m
1056:,
1051:0
1047:x
1042:(
1034:(
975:)
971:1
968:+
964:)
961:s
958:(
954:L
947:)
943:1
940:+
937:i
933:(
929:,
925:)
922:s
919:(
915:K
911:(
906:m
903:e
900:r
896:=
893:)
890:i
887:,
884:s
881:(
815:1
812:=
809:)
806:2
803:,
800:7
797:(
793:m
790:e
787:r
765:2
762:=
759:)
756:3
753:,
750:5
747:(
743:m
740:e
737:r
701:y
698:=
694:)
689:)
685:y
682:,
679:x
675:(
667:(
663:L
642:x
639:=
635:)
630:)
626:y
623:,
620:x
616:(
608:(
604:K
583:L
579:K
517:i
513:a
509:=
506:)
503:i
500:,
497:a
494:(
481:a
462:1
456:n
452:a
445:,
440:0
436:a
422:n
418:n
322:i
318:a
314:=
311:)
308:i
305:,
302:a
299:(
296:f
276:1
270:n
264:i
258:0
248:i
244:a
225:1
219:n
215:a
208:,
203:0
199:a
185:n
181:n
177:f
72:)
66:(
61:)
57:(
46:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.