17:
5224:
1639:. This formula is indeed equivalent to φ because it states that for every x, if there is a y that satisfies Q'(x,y), then (something) holds, and furthermore, we know that there is such a y, because for every x', there is a y' that satisfies Q'(x',y'). Therefore φ follows from this formula. It is also easy to show that if the formula is false, then so is φ.
1186:
5645:
3606:
4863:
2723:
is a string of quantifiers containing all quantifiers in (S) and (S') interleaved among themselves in any fashion, but maintaining the relative order inside (S) and (S'), will be equivalent to the original formula Φ'(this is yet another basic result in first-order predicate calculus that we rely on).
2594:
1637:
32:
in his doctoral dissertation of 1929 (and a shorter version of the proof, published as an article in 1930, titled "The completeness of the axioms of the functional calculus of logic" (in German)) is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that
3144:
This is yet another basic result of first-order predicate calculus. Depending on the particular formalism adopted for the calculus, it may be seen as a simple application of a "functional substitution" rule of inference, as in Gödel's paper, or it may be proved by considering the formal proof of
355:
This is the most basic form of the completeness theorem. We immediately restate it in a form more convenient for our purposes: When we say "all structures", it is important to specify that the structures involved are classical (Tarskian) interpretations I, where I = <U,F> (U is a
2900:
2169:
444:
There are standard techniques for rewriting an arbitrary formula into one that does not use function or constant symbols, at the cost of introducing additional quantifiers; we will therefore assume that all formulas are free of such symbols. Gödel's paper uses a version of first-order predicate
412:
by successively restricting the class of all formulas φ for which we need to prove "φ is either refutable or satisfiable". At the beginning we need to prove this for all possible formulas φ in our language. However, suppose that for every formula φ there is some formula ψ taken from a more
931:
5363:
5219:{\displaystyle D_{n}\Leftarrow D_{n-1}\wedge (\forall z_{1}\ldots z_{(n-1)m+1})(\exists z_{(n-1)m+2}\ldots z_{nm+1})B_{n}\Leftarrow D_{n-1}\wedge (\forall z_{a_{1}^{n}}\ldots z_{a_{k}^{n}})(\exists y_{1}\ldots y_{m})\varphi (z_{a_{1}^{n}}\ldots z_{a_{k}^{n}},y_{1}\ldots y_{m})}
417:, such that "ψ is either refutable or satisfiable" → "φ is either refutable or satisfiable". Then, once this claim (expressed in the previous sentence) is proved, it will suffice to prove "φ is either refutable or satisfiable" only for φ's belonging to the class
7971:
Gödel also considered the case where there are a countably infinite collection of formulas. Using the same reductions as above, he was able to consider only those cases where each formula is of degree 1 and contains no uses of equality. For a countable collection of formulas
2408:
3370:
3970:
55:
We fix some axiomatization (i.e. a syntax-based, machine-manageable proof system) of the predicate calculus: logical axioms and rules of inference. Any of the several well-known equivalent axiomatizations will do. Gödel's original proof assumed the
3168:, replacing in it all occurrences of Q by some other formula with the same free variables, and noting that all logical axioms in the formal proof remain logical axioms after the substitution, and all rules of inference still apply in the same way.
4666:
6656:
4805:
82:), i.e. there are no special axioms expressing the properties of (object) equality as a special relation symbol. After the basic form of the theorem has been proved, it will be easy to extend it to the case of predicate calculus
3034:
4161:
4259:
1738:
1381:
1181:{\displaystyle \varphi =(\forall x_{1}\cdots \forall x_{k_{1}})(\exists x_{k_{1}+1}\cdots \exists x_{k_{2}})\cdots (\forall x_{k_{n-2}+1}\cdots \forall x_{k_{n-1}})(\exists x_{k_{n-1}+1}\cdots \exists x_{k_{n}})(\Phi )}
8148:
653:
5640:{\displaystyle D_{1}\equiv (\exists z_{1}\ldots z_{m+1})\varphi (z_{a_{1}^{1}}\ldots z_{a_{k}^{1}},z_{2},z_{3}\ldots z_{m+1})\equiv (\exists z_{1}\ldots z_{m+1})\varphi (z_{1}\ldots z_{1},z_{2},z_{3}\ldots z_{m+1})}
3785:
3284:
7030:
Gödel reduced a formula containing instances of the equality predicate to ones without it in an extended language. His method involves replacing a formula φ containing some instances of equality with the formula
49:. Our languages allow constant, function and relation symbols. Structures consist of (non-empty) domains and interpretations of the relevant symbols as constant members, functions or relations over that domain.
7959:. If this new formula is refutable, the original φ was as well; the same is true of satisfiability, since we may take a quotient of satisfying model of the new formula by the equivalence relation representing
5319:
576:
1920:
7848:
7578:
2419:
2730:
1999:
4063:
816:
7190:
1463:
881:
3601:{\displaystyle \neg ((\forall x')(\exists y')(\forall u)(\exists v)(P)\psi (x,y\mid x',y')\wedge (\forall x)(\forall y)((\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P)\psi ))}
2651:
2267:
6503:
917:
Our generic formula φ now is a sentence, in normal form, and its prefix starts with a universal quantifier and ends with an existential quantifier. Let us call the class of all such formulas
296:
is either refutable (its negation is always true) or satisfiable, i.e. there is some model in which it holds (it might even be always true, i.e. a tautology); this model is simply assigning
4417:
3337:
2717:
4473:
3833:
4848:
2251:
2198:
33:
is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of
2934:
7314:
7605:
6440:
4305:
1960:
7898:
4357:
5355:
907:
3688:
7997:
4508:
1861:
3362:
3194:
3166:
3140:
3117:
8029:
7953:
7927:
3054:
1809:
1765:
1430:
1410:
1257:
1233:
1213:
7869:
7335:
6113:
3649:
3629:
3286:. Here (x,y | x',y') means that instead of ψ we are writing a different formula, in which x and y are replaced with x' and y'. Q(x,y) is simply replaced by
8056:
6683:
6530:
6394:
6370:
6340:
6309:
6282:
6251:
6224:
6197:
6170:
6140:
6080:
6049:
6022:
5995:
5968:
5941:
5914:
5887:
5860:
5826:
5799:
5772:
5745:
5710:
5679:
4693:
4503:
3805:
3094:
3074:
2981:
2957:
1789:
6538:
4701:
396:
holds and φ is valid in all structures, then ¬φ is not satisfiable in any structure and therefore refutable; then ¬¬φ is provable and then so is φ, thus
3827:
of degree 1. φ cannot be of degree 0, since formulas in R have no free variables and don't use constant symbols. So the formula φ has the general form:
4068:
2990:
4166:
1660:
1303:
5943:; we will inductively define a general assignment to them by a sort of "majority vote": Since there are infinitely many assignments (one for each
8061:
597:
213:. While we cannot do this by simply rearranging the quantifiers, we show that it is yet enough to prove the theorem for sentences of that form.
8244:
5229:
2413:
And since these two formulas are equivalent, if we replace the first with the second inside Φ, we obtain the formula Φ' such that Φ≡Φ':
2589:{\displaystyle \Phi '=(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )}
356:
non-empty (possibly infinite) set of objects, whereas F is a set of functions from expressions of the interpreted symbolism into U).
8234:
The same material as the dissertation, except with briefer proofs, more succinct explanations, and omitting the lengthy introduction.
2895:{\displaystyle \Psi =(\forall x')(\forall x)(\forall y)(\forall u)(\exists y')(\exists v)(P)Q(x',y')\wedge (Q(x,y)\rightarrow \psi )}
2164:{\displaystyle \Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )}
526:
388:
holds, and φ is not satisfiable in any structure, then ¬φ is valid in all structures and therefore provable, thus φ is refutable and
25:
1866:
686:, which is in normal form) begin with a universal quantifier and end with an existential quantifier. To achieve this for a generic
7611:
7341:
3700:
3199:
1436: − 1). φ states that for every x there is a y such that... (something). It would have been nice to have a predicate
1643:, in general there is no such predicate Q'. However, this idea can be understood as a basis for the following proof of the Lemma.
1632:{\displaystyle (\forall x')(\forall x)(\forall y)(\forall u)(\exists v)(\exists y')(P)Q'(x',y')\wedge (Q'(x,y)\rightarrow \psi )}
3990:
1236:
8299:
3690:
is provable, and φ is refutable. We have proved that φ is either satisfiable or refutable, and this concludes the proof of the
729:
7037:
1215:
to be the number of universal quantifier blocks, separated by existential quantifier blocks as shown above, in the prefix of
46:
821:
6372:
true, we construct an interpretation of the language's predicates that makes φ true. The universe of the model will be the
2403:{\displaystyle (Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )\equiv (\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )}
7963:. This quotient is well-defined with respect to the other predicates, and therefore will satisfy the original formula φ.
925:
is either refutable or satisfiable. Given our formula φ, we group strings of quantifiers of one kind together in blocks:
8284:
8289:
8171:
6445:
5828:
will be true when each proposition is evaluated in this fashion. This follows from the completeness of the underlying
7955:
their respective arities), and φ' is the formula φ with all occurrences of equality replaced with the new predicate
4366:
3965:{\displaystyle (\forall x_{1}\ldots x_{k})(\exists y_{1}\ldots y_{m})\varphi (x_{1}\ldots x_{k},y_{1}\ldots y_{m}).}
3289:
121:. This is possible because for every sentence, there is an equivalent one in prenex form whose first quantifier is
4422:
4820:
3811:
in that case. This is why we cannot naively use the argument appearing at the comment that precedes the proof.
2602:
2206:
2177:
5226:, where the latter implication holds by variable substitution, since the ordering of the tuples is such that
2676:
8304:
7194:
7584:
6024:
true, or infinitely many make it false and only finitely many make it true. In the former case, we choose
6399:
4264:
8294:
8279:
8259:
8170:. Other approaches can be used to prove that the completeness theorem in this case is equivalent to the
8167:
6505:
is either true in the general assignment, or not assigned by it (because it never appears in any of the
2908:
1925:
63:
We assume without proof all the basic well-known results about our formalism that we need, such as the
8166:
the formulas, and prove the uncountable case with the same argument as the countable one, except with
6051:
to be true in general; in the latter we take it to be false in general. Then from the infinitely many
4310:
5324:
4661:{\displaystyle \varphi (z_{a_{1}^{n}}\ldots z_{a_{k}^{n}},z_{(n-1)m+2},z_{(n-1)m+3}\ldots z_{nm+1})}
886:
5829:
4360:
3808:
3670:
301:
7975:
3142:
by some other formula dependent on the same variables, and we will still get a provable formula. (
16:
8225:
1837:
106:
64:
34:
7875:
6115:
are assigned the same truth value as in the general assignment, we pick a general assignment to
3344:
3176:
3148:
3122:
3099:
2261:, the following equivalence is easily provable with the help of whatever formalism we're using:
433:) is provable), then it is indeed the case that "ψ is either refutable or satisfiable" → "
8002:
7932:
7906:
3039:
1794:
1750:
1415:
1386:
1242:
1218:
1198:
438:
68:
7854:
7320:
6085:
3634:
3614:
1985:
be a previously unused relation symbol that takes as many arguments as the sum of lengths of
1456:
is the required one to make (something) true. Then we could have written a formula of degree
8252:
8217:
8209:
6651:{\displaystyle (\exists y_{1}\ldots y_{m})\varphi (a_{1}^{n}\ldots a_{k}^{n},y_{1}...y_{m})}
4800:{\displaystyle (\exists z_{1}\ldots z_{nm+1})(B_{1}\wedge B_{2}\wedge \cdots \wedge B_{n}).}
94:
In the following, we state two equivalent forms of the theorem, and show their equivalence.
8034:
6685:
range over all possible k-tuples of natural numbers. So φ is satisfiable, and we are done.
6661:
6508:
6379:
6348:
6318:
6287:
6260:
6229:
6202:
6175:
6148:
6118:
6058:
6027:
6000:
5973:
5946:
5919:
5892:
5865:
5838:
5804:
5777:
5750:
5723:
5688:
5657:
4671:
4481:
3790:
3079:
3059:
2966:
2942:
1774:
8221:
8159:
6373:
300:
to the subpropositions from which B is built. The reason for that is the completeness of
690:(subject to restrictions we have already proved), we take some one-place relation symbol
6658:
is true by construction. But this implies that φ itself is true in the model, since the
8274:
3984:
57:
8268:
8229:
8197:
8184:
360:
Theorem 2. Every formula φ is either refutable or satisfiable in some structure.
29:
5774:; "distinct" here means either distinct predicates, or distinct bound variables) in
117:) at the beginning. Furthermore, we reduce it to formulas whose first quantifier is
4419:
denotes the sum of the terms of the tuple.] Denote the nth tuple in this order by
3119:
is provable. Now we can replace all occurrences of Q inside the provable formula
4156:{\displaystyle \Sigma _{k}(x_{1}\ldots x_{k})<\Sigma _{k}(y_{1}\ldots y_{k})}
453:
297:
102:
8163:
3029:{\displaystyle \Psi \equiv \Phi '\equiv \Phi \wedge \Phi \rightarrow \varphi }
4254:{\displaystyle \Sigma _{k}(x_{1}\ldots x_{k})=\Sigma _{k}(y_{1}\ldots y_{k})}
1733:{\displaystyle \varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi }
1376:{\displaystyle \varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi }
8248:
5720:
there is some way of assigning truth values to the distinct subpropositions
52:
We assume classical logic (as opposed to intuitionistic logic for example).
8143:{\displaystyle B_{1}^{1}\ldots B_{k}^{1},\ldots ,B_{1}^{k}\ldots B_{k}^{k}}
8200:(1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls".
6257:. But this contradicts the fact that for the finite collection of general
3611:
and this formula is provable; since the part under negation and after the
328:, or all of them are not refutable and therefore each holds in some model.
8162:(or at least some weak form of it) is needed. Using the full AC, one can
648:{\displaystyle \neg \psi =\forall x_{1}\cdots \forall x_{n}\neg \varphi }
37:. This outline should not be considered a rigorous proof of the theorem.
340:
hold (in case all are not refutable) in order to build a model in which
8213:
3631:
sign is obviously provable, and the part under negation and before the
674:
Finally, we would like, for reasons of technical convenience, that the
101:
Reducing the theorem to sentences (formulas with no free variables) in
1235:. The following lemma, which Gödel adapted from Skolem's proof of the
307:
We extend this result to more and more complex and lengthy sentences,
5835:
We will now show that there is such an assignment of truth values to
351:
Theorem 1. Every valid formula (true in all structures) is provable.
8158:
When there is an uncountably infinite collection of formulas, the
5685:, it follows that φ is refutable. On the other hand, suppose that
5314:{\displaystyle (\forall k)(a_{1}^{n}\ldots a_{k}^{n})<(n-1)m+2}
3980:
452:(which no longer uses function or constant symbols) and apply the
97:
Later, we prove the theorem. This is done in the following steps:
15:
445:
calculus that has no function or constant symbols to begin with.
2963:
and therefore by assumption either refutable or satisfiable. If
2661:
are some quantifier strings, ρ and ρ' are quantifier-free, and,
1277:
is either refutable or satisfiable, then so is every formula in
1973:
be tuples of previously unused variables of the same length as
1239:, lets us sharply reduce the complexity of the generic formula
571:{\displaystyle \psi =\exists x_{1}\cdots \exists x_{n}\varphi }
1915:{\displaystyle \forall x_{1}\forall x_{2}\cdots \forall x_{n}}
324:, so that either any of them is refutable and therefore so is
7843:{\displaystyle (\forall x_{1}\ldots x_{m},y_{1}\ldots x_{m})}
7573:{\displaystyle (\forall x_{1}\ldots x_{k},y_{1}\ldots x_{k})}
3780:{\displaystyle (\forall u)(\exists v)(P)\psi (x,y\mid x',y')}
3279:{\displaystyle (\forall u)(\exists v)(P)\psi (x,y\mid x',y')}
2673:
occurs in ρ. Under such conditions every formula of the form
3823:
above, we only need to prove our theorem for formulas φ in
8150:. The remainder of the proof then went through as before.
4058:{\displaystyle (x_{1}\ldots x_{k})<(y_{1}\ldots y_{k})}
7026:
Extension to first-order predicate calculus with equality
811:{\displaystyle \psi =\forall y(P)\exists z(\Phi \wedge )}
216:
Finally we prove the theorem for sentences of that form.
7185:{\displaystyle (\forall x)Eq(x,x)\wedge (\forall x,y,z)}
682:(that is, the string of quantifiers at the beginning of
484:, if there are any, are found at the very beginning of
6145:
This general assignment must lead to every one of the
876:{\displaystyle \forall y\exists z(F(y)\vee \neg F(z))}
8064:
8037:
8005:
7978:
7935:
7909:
7878:
7857:
7614:
7587:
7344:
7323:
7197:
7040:
6664:
6541:
6511:
6448:
6402:
6382:
6351:
6345:
From this general assignment, which makes all of the
6321:
6290:
6263:
6232:
6205:
6178:
6151:
6121:
6088:
6061:
6030:
6003:
5976:
5949:
5922:
5895:
5868:
5841:
5807:
5780:
5753:
5726:
5691:
5660:
5366:
5327:
5232:
4866:
4823:
4704:
4674:
4511:
4484:
4425:
4369:
4313:
4267:
4169:
4071:
3993:
3836:
3793:
3703:
3673:
3637:
3617:
3373:
3347:
3292:
3202:
3179:
3151:
3125:
3102:
3082:
3062:
3042:
2993:
2969:
2945:
2911:
2733:
2679:
2605:
2422:
2270:
2209:
2180:
2002:
1928:
1869:
1840:
1797:
1777:
1753:
1663:
1466:
1418:
1389:
1306:
1245:
1221:
1201:
934:
889:
824:
732:
600:
529:
219:
This is done by first noting that a sentence such as
304:, with the existential quantifiers playing no role.
8142:
8050:
8023:
7991:
7947:
7921:
7892:
7863:
7842:
7599:
7572:
7329:
7308:
7184:
6999:) satisfied. By taking a submodel with only these
6677:
6650:
6524:
6497:
6434:
6388:
6364:
6334:
6303:
6276:
6245:
6218:
6191:
6164:
6134:
6107:
6074:
6043:
6016:
5989:
5962:
5935:
5908:
5881:
5854:
5820:
5793:
5766:
5739:
5704:
5673:
5639:
5349:
5313:
5218:
4842:
4799:
4687:
4660:
4497:
4467:
4411:
4351:
4299:
4253:
4155:
4057:
3964:
3799:
3779:
3682:
3643:
3623:
3600:
3356:
3331:
3278:
3188:
3160:
3134:
3111:
3088:
3068:
3048:
3028:
2975:
2951:
2928:
2894:
2711:
2645:
2588:
2402:
2245:
2192:
2163:
1954:
1914:
1855:
1803:
1783:
1759:
1732:
1631:
1424:
1404:
1375:
1251:
1227:
1207:
1180:
921:. We are faced with proving that every formula in
901:
875:
810:
647:
570:
6498:{\displaystyle \Psi (z_{u_{1}}\ldots z_{u_{i}})}
3787:instead of Q(x',y') from the beginning, because
3173:In this particular case, we replace Q(x',y') in
8191:(Doctoral dissertation). University Of Vienna.
6812:has the property that the "last arguments" of
5647:is obviously a corollary of φ as well. So the
4412:{\displaystyle \Sigma _{k}(x_{1}\ldots x_{k})}
3332:{\displaystyle (\forall u)(\exists v)(P)\psi }
128:Reducing the theorem to sentences of the form
7013:... objects, we have a model satisfying
6882:of these appear as "first arguments" in some
671:, that is, a formula with no free variables.
8:
8193:The first proof of the completeness theorem.
6855:Therefore in a model that satisfies all the
6784:so that they appear as "first arguments" in
3815:Proving the theorem for formulas of degree 1
913:Reducing the theorem to formulas of degree 1
883:is clearly provable, it is easy to see that
503:by quantifying them existentially: if, say,
7929:denote the predicates appearing in φ (with
6738:s, which we may call "first arguments" and
4468:{\displaystyle (a_{1}^{n}\ldots a_{k}^{n})}
1831:of variables rather than single variables;
499:Next, we eliminate all free variables from
6819:appear, in every possible combinations of
663:is refutable. We see that we can restrict
488:). It follows now that we need only prove
8189:Über die Vollständigkeit des Logikkalküls
8134:
8129:
8116:
8111:
8092:
8087:
8074:
8069:
8063:
8042:
8036:
8015:
8010:
8004:
7983:
7977:
7934:
7908:
7877:
7856:
7825:
7812:
7790:
7777:
7749:
7736:
7705:
7692:
7664:
7651:
7638:
7625:
7613:
7586:
7555:
7542:
7520:
7507:
7479:
7466:
7435:
7422:
7394:
7381:
7368:
7355:
7343:
7322:
7196:
7039:
6669:
6663:
6639:
6620:
6607:
6602:
6589:
6584:
6565:
6552:
6540:
6516:
6510:
6484:
6479:
6464:
6459:
6447:
6423:
6410:
6401:
6381:
6356:
6350:
6326:
6320:
6295:
6289:
6268:
6262:
6237:
6231:
6226:were false under the general assignment,
6210:
6204:
6183:
6177:
6156:
6150:
6126:
6120:
6093:
6087:
6066:
6060:
6035:
6029:
6008:
6002:
5981:
5975:
5954:
5948:
5927:
5921:
5900:
5894:
5873:
5867:
5846:
5840:
5812:
5806:
5785:
5779:
5758:
5752:
5731:
5725:
5696:
5690:
5665:
5659:
5622:
5609:
5596:
5583:
5570:
5545:
5532:
5504:
5491:
5478:
5463:
5458:
5453:
5438:
5433:
5428:
5403:
5390:
5371:
5365:
5332:
5326:
5275:
5270:
5257:
5252:
5231:
5207:
5194:
5179:
5174:
5169:
5154:
5149:
5144:
5125:
5112:
5091:
5086:
5081:
5066:
5061:
5056:
5031:
5018:
4996:
4962:
4922:
4909:
4884:
4871:
4865:
4843:{\displaystyle \varphi \rightarrow D_{n}}
4834:
4822:
4785:
4766:
4753:
4728:
4715:
4703:
4679:
4673:
4640:
4606:
4572:
4557:
4552:
4547:
4532:
4527:
4522:
4510:
4489:
4483:
4456:
4451:
4438:
4433:
4424:
4400:
4387:
4374:
4368:
4340:
4321:
4312:
4288:
4275:
4266:
4242:
4229:
4216:
4200:
4187:
4174:
4168:
4144:
4131:
4118:
4102:
4089:
4076:
4070:
4046:
4033:
4014:
4001:
3992:
3950:
3937:
3924:
3911:
3892:
3879:
3860:
3847:
3835:
3792:
3702:
3672:
3636:
3616:
3372:
3346:
3291:
3201:
3178:
3150:
3124:
3101:
3081:
3061:
3041:
2992:
2968:
2944:
2910:
2732:
2678:
2646:{\displaystyle (S)\rho \wedge (S')\rho '}
2604:
2421:
2269:
2246:{\displaystyle (\forall u)(\exists v)(P)}
2208:
2193:{\displaystyle \Phi \rightarrow \varphi }
2179:
2001:
1946:
1933:
1927:
1906:
1890:
1877:
1868:
1839:
1796:
1776:
1752:
1662:
1465:
1417:
1388:
1305:
1244:
1220:
1200:
1158:
1153:
1123:
1118:
1091:
1086:
1056:
1051:
1027:
1022:
998:
993:
972:
967:
951:
933:
888:
823:
731:
633:
617:
599:
559:
543:
528:
437:is either refutable or satisfiable" (the
6776:, and for every possible combination of
5321:. But the last formula is equivalent to
1654: + 1; then we can write it as
1460:, which is equivalent to φ, namely
722:(the remaining, quantifier-free part of
8154:Extension to arbitrary sets of formulas
7967:Extension to countable sets of formulas
6823:of them, as "first arguments" in other
2712:{\displaystyle (T)(\rho \wedge \rho ')}
331:We finally use the models in which the
7309:{\displaystyle \wedge (\forall x,y,z)}
6864:s, there are objects corresponding to
6752:for example. Its "last arguments" are
5747:(ordered by their first appearance in
90:Statement of the theorem and its proof
7600:{\displaystyle \wedge \cdots \wedge }
6742:s that we may call "last arguments".
6342:true matches the general assignment.
714:, where (P) stands for the prefix of
320: = 1,2...), built out from
7:
6535:In this model, each of the formulas
2203:Now since the string of quantifiers
1269: ≥ 1. If every formula in
421:. If φ is provably equivalent to ψ (
8245:Stanford Encyclopedia of Philosophy
6435:{\displaystyle (u_{1}\ldots u_{i})}
4300:{\displaystyle (x_{1}\ldots x_{k})}
3697:Notice that we could not have used
448:Next we consider a generic formula
7618:
7348:
7204:
7080:
7044:
6545:
6449:
6383:
5916:appear in the same order in every
5525:
5383:
5236:
5105:
5049:
4955:
4902:
4708:
4371:
4213:
4171:
4115:
4073:
3872:
3840:
3794:
3719:
3707:
3674:
3571:
3559:
3532:
3520:
3505:
3493:
3429:
3417:
3400:
3383:
3374:
3351:
3348:
3308:
3296:
3218:
3206:
3183:
3180:
3155:
3152:
3129:
3126:
3106:
3103:
3096:, which is equivalent to it; thus
3083:
3063:
3017:
3011:
3001:
2994:
2970:
2946:
2929:{\displaystyle \Phi '\equiv \Psi }
2923:
2913:
2813:
2796:
2784:
2772:
2760:
2743:
2734:
2538:
2526:
2514:
2502:
2454:
2437:
2424:
2352:
2340:
2310:
2298:
2225:
2213:
2181:
2137:
2125:
2089:
2077:
2029:
2012:
2003:
1899:
1883:
1870:
1844:
1747:is the remainder of the prefix of
1709:
1697:
1685:
1673:
1535:
1523:
1511:
1499:
1487:
1470:
1352:
1340:
1328:
1316:
1259:we need to prove the theorem for:
1172:
1146:
1111:
1079:
1044:
1015:
986:
960:
944:
855:
831:
825:
787:
763:
754:
739:
639:
626:
610:
601:
552:
536:
480:means that all the quantifiers in
14:
6852:with the corresponding property.
6780:of these variables there is some
3975:Now we define an ordering of the
1955:{\displaystyle x_{1}\ldots x_{n}}
1791:is the quantifier-free matrix of
74:We axiomatize predicate calculus
6199:being true, since if one of the
2669:occurs in ρ' and no variable of
2253:does not contain variables from
6442:precisely when the proposition
6396:should be true of the naturals
4352:{\displaystyle (y_{1}...y_{k})}
3651:sign is obviously φ, just with
1452:) would be true if and only if
7837:
7834:
7831:
7805:
7796:
7770:
7764:
7761:
7758:
7755:
7729:
7711:
7685:
7676:
7673:
7670:
7615:
7567:
7564:
7561:
7535:
7526:
7500:
7494:
7491:
7488:
7485:
7459:
7441:
7415:
7406:
7403:
7400:
7345:
7303:
7300:
7297:
7285:
7276:
7273:
7261:
7252:
7249:
7246:
7234:
7225:
7222:
7201:
7179:
7176:
7173:
7161:
7152:
7149:
7137:
7128:
7125:
7122:
7110:
7101:
7098:
7077:
7071:
7059:
7050:
7041:
6645:
6577:
6571:
6542:
6492:
6452:
6429:
6403:
6253:would also be false for every
5997:, either infinitely many make
5634:
5563:
5557:
5522:
5516:
5421:
5415:
5380:
5350:{\displaystyle D_{n-1}\wedge }
5299:
5287:
5281:
5245:
5242:
5233:
5213:
5137:
5131:
5102:
5099:
5046:
5024:
5011:
4975:
4963:
4952:
4949:
4935:
4923:
4899:
4877:
4827:
4791:
4746:
4743:
4705:
4655:
4619:
4607:
4585:
4573:
4515:
4462:
4426:
4406:
4380:
4346:
4314:
4294:
4268:
4248:
4222:
4206:
4180:
4150:
4124:
4108:
4082:
4052:
4026:
4020:
3994:
3956:
3904:
3898:
3869:
3866:
3837:
3774:
3740:
3734:
3728:
3725:
3716:
3713:
3704:
3595:
3592:
3586:
3580:
3577:
3568:
3565:
3556:
3553:
3547:
3541:
3538:
3529:
3526:
3517:
3514:
3511:
3502:
3499:
3490:
3484:
3450:
3444:
3438:
3435:
3426:
3423:
3414:
3411:
3397:
3394:
3380:
3377:
3323:
3317:
3314:
3305:
3302:
3293:
3273:
3239:
3233:
3227:
3224:
3215:
3212:
3203:
3020:
2983:is satisfiable in a structure
2889:
2883:
2880:
2868:
2862:
2856:
2834:
2828:
2822:
2819:
2810:
2807:
2793:
2790:
2781:
2778:
2769:
2766:
2757:
2754:
2740:
2724:To wit, we form Ψ as follows:
2706:
2689:
2686:
2680:
2632:
2621:
2612:
2606:
2583:
2577:
2574:
2562:
2556:
2553:
2547:
2544:
2535:
2532:
2523:
2520:
2511:
2508:
2499:
2493:
2471:
2465:
2451:
2448:
2434:
2397:
2391:
2388:
2376:
2370:
2367:
2361:
2358:
2349:
2346:
2337:
2331:
2325:
2319:
2316:
2307:
2304:
2295:
2292:
2289:
2277:
2271:
2240:
2234:
2231:
2222:
2219:
2210:
2184:
2158:
2152:
2146:
2143:
2134:
2131:
2122:
2119:
2116:
2104:
2098:
2095:
2086:
2083:
2074:
2068:
2046:
2040:
2026:
2023:
2009:
1850:
1841:
1724:
1718:
1715:
1706:
1703:
1694:
1691:
1682:
1679:
1670:
1626:
1620:
1617:
1605:
1594:
1588:
1566:
1555:
1549:
1546:
1532:
1529:
1520:
1517:
1508:
1505:
1496:
1493:
1484:
1481:
1467:
1396:
1390:
1367:
1361:
1358:
1349:
1346:
1337:
1334:
1325:
1322:
1313:
1175:
1169:
1166:
1108:
1105:
1041:
1035:
983:
980:
941:
902:{\displaystyle \varphi =\psi }
870:
867:
861:
849:
843:
837:
805:
802:
799:
793:
781:
775:
769:
760:
751:
745:
582:is satisfiable in a structure
404:Proof of theorem 2: first step
78:(sometimes confusingly called
58:Hilbert-Ackermann proof system
47:first-order predicate calculus
1:
3683:{\displaystyle \neg \varphi }
1962:are some distinct variables.
1650:Let φ be a formula of degree
655:is provable, and then so is ¬
413:restricted class of formulas
7992:{\displaystyle \varphi ^{i}}
6878:... and each combination of
6315:where the assignment making
6311:, there are infinitely many
392:holds. If on the other hand
380:Equivalence of both theorems
26:Gödel's completeness theorem
8172:Boolean prime ideal theorem
7999:of degree 1, we may define
3056:is satisfiable as well. If
1856:{\displaystyle (\forall x)}
1300: + 1 of the form
8321:
8202:Monatshefte für Mathematik
7893:{\displaystyle \varphi '.}
3357:{\displaystyle \neg \Phi }
3189:{\displaystyle \neg \Phi }
3161:{\displaystyle \neg \Phi }
3135:{\displaystyle \neg \Phi }
3112:{\displaystyle \neg \Phi }
1993:; we consider the formula
456:theorem to find a formula
8024:{\displaystyle B_{k}^{i}}
7948:{\displaystyle k\ldots m}
7922:{\displaystyle A\ldots Z}
6891:, meaning that for every
6284:assignments appearing in
5712:is not refutable for any
3076:is refutable, then so is
441:is needed to show this).
408:We approach the proof of
6793:. Thus for large enough
3049:{\displaystyle \varphi }
1804:{\displaystyle \varphi }
1760:{\displaystyle \varphi }
1425:{\displaystyle \varphi }
1405:{\displaystyle (P)\psi }
1252:{\displaystyle \varphi }
1237:Löwenheim–Skolem theorem
1228:{\displaystyle \varphi }
1208:{\displaystyle \varphi }
698:, and two new variables
7864:{\displaystyle \wedge }
7330:{\displaystyle \wedge }
6376:. Each i-ary predicate
6108:{\displaystyle E_{h-1}}
3644:{\displaystyle \wedge }
3624:{\displaystyle \wedge }
2959:is a formula of degree
586:, then certainly so is
8144:
8052:
8031:as above; then define
8025:
7993:
7949:
7923:
7894:
7865:
7844:
7601:
7574:
7331:
7310:
7186:
6679:
6652:
6526:
6499:
6436:
6390:
6366:
6336:
6305:
6278:
6247:
6220:
6193:
6166:
6136:
6109:
6076:
6045:
6018:
5991:
5964:
5937:
5910:
5883:
5856:
5822:
5795:
5768:
5741:
5706:
5681:is refutable for some
5675:
5641:
5351:
5315:
5220:
4844:
4801:
4689:
4662:
4499:
4469:
4413:
4353:
4301:
4255:
4157:
4065:should hold if either
4059:
3966:
3807:would not have been a
3801:
3781:
3684:
3645:
3625:
3602:
3358:
3333:
3280:
3190:
3162:
3136:
3113:
3090:
3070:
3050:
3030:
2977:
2953:
2930:
2896:
2713:
2647:
2590:
2404:
2247:
2194:
2165:
1981:respectively, and let
1956:
1916:
1857:
1805:
1785:
1767:(it is thus of degree
1761:
1734:
1633:
1432:(it is thus of degree
1426:
1406:
1377:
1253:
1229:
1209:
1182:
903:
877:
812:
649:
572:
167: ... ∃
144: ... ∀
21:
8174:, a weak form of AC.
8168:transfinite induction
8145:
8058:to be the closure of
8053:
8051:{\displaystyle D_{k}}
8026:
7994:
7950:
7924:
7895:
7866:
7845:
7602:
7575:
7332:
7311:
7187:
6689:Intuitive explanation
6680:
6678:{\displaystyle a^{n}}
6653:
6527:
6525:{\displaystyle D_{k}}
6500:
6437:
6391:
6389:{\displaystyle \Psi }
6367:
6365:{\displaystyle D_{k}}
6337:
6335:{\displaystyle D_{n}}
6306:
6304:{\displaystyle D_{k}}
6279:
6277:{\displaystyle E_{h}}
6248:
6246:{\displaystyle D_{n}}
6221:
6219:{\displaystyle B_{k}}
6194:
6192:{\displaystyle D_{k}}
6167:
6165:{\displaystyle B_{k}}
6142:in the same fashion.
6137:
6135:{\displaystyle E_{h}}
6110:
6077:
6075:{\displaystyle E_{1}}
6046:
6044:{\displaystyle E_{1}}
6019:
6017:{\displaystyle E_{1}}
5992:
5990:{\displaystyle E_{1}}
5965:
5963:{\displaystyle D_{n}}
5938:
5936:{\displaystyle D_{n}}
5911:
5909:{\displaystyle E_{h}}
5884:
5882:{\displaystyle D_{n}}
5857:
5855:{\displaystyle E_{h}}
5823:
5821:{\displaystyle D_{n}}
5796:
5794:{\displaystyle B_{k}}
5769:
5767:{\displaystyle D_{n}}
5742:
5740:{\displaystyle E_{h}}
5707:
5705:{\displaystyle D_{n}}
5676:
5674:{\displaystyle D_{n}}
5642:
5352:
5316:
5221:
4845:
4802:
4690:
4688:{\displaystyle D_{n}}
4663:
4500:
4498:{\displaystyle B_{n}}
4470:
4414:
4354:
4302:
4256:
4158:
4060:
3967:
3802:
3800:{\displaystyle \Psi }
3782:
3685:
3646:
3626:
3603:
3359:
3334:
3281:
3191:
3163:
3137:
3114:
3091:
3089:{\displaystyle \Phi }
3071:
3069:{\displaystyle \Psi }
3051:
3031:
2978:
2976:{\displaystyle \Psi }
2954:
2952:{\displaystyle \Psi }
2931:
2897:
2714:
2648:
2591:
2405:
2248:
2195:
2166:
1957:
1917:
1858:
1806:
1786:
1784:{\displaystyle \psi }
1762:
1735:
1634:
1440:so that for every x,
1427:
1407:
1378:
1254:
1230:
1210:
1183:
904:
878:
813:
650:
573:
19:
8258:MacTutor biography:
8062:
8035:
8003:
7976:
7933:
7907:
7876:
7855:
7612:
7585:
7342:
7321:
7195:
7038:
6662:
6539:
6509:
6446:
6400:
6380:
6349:
6319:
6288:
6261:
6230:
6203:
6176:
6149:
6119:
6086:
6059:
6028:
6001:
5974:
5947:
5920:
5893:
5866:
5839:
5805:
5778:
5751:
5724:
5689:
5658:
5364:
5325:
5230:
4864:
4821:
4702:
4672:
4509:
4482:
4423:
4367:
4311:
4265:
4167:
4069:
3991:
3834:
3791:
3701:
3671:
3635:
3615:
3371:
3345:
3290:
3200:
3177:
3149:
3123:
3100:
3080:
3060:
3040:
2991:
2987:, then, considering
2967:
2943:
2909:
2731:
2677:
2603:
2599:Now Φ' has the form
2420:
2268:
2207:
2178:
2000:
1926:
1867:
1838:
1795:
1775:
1771: – 1) and
1751:
1661:
1464:
1416:
1412:is the remainder of
1387:
1304:
1243:
1219:
1199:
932:
887:
822:
730:
598:
527:
368:is refutable" means
8300:Works by Kurt Gödel
8285:Mathematical proofs
8139:
8121:
8097:
8079:
8020:
6612:
6594:
5830:propositional logic
5468:
5443:
5360:For the base case,
5280:
5262:
5184:
5159:
5096:
5071:
4562:
4537:
4461:
4443:
4361:lexicographic order
3809:well-formed formula
1863:really stands for
594:is refutable, then
302:propositional logic
65:normal form theorem
8290:Mathematical logic
8214:10.1007/BF01696781
8140:
8125:
8107:
8083:
8065:
8048:
8021:
8006:
7989:
7945:
7919:
7890:
7861:
7840:
7597:
7570:
7327:
7306:
7182:
6693:We may write each
6675:
6648:
6598:
6580:
6522:
6495:
6432:
6386:
6362:
6332:
6301:
6274:
6243:
6216:
6189:
6162:
6132:
6105:
6072:
6041:
6014:
5987:
5960:
5933:
5906:
5889:will be true: The
5879:
5852:
5818:
5791:
5764:
5737:
5702:
5671:
5637:
5454:
5429:
5347:
5311:
5266:
5248:
5216:
5170:
5145:
5082:
5057:
4856:: By induction on
4840:
4797:
4685:
4658:
4548:
4523:
4495:
4465:
4447:
4429:
4409:
4349:
4297:
4251:
4153:
4055:
3962:
3797:
3777:
3680:
3641:
3621:
3598:
3354:
3329:
3276:
3186:
3158:
3132:
3109:
3086:
3066:
3046:
3026:
2973:
2949:
2926:
2892:
2709:
2643:
2586:
2400:
2243:
2190:
2161:
1952:
1912:
1853:
1801:
1781:
1757:
1730:
1629:
1422:
1402:
1373:
1249:
1225:
1205:
1178:
899:
873:
808:
645:
568:
35:mathematical logic
22:
6895:of these objects
3196:with the formula
2665:, no variable of
1292:: Take a formula
439:soundness theorem
69:soundness theorem
20:Kurt Gödel (1925)
8312:
8253:Juliette Kennedy
8233:
8192:
8149:
8147:
8146:
8141:
8138:
8133:
8120:
8115:
8096:
8091:
8078:
8073:
8057:
8055:
8054:
8049:
8047:
8046:
8030:
8028:
8027:
8022:
8019:
8014:
7998:
7996:
7995:
7990:
7988:
7987:
7954:
7952:
7951:
7946:
7928:
7926:
7925:
7920:
7899:
7897:
7896:
7891:
7886:
7870:
7868:
7867:
7862:
7849:
7847:
7846:
7841:
7830:
7829:
7817:
7816:
7795:
7794:
7782:
7781:
7754:
7753:
7741:
7740:
7710:
7709:
7697:
7696:
7669:
7668:
7656:
7655:
7643:
7642:
7630:
7629:
7606:
7604:
7603:
7598:
7579:
7577:
7576:
7571:
7560:
7559:
7547:
7546:
7525:
7524:
7512:
7511:
7484:
7483:
7471:
7470:
7440:
7439:
7427:
7426:
7399:
7398:
7386:
7385:
7373:
7372:
7360:
7359:
7336:
7334:
7333:
7328:
7315:
7313:
7312:
7307:
7191:
7189:
7188:
7183:
6947:, which makes Φ(
6684:
6682:
6681:
6676:
6674:
6673:
6657:
6655:
6654:
6649:
6644:
6643:
6625:
6624:
6611:
6606:
6593:
6588:
6570:
6569:
6557:
6556:
6531:
6529:
6528:
6523:
6521:
6520:
6504:
6502:
6501:
6496:
6491:
6490:
6489:
6488:
6471:
6470:
6469:
6468:
6441:
6439:
6438:
6433:
6428:
6427:
6415:
6414:
6395:
6393:
6392:
6387:
6371:
6369:
6368:
6363:
6361:
6360:
6341:
6339:
6338:
6333:
6331:
6330:
6310:
6308:
6307:
6302:
6300:
6299:
6283:
6281:
6280:
6275:
6273:
6272:
6252:
6250:
6249:
6244:
6242:
6241:
6225:
6223:
6222:
6217:
6215:
6214:
6198:
6196:
6195:
6190:
6188:
6187:
6171:
6169:
6168:
6163:
6161:
6160:
6141:
6139:
6138:
6133:
6131:
6130:
6114:
6112:
6111:
6106:
6104:
6103:
6081:
6079:
6078:
6073:
6071:
6070:
6050:
6048:
6047:
6042:
6040:
6039:
6023:
6021:
6020:
6015:
6013:
6012:
5996:
5994:
5993:
5988:
5986:
5985:
5969:
5967:
5966:
5961:
5959:
5958:
5942:
5940:
5939:
5934:
5932:
5931:
5915:
5913:
5912:
5907:
5905:
5904:
5888:
5886:
5885:
5880:
5878:
5877:
5861:
5859:
5858:
5853:
5851:
5850:
5827:
5825:
5824:
5819:
5817:
5816:
5800:
5798:
5797:
5792:
5790:
5789:
5773:
5771:
5770:
5765:
5763:
5762:
5746:
5744:
5743:
5738:
5736:
5735:
5716:. Then for each
5711:
5709:
5708:
5703:
5701:
5700:
5680:
5678:
5677:
5672:
5670:
5669:
5646:
5644:
5643:
5638:
5633:
5632:
5614:
5613:
5601:
5600:
5588:
5587:
5575:
5574:
5556:
5555:
5537:
5536:
5515:
5514:
5496:
5495:
5483:
5482:
5470:
5469:
5467:
5462:
5445:
5444:
5442:
5437:
5414:
5413:
5395:
5394:
5376:
5375:
5356:
5354:
5353:
5348:
5343:
5342:
5320:
5318:
5317:
5312:
5279:
5274:
5261:
5256:
5225:
5223:
5222:
5217:
5212:
5211:
5199:
5198:
5186:
5185:
5183:
5178:
5161:
5160:
5158:
5153:
5130:
5129:
5117:
5116:
5098:
5097:
5095:
5090:
5073:
5072:
5070:
5065:
5042:
5041:
5023:
5022:
5010:
5009:
4988:
4987:
4948:
4947:
4914:
4913:
4895:
4894:
4876:
4875:
4849:
4847:
4846:
4841:
4839:
4838:
4806:
4804:
4803:
4798:
4790:
4789:
4771:
4770:
4758:
4757:
4742:
4741:
4720:
4719:
4694:
4692:
4691:
4686:
4684:
4683:
4667:
4665:
4664:
4659:
4654:
4653:
4632:
4631:
4598:
4597:
4564:
4563:
4561:
4556:
4539:
4538:
4536:
4531:
4504:
4502:
4501:
4496:
4494:
4493:
4478:Set the formula
4474:
4472:
4471:
4466:
4460:
4455:
4442:
4437:
4418:
4416:
4415:
4410:
4405:
4404:
4392:
4391:
4379:
4378:
4358:
4356:
4355:
4350:
4345:
4344:
4326:
4325:
4306:
4304:
4303:
4298:
4293:
4292:
4280:
4279:
4260:
4258:
4257:
4252:
4247:
4246:
4234:
4233:
4221:
4220:
4205:
4204:
4192:
4191:
4179:
4178:
4162:
4160:
4159:
4154:
4149:
4148:
4136:
4135:
4123:
4122:
4107:
4106:
4094:
4093:
4081:
4080:
4064:
4062:
4061:
4056:
4051:
4050:
4038:
4037:
4019:
4018:
4006:
4005:
3971:
3969:
3968:
3963:
3955:
3954:
3942:
3941:
3929:
3928:
3916:
3915:
3897:
3896:
3884:
3883:
3865:
3864:
3852:
3851:
3819:As shown by the
3806:
3804:
3803:
3798:
3786:
3784:
3783:
3778:
3773:
3762:
3689:
3687:
3686:
3681:
3650:
3648:
3647:
3642:
3630:
3628:
3627:
3622:
3607:
3605:
3604:
3599:
3483:
3472:
3410:
3393:
3363:
3361:
3360:
3355:
3338:
3336:
3335:
3330:
3285:
3283:
3282:
3277:
3272:
3261:
3195:
3193:
3192:
3187:
3167:
3165:
3164:
3159:
3141:
3139:
3138:
3133:
3118:
3116:
3115:
3110:
3095:
3093:
3092:
3087:
3075:
3073:
3072:
3067:
3055:
3053:
3052:
3047:
3035:
3033:
3032:
3027:
3007:
2982:
2980:
2979:
2974:
2958:
2956:
2955:
2950:
2935:
2933:
2932:
2927:
2919:
2901:
2899:
2898:
2893:
2855:
2844:
2806:
2753:
2718:
2716:
2715:
2710:
2705:
2652:
2650:
2649:
2644:
2642:
2631:
2595:
2593:
2592:
2587:
2492:
2481:
2464:
2447:
2430:
2409:
2407:
2406:
2401:
2252:
2250:
2249:
2244:
2199:
2197:
2196:
2191:
2170:
2168:
2167:
2162:
2067:
2056:
2039:
2022:
1961:
1959:
1958:
1953:
1951:
1950:
1938:
1937:
1921:
1919:
1918:
1913:
1911:
1910:
1895:
1894:
1882:
1881:
1862:
1860:
1859:
1854:
1810:
1808:
1807:
1802:
1790:
1788:
1787:
1782:
1766:
1764:
1763:
1758:
1739:
1737:
1736:
1731:
1638:
1636:
1635:
1630:
1604:
1587:
1576:
1565:
1545:
1480:
1431:
1429:
1428:
1423:
1411:
1409:
1408:
1403:
1382:
1380:
1379:
1374:
1285: + 1.
1258:
1256:
1255:
1250:
1234:
1232:
1231:
1226:
1214:
1212:
1211:
1206:
1187:
1185:
1184:
1179:
1165:
1164:
1163:
1162:
1142:
1141:
1134:
1133:
1104:
1103:
1102:
1101:
1075:
1074:
1067:
1066:
1034:
1033:
1032:
1031:
1011:
1010:
1003:
1002:
979:
978:
977:
976:
956:
955:
908:
906:
905:
900:
882:
880:
879:
874:
817:
815:
814:
809:
654:
652:
651:
646:
638:
637:
622:
621:
577:
575:
574:
569:
564:
563:
548:
547:
496:in normal form.
295:
212:
124:
120:
116:
112:
105:, i.e. with all
80:without identity
76:without equality
8320:
8319:
8315:
8314:
8313:
8311:
8310:
8309:
8265:
8264:
8241:
8196:
8183:
8180:
8160:Axiom of Choice
8156:
8060:
8059:
8038:
8033:
8032:
8001:
8000:
7979:
7974:
7973:
7969:
7931:
7930:
7905:
7904:
7879:
7874:
7873:
7853:
7852:
7821:
7808:
7786:
7773:
7745:
7732:
7701:
7688:
7660:
7647:
7634:
7621:
7610:
7609:
7583:
7582:
7551:
7538:
7516:
7503:
7475:
7462:
7431:
7418:
7390:
7377:
7364:
7351:
7340:
7339:
7319:
7318:
7193:
7192:
7036:
7035:
7028:
7023:
7012:
7005:
6998:
6997:
6984:
6983:
6972:
6971:
6958:
6957:
6946:
6945:
6932:
6931:
6920:
6919:
6906:
6905:
6890:
6877:
6870:
6863:
6851:
6850:
6844:
6840:
6831:
6818:
6811:
6810:
6799:
6792:
6775:
6765:
6758:
6751:
6733:
6724:
6717:
6708:
6701:
6691:
6665:
6660:
6659:
6635:
6616:
6561:
6548:
6537:
6536:
6512:
6507:
6506:
6480:
6475:
6460:
6455:
6444:
6443:
6419:
6406:
6398:
6397:
6378:
6377:
6374:natural numbers
6352:
6347:
6346:
6322:
6317:
6316:
6291:
6286:
6285:
6264:
6259:
6258:
6233:
6228:
6227:
6206:
6201:
6200:
6179:
6174:
6173:
6152:
6147:
6146:
6122:
6117:
6116:
6089:
6084:
6083:
6062:
6057:
6056:
6031:
6026:
6025:
6004:
5999:
5998:
5977:
5972:
5971:
5950:
5945:
5944:
5923:
5918:
5917:
5896:
5891:
5890:
5869:
5864:
5863:
5842:
5837:
5836:
5808:
5803:
5802:
5781:
5776:
5775:
5754:
5749:
5748:
5727:
5722:
5721:
5692:
5687:
5686:
5661:
5656:
5655:
5618:
5605:
5592:
5579:
5566:
5541:
5528:
5500:
5487:
5474:
5449:
5424:
5399:
5386:
5367:
5362:
5361:
5328:
5323:
5322:
5228:
5227:
5203:
5190:
5165:
5140:
5121:
5108:
5077:
5052:
5027:
5014:
4992:
4958:
4918:
4905:
4880:
4867:
4862:
4861:
4830:
4819:
4818:
4781:
4762:
4749:
4724:
4711:
4700:
4699:
4675:
4670:
4669:
4636:
4602:
4568:
4543:
4518:
4507:
4506:
4485:
4480:
4479:
4421:
4420:
4396:
4383:
4370:
4365:
4364:
4336:
4317:
4309:
4308:
4284:
4271:
4263:
4262:
4238:
4225:
4212:
4196:
4183:
4170:
4165:
4164:
4140:
4127:
4114:
4098:
4085:
4072:
4067:
4066:
4042:
4029:
4010:
3997:
3989:
3988:
3985:natural numbers
3946:
3933:
3920:
3907:
3888:
3875:
3856:
3843:
3832:
3831:
3817:
3789:
3788:
3766:
3755:
3699:
3698:
3669:
3668:
3633:
3632:
3613:
3612:
3476:
3465:
3403:
3386:
3369:
3368:
3343:
3342:
3288:
3287:
3265:
3254:
3198:
3197:
3175:
3174:
3147:
3146:
3121:
3120:
3098:
3097:
3078:
3077:
3058:
3057:
3038:
3037:
3000:
2989:
2988:
2965:
2964:
2941:
2940:
2912:
2907:
2906:
2848:
2837:
2799:
2746:
2729:
2728:
2698:
2675:
2674:
2635:
2624:
2601:
2600:
2485:
2474:
2457:
2440:
2423:
2418:
2417:
2266:
2265:
2205:
2204:
2176:
2175:
2060:
2049:
2032:
2015:
1998:
1997:
1942:
1929:
1924:
1923:
1902:
1886:
1873:
1865:
1864:
1836:
1835:
1793:
1792:
1773:
1772:
1749:
1748:
1659:
1658:
1597:
1580:
1569:
1558:
1538:
1473:
1462:
1461:
1414:
1413:
1385:
1384:
1302:
1301:
1241:
1240:
1217:
1216:
1197:
1196:
1154:
1149:
1119:
1114:
1087:
1082:
1052:
1047:
1023:
1018:
994:
989:
968:
963:
947:
930:
929:
915:
885:
884:
820:
819:
728:
727:
629:
613:
596:
595:
555:
539:
525:
524:
518:
509:
406:
382:
362:
353:
339:
315:
293:
292:
286:
285:
279:
278:
272:
271:
265:
264:
258:
257:
251:
250:
244:
243:
237:
236:
230:
229:
223:
220:
210:
202: ...
201:
194:
186: ...
185:
175:
166:
159:
152:
143:
136:
129:
122:
118:
114:
110:
92:
43:
12:
11:
5:
8318:
8316:
8308:
8307:
8305:Article proofs
8302:
8297:
8292:
8287:
8282:
8277:
8267:
8266:
8263:
8262:
8256:
8240:
8239:External links
8237:
8236:
8235:
8208:(1): 349–360.
8194:
8179:
8176:
8155:
8152:
8137:
8132:
8128:
8124:
8119:
8114:
8110:
8106:
8103:
8100:
8095:
8090:
8086:
8082:
8077:
8072:
8068:
8045:
8041:
8018:
8013:
8009:
7986:
7982:
7968:
7965:
7944:
7941:
7938:
7918:
7915:
7912:
7901:
7900:
7889:
7885:
7882:
7871:
7860:
7850:
7839:
7836:
7833:
7828:
7824:
7820:
7815:
7811:
7807:
7804:
7801:
7798:
7793:
7789:
7785:
7780:
7776:
7772:
7769:
7766:
7763:
7760:
7757:
7752:
7748:
7744:
7739:
7735:
7731:
7728:
7725:
7722:
7719:
7716:
7713:
7708:
7704:
7700:
7695:
7691:
7687:
7684:
7681:
7678:
7675:
7672:
7667:
7663:
7659:
7654:
7650:
7646:
7641:
7637:
7633:
7628:
7624:
7620:
7617:
7607:
7596:
7593:
7590:
7580:
7569:
7566:
7563:
7558:
7554:
7550:
7545:
7541:
7537:
7534:
7531:
7528:
7523:
7519:
7515:
7510:
7506:
7502:
7499:
7496:
7493:
7490:
7487:
7482:
7478:
7474:
7469:
7465:
7461:
7458:
7455:
7452:
7449:
7446:
7443:
7438:
7434:
7430:
7425:
7421:
7417:
7414:
7411:
7408:
7405:
7402:
7397:
7393:
7389:
7384:
7380:
7376:
7371:
7367:
7363:
7358:
7354:
7350:
7347:
7337:
7326:
7316:
7305:
7302:
7299:
7296:
7293:
7290:
7287:
7284:
7281:
7278:
7275:
7272:
7269:
7266:
7263:
7260:
7257:
7254:
7251:
7248:
7245:
7242:
7239:
7236:
7233:
7230:
7227:
7224:
7221:
7218:
7215:
7212:
7209:
7206:
7203:
7200:
7181:
7178:
7175:
7172:
7169:
7166:
7163:
7160:
7157:
7154:
7151:
7148:
7145:
7142:
7139:
7136:
7133:
7130:
7127:
7124:
7121:
7118:
7115:
7112:
7109:
7106:
7103:
7100:
7097:
7094:
7091:
7088:
7085:
7082:
7079:
7076:
7073:
7070:
7067:
7064:
7061:
7058:
7055:
7052:
7049:
7046:
7043:
7027:
7024:
7022:
7019:
7010:
7003:
6993:
6989:
6981:
6977:
6967:
6963:
6955:
6951:
6941:
6937:
6929:
6925:
6915:
6911:
6903:
6899:
6886:
6875:
6868:
6859:
6848:
6846:
6842:
6836:
6827:
6816:
6808:
6804:
6797:
6788:
6770:
6763:
6756:
6749:
6729:
6722:
6713:
6706:
6697:
6690:
6687:
6672:
6668:
6647:
6642:
6638:
6634:
6631:
6628:
6623:
6619:
6615:
6610:
6605:
6601:
6597:
6592:
6587:
6583:
6579:
6576:
6573:
6568:
6564:
6560:
6555:
6551:
6547:
6544:
6519:
6515:
6494:
6487:
6483:
6478:
6474:
6467:
6463:
6458:
6454:
6451:
6431:
6426:
6422:
6418:
6413:
6409:
6405:
6385:
6359:
6355:
6329:
6325:
6298:
6294:
6271:
6267:
6240:
6236:
6213:
6209:
6186:
6182:
6159:
6155:
6129:
6125:
6102:
6099:
6096:
6092:
6069:
6065:
6038:
6034:
6011:
6007:
5984:
5980:
5957:
5953:
5930:
5926:
5903:
5899:
5876:
5872:
5862:, so that all
5849:
5845:
5815:
5811:
5788:
5784:
5761:
5757:
5734:
5730:
5699:
5695:
5668:
5664:
5636:
5631:
5628:
5625:
5621:
5617:
5612:
5608:
5604:
5599:
5595:
5591:
5586:
5582:
5578:
5573:
5569:
5565:
5562:
5559:
5554:
5551:
5548:
5544:
5540:
5535:
5531:
5527:
5524:
5521:
5518:
5513:
5510:
5507:
5503:
5499:
5494:
5490:
5486:
5481:
5477:
5473:
5466:
5461:
5457:
5452:
5448:
5441:
5436:
5432:
5427:
5423:
5420:
5417:
5412:
5409:
5406:
5402:
5398:
5393:
5389:
5385:
5382:
5379:
5374:
5370:
5346:
5341:
5338:
5335:
5331:
5310:
5307:
5304:
5301:
5298:
5295:
5292:
5289:
5286:
5283:
5278:
5273:
5269:
5265:
5260:
5255:
5251:
5247:
5244:
5241:
5238:
5235:
5215:
5210:
5206:
5202:
5197:
5193:
5189:
5182:
5177:
5173:
5168:
5164:
5157:
5152:
5148:
5143:
5139:
5136:
5133:
5128:
5124:
5120:
5115:
5111:
5107:
5104:
5101:
5094:
5089:
5085:
5080:
5076:
5069:
5064:
5060:
5055:
5051:
5048:
5045:
5040:
5037:
5034:
5030:
5026:
5021:
5017:
5013:
5008:
5005:
5002:
4999:
4995:
4991:
4986:
4983:
4980:
4977:
4974:
4971:
4968:
4965:
4961:
4957:
4954:
4951:
4946:
4943:
4940:
4937:
4934:
4931:
4928:
4925:
4921:
4917:
4912:
4908:
4904:
4901:
4898:
4893:
4890:
4887:
4883:
4879:
4874:
4870:
4837:
4833:
4829:
4826:
4808:
4807:
4796:
4793:
4788:
4784:
4780:
4777:
4774:
4769:
4765:
4761:
4756:
4752:
4748:
4745:
4740:
4737:
4734:
4731:
4727:
4723:
4718:
4714:
4710:
4707:
4682:
4678:
4657:
4652:
4649:
4646:
4643:
4639:
4635:
4630:
4627:
4624:
4621:
4618:
4615:
4612:
4609:
4605:
4601:
4596:
4593:
4590:
4587:
4584:
4581:
4578:
4575:
4571:
4567:
4560:
4555:
4551:
4546:
4542:
4535:
4530:
4526:
4521:
4517:
4514:
4492:
4488:
4464:
4459:
4454:
4450:
4446:
4441:
4436:
4432:
4428:
4408:
4403:
4399:
4395:
4390:
4386:
4382:
4377:
4373:
4348:
4343:
4339:
4335:
4332:
4329:
4324:
4320:
4316:
4296:
4291:
4287:
4283:
4278:
4274:
4270:
4250:
4245:
4241:
4237:
4232:
4228:
4224:
4219:
4215:
4211:
4208:
4203:
4199:
4195:
4190:
4186:
4182:
4177:
4173:
4152:
4147:
4143:
4139:
4134:
4130:
4126:
4121:
4117:
4113:
4110:
4105:
4101:
4097:
4092:
4088:
4084:
4079:
4075:
4054:
4049:
4045:
4041:
4036:
4032:
4028:
4025:
4022:
4017:
4013:
4009:
4004:
4000:
3996:
3973:
3972:
3961:
3958:
3953:
3949:
3945:
3940:
3936:
3932:
3927:
3923:
3919:
3914:
3910:
3906:
3903:
3900:
3895:
3891:
3887:
3882:
3878:
3874:
3871:
3868:
3863:
3859:
3855:
3850:
3846:
3842:
3839:
3816:
3813:
3796:
3776:
3772:
3769:
3765:
3761:
3758:
3754:
3751:
3748:
3745:
3742:
3739:
3736:
3733:
3730:
3727:
3724:
3721:
3718:
3715:
3712:
3709:
3706:
3679:
3676:
3667:, we see that
3640:
3620:
3609:
3608:
3597:
3594:
3591:
3588:
3585:
3582:
3579:
3576:
3573:
3570:
3567:
3564:
3561:
3558:
3555:
3552:
3549:
3546:
3543:
3540:
3537:
3534:
3531:
3528:
3525:
3522:
3519:
3516:
3513:
3510:
3507:
3504:
3501:
3498:
3495:
3492:
3489:
3486:
3482:
3479:
3475:
3471:
3468:
3464:
3461:
3458:
3455:
3452:
3449:
3446:
3443:
3440:
3437:
3434:
3431:
3428:
3425:
3422:
3419:
3416:
3413:
3409:
3406:
3402:
3399:
3396:
3392:
3389:
3385:
3382:
3379:
3376:
3353:
3350:
3328:
3325:
3322:
3319:
3316:
3313:
3310:
3307:
3304:
3301:
3298:
3295:
3275:
3271:
3268:
3264:
3260:
3257:
3253:
3250:
3247:
3244:
3241:
3238:
3235:
3232:
3229:
3226:
3223:
3220:
3217:
3214:
3211:
3208:
3205:
3185:
3182:
3157:
3154:
3131:
3128:
3108:
3105:
3085:
3065:
3045:
3036:, we see that
3025:
3022:
3019:
3016:
3013:
3010:
3006:
3003:
2999:
2996:
2972:
2948:
2925:
2922:
2918:
2915:
2903:
2902:
2891:
2888:
2885:
2882:
2879:
2876:
2873:
2870:
2867:
2864:
2861:
2858:
2854:
2851:
2847:
2843:
2840:
2836:
2833:
2830:
2827:
2824:
2821:
2818:
2815:
2812:
2809:
2805:
2802:
2798:
2795:
2792:
2789:
2786:
2783:
2780:
2777:
2774:
2771:
2768:
2765:
2762:
2759:
2756:
2752:
2749:
2745:
2742:
2739:
2736:
2708:
2704:
2701:
2697:
2694:
2691:
2688:
2685:
2682:
2641:
2638:
2634:
2630:
2627:
2623:
2620:
2617:
2614:
2611:
2608:
2597:
2596:
2585:
2582:
2579:
2576:
2573:
2570:
2567:
2564:
2561:
2558:
2555:
2552:
2549:
2546:
2543:
2540:
2537:
2534:
2531:
2528:
2525:
2522:
2519:
2516:
2513:
2510:
2507:
2504:
2501:
2498:
2495:
2491:
2488:
2484:
2480:
2477:
2473:
2470:
2467:
2463:
2460:
2456:
2453:
2450:
2446:
2443:
2439:
2436:
2433:
2429:
2426:
2411:
2410:
2399:
2396:
2393:
2390:
2387:
2384:
2381:
2378:
2375:
2372:
2369:
2366:
2363:
2360:
2357:
2354:
2351:
2348:
2345:
2342:
2339:
2336:
2333:
2330:
2327:
2324:
2321:
2318:
2315:
2312:
2309:
2306:
2303:
2300:
2297:
2294:
2291:
2288:
2285:
2282:
2279:
2276:
2273:
2242:
2239:
2236:
2233:
2230:
2227:
2224:
2221:
2218:
2215:
2212:
2189:
2186:
2183:
2172:
2171:
2160:
2157:
2154:
2151:
2148:
2145:
2142:
2139:
2136:
2133:
2130:
2127:
2124:
2121:
2118:
2115:
2112:
2109:
2106:
2103:
2100:
2097:
2094:
2091:
2088:
2085:
2082:
2079:
2076:
2073:
2070:
2066:
2063:
2059:
2055:
2052:
2048:
2045:
2042:
2038:
2035:
2031:
2028:
2025:
2021:
2018:
2014:
2011:
2008:
2005:
1949:
1945:
1941:
1936:
1932:
1909:
1905:
1901:
1898:
1893:
1889:
1885:
1880:
1876:
1872:
1852:
1849:
1846:
1843:
1800:
1780:
1756:
1741:
1740:
1729:
1726:
1723:
1720:
1717:
1714:
1711:
1708:
1705:
1702:
1699:
1696:
1693:
1690:
1687:
1684:
1681:
1678:
1675:
1672:
1669:
1666:
1645:
1644:
1628:
1625:
1622:
1619:
1616:
1613:
1610:
1607:
1603:
1600:
1596:
1593:
1590:
1586:
1583:
1579:
1575:
1572:
1568:
1564:
1561:
1557:
1554:
1551:
1548:
1544:
1541:
1537:
1534:
1531:
1528:
1525:
1522:
1519:
1516:
1513:
1510:
1507:
1504:
1501:
1498:
1495:
1492:
1489:
1486:
1483:
1479:
1476:
1472:
1469:
1421:
1401:
1398:
1395:
1392:
1372:
1369:
1366:
1363:
1360:
1357:
1354:
1351:
1348:
1345:
1342:
1339:
1336:
1333:
1330:
1327:
1324:
1321:
1318:
1315:
1312:
1309:
1248:
1224:
1204:
1191:We define the
1189:
1188:
1177:
1174:
1171:
1168:
1161:
1157:
1152:
1148:
1145:
1140:
1137:
1132:
1129:
1126:
1122:
1117:
1113:
1110:
1107:
1100:
1097:
1094:
1090:
1085:
1081:
1078:
1073:
1070:
1065:
1062:
1059:
1055:
1050:
1046:
1043:
1040:
1037:
1030:
1026:
1021:
1017:
1014:
1009:
1006:
1001:
997:
992:
988:
985:
982:
975:
971:
966:
962:
959:
954:
950:
946:
943:
940:
937:
914:
911:
898:
895:
892:
872:
869:
866:
863:
860:
857:
854:
851:
848:
845:
842:
839:
836:
833:
830:
827:
807:
804:
801:
798:
795:
792:
789:
786:
783:
780:
777:
774:
771:
768:
765:
762:
759:
756:
753:
750:
747:
744:
741:
738:
735:
718:and Φ for the
644:
641:
636:
632:
628:
625:
620:
616:
612:
609:
606:
603:
567:
562:
558:
554:
551:
546:
542:
538:
535:
532:
514:
507:
405:
402:
381:
378:
376:is provable".
361:
358:
352:
349:
348:
347:
346:
345:
335:
329:
311:
305:
290:
288:
283:
281:
276:
274:
269:
267:
262:
260:
255:
253:
248:
246:
241:
239:
234:
232:
227:
225:
221:
214:
206:
199:
190:
183:
171:
164:
157:
148:
141:
134:
126:
91:
88:
42:
39:
13:
10:
9:
6:
4:
3:
2:
8317:
8306:
8303:
8301:
8298:
8296:
8293:
8291:
8288:
8286:
8283:
8281:
8278:
8276:
8273:
8272:
8270:
8261:
8257:
8254:
8250:
8246:
8243:
8242:
8238:
8231:
8227:
8223:
8219:
8215:
8211:
8207:
8204:(in German).
8203:
8199:
8195:
8190:
8186:
8182:
8181:
8177:
8175:
8173:
8169:
8165:
8161:
8153:
8151:
8135:
8130:
8126:
8122:
8117:
8112:
8108:
8104:
8101:
8098:
8093:
8088:
8084:
8080:
8075:
8070:
8066:
8043:
8039:
8016:
8011:
8007:
7984:
7980:
7966:
7964:
7962:
7958:
7942:
7939:
7936:
7916:
7913:
7910:
7887:
7883:
7880:
7872:
7858:
7851:
7826:
7822:
7818:
7813:
7809:
7802:
7799:
7791:
7787:
7783:
7778:
7774:
7767:
7750:
7746:
7742:
7737:
7733:
7726:
7723:
7720:
7717:
7714:
7706:
7702:
7698:
7693:
7689:
7682:
7679:
7665:
7661:
7657:
7652:
7648:
7644:
7639:
7635:
7631:
7626:
7622:
7608:
7594:
7591:
7588:
7581:
7556:
7552:
7548:
7543:
7539:
7532:
7529:
7521:
7517:
7513:
7508:
7504:
7497:
7480:
7476:
7472:
7467:
7463:
7456:
7453:
7450:
7447:
7444:
7436:
7432:
7428:
7423:
7419:
7412:
7409:
7395:
7391:
7387:
7382:
7378:
7374:
7369:
7365:
7361:
7356:
7352:
7338:
7324:
7317:
7294:
7291:
7288:
7282:
7279:
7270:
7267:
7264:
7258:
7255:
7243:
7240:
7237:
7231:
7228:
7219:
7216:
7213:
7210:
7207:
7198:
7170:
7167:
7164:
7158:
7155:
7146:
7143:
7140:
7134:
7131:
7119:
7116:
7113:
7107:
7104:
7095:
7092:
7089:
7086:
7083:
7074:
7068:
7065:
7062:
7056:
7053:
7047:
7034:
7033:
7032:
7025:
7020:
7018:
7016:
7009:
7002:
6996:
6992:
6988:
6980:
6976:
6970:
6966:
6962:
6954:
6950:
6944:
6940:
6936:
6928:
6924:
6918:
6914:
6910:
6902:
6898:
6894:
6889:
6885:
6881:
6874:
6867:
6862:
6858:
6853:
6841:. For every B
6839:
6835:
6830:
6826:
6822:
6815:
6807:
6803:
6796:
6791:
6787:
6783:
6779:
6773:
6769:
6762:
6755:
6748:
6743:
6741:
6737:
6732:
6728:
6721:
6716:
6712:
6705:
6700:
6696:
6688:
6686:
6670:
6666:
6640:
6636:
6632:
6629:
6626:
6621:
6617:
6613:
6608:
6603:
6599:
6595:
6590:
6585:
6581:
6574:
6566:
6562:
6558:
6553:
6549:
6533:
6517:
6513:
6485:
6481:
6476:
6472:
6465:
6461:
6456:
6424:
6420:
6416:
6411:
6407:
6375:
6357:
6353:
6343:
6327:
6323:
6314:
6296:
6292:
6269:
6265:
6256:
6238:
6234:
6211:
6207:
6184:
6180:
6157:
6153:
6143:
6127:
6123:
6100:
6097:
6094:
6090:
6067:
6063:
6054:
6036:
6032:
6009:
6005:
5982:
5978:
5955:
5951:
5928:
5924:
5901:
5897:
5874:
5870:
5847:
5843:
5833:
5831:
5813:
5809:
5786:
5782:
5759:
5755:
5732:
5728:
5719:
5715:
5697:
5693:
5684:
5666:
5662:
5652:
5650:
5629:
5626:
5623:
5619:
5615:
5610:
5606:
5602:
5597:
5593:
5589:
5584:
5580:
5576:
5571:
5567:
5560:
5552:
5549:
5546:
5542:
5538:
5533:
5529:
5519:
5511:
5508:
5505:
5501:
5497:
5492:
5488:
5484:
5479:
5475:
5471:
5464:
5459:
5455:
5450:
5446:
5439:
5434:
5430:
5425:
5418:
5410:
5407:
5404:
5400:
5396:
5391:
5387:
5377:
5372:
5368:
5358:
5344:
5339:
5336:
5333:
5329:
5308:
5305:
5302:
5296:
5293:
5290:
5284:
5276:
5271:
5267:
5263:
5258:
5253:
5249:
5239:
5208:
5204:
5200:
5195:
5191:
5187:
5180:
5175:
5171:
5166:
5162:
5155:
5150:
5146:
5141:
5134:
5126:
5122:
5118:
5113:
5109:
5092:
5087:
5083:
5078:
5074:
5067:
5062:
5058:
5053:
5043:
5038:
5035:
5032:
5028:
5019:
5015:
5006:
5003:
5000:
4997:
4993:
4989:
4984:
4981:
4978:
4972:
4969:
4966:
4959:
4944:
4941:
4938:
4932:
4929:
4926:
4919:
4915:
4910:
4906:
4896:
4891:
4888:
4885:
4881:
4872:
4868:
4859:
4855:
4851:
4835:
4831:
4824:
4816:
4812:
4794:
4786:
4782:
4778:
4775:
4772:
4767:
4763:
4759:
4754:
4750:
4738:
4735:
4732:
4729:
4725:
4721:
4716:
4712:
4698:
4697:
4696:
4680:
4676:
4650:
4647:
4644:
4641:
4637:
4633:
4628:
4625:
4622:
4616:
4613:
4610:
4603:
4599:
4594:
4591:
4588:
4582:
4579:
4576:
4569:
4565:
4558:
4553:
4549:
4544:
4540:
4533:
4528:
4524:
4519:
4512:
4490:
4486:
4476:
4457:
4452:
4448:
4444:
4439:
4434:
4430:
4401:
4397:
4393:
4388:
4384:
4375:
4362:
4341:
4337:
4333:
4330:
4327:
4322:
4318:
4289:
4285:
4281:
4276:
4272:
4243:
4239:
4235:
4230:
4226:
4217:
4209:
4201:
4197:
4193:
4188:
4184:
4175:
4145:
4141:
4137:
4132:
4128:
4119:
4111:
4103:
4099:
4095:
4090:
4086:
4077:
4047:
4043:
4039:
4034:
4030:
4023:
4015:
4011:
4007:
4002:
3998:
3986:
3982:
3978:
3959:
3951:
3947:
3943:
3938:
3934:
3930:
3925:
3921:
3917:
3912:
3908:
3901:
3893:
3889:
3885:
3880:
3876:
3861:
3857:
3853:
3848:
3844:
3830:
3829:
3828:
3826:
3822:
3814:
3812:
3810:
3770:
3767:
3763:
3759:
3756:
3752:
3749:
3746:
3743:
3737:
3731:
3722:
3710:
3695:
3693:
3677:
3666:
3662:
3658:
3654:
3638:
3618:
3589:
3583:
3574:
3562:
3550:
3544:
3535:
3523:
3508:
3496:
3487:
3480:
3477:
3473:
3469:
3466:
3462:
3459:
3456:
3453:
3447:
3441:
3432:
3420:
3407:
3404:
3390:
3387:
3367:
3366:
3365:
3364:then becomes
3340:
3326:
3320:
3311:
3299:
3269:
3266:
3262:
3258:
3255:
3251:
3248:
3245:
3242:
3236:
3230:
3221:
3209:
3171:
3169:
3043:
3023:
3014:
3008:
3004:
2997:
2986:
2962:
2937:
2920:
2916:
2886:
2877:
2874:
2871:
2865:
2859:
2852:
2849:
2845:
2841:
2838:
2831:
2825:
2816:
2803:
2800:
2787:
2775:
2763:
2750:
2747:
2737:
2727:
2726:
2725:
2722:
2702:
2699:
2695:
2692:
2683:
2672:
2668:
2664:
2660:
2656:
2639:
2636:
2628:
2625:
2618:
2615:
2609:
2580:
2571:
2568:
2565:
2559:
2550:
2541:
2529:
2517:
2505:
2496:
2489:
2486:
2482:
2478:
2475:
2468:
2461:
2458:
2444:
2441:
2431:
2427:
2416:
2415:
2414:
2394:
2385:
2382:
2379:
2373:
2364:
2355:
2343:
2334:
2328:
2322:
2313:
2301:
2286:
2283:
2280:
2274:
2264:
2263:
2262:
2260:
2256:
2237:
2228:
2216:
2201:
2200:is provable.
2187:
2155:
2149:
2140:
2128:
2113:
2110:
2107:
2101:
2092:
2080:
2071:
2064:
2061:
2057:
2053:
2050:
2043:
2036:
2033:
2019:
2016:
2006:
1996:
1995:
1994:
1992:
1988:
1984:
1980:
1976:
1972:
1968:
1963:
1947:
1943:
1939:
1934:
1930:
1907:
1903:
1896:
1891:
1887:
1878:
1874:
1847:
1834:
1830:
1826:
1822:
1818:
1814:
1798:
1778:
1770:
1754:
1746:
1727:
1721:
1712:
1700:
1688:
1676:
1667:
1664:
1657:
1656:
1655:
1653:
1649:
1642:
1641:Unfortunately
1623:
1614:
1611:
1608:
1601:
1598:
1591:
1584:
1581:
1577:
1573:
1570:
1562:
1559:
1552:
1542:
1539:
1526:
1514:
1502:
1490:
1477:
1474:
1459:
1455:
1451:
1447:
1443:
1439:
1435:
1419:
1399:
1393:
1370:
1364:
1355:
1343:
1331:
1319:
1310:
1307:
1299:
1295:
1291:
1288:
1287:
1286:
1284:
1280:
1276:
1272:
1268:
1264:
1260:
1246:
1238:
1222:
1202:
1194:
1159:
1155:
1150:
1143:
1138:
1135:
1130:
1127:
1124:
1120:
1115:
1098:
1095:
1092:
1088:
1083:
1076:
1071:
1068:
1063:
1060:
1057:
1053:
1048:
1038:
1028:
1024:
1019:
1012:
1007:
1004:
999:
995:
990:
973:
969:
964:
957:
952:
948:
938:
935:
928:
927:
926:
924:
920:
912:
910:
909:is provable.
896:
893:
890:
864:
858:
852:
846:
840:
834:
828:
796:
790:
784:
778:
772:
766:
757:
748:
742:
736:
733:
725:
721:
717:
713:
709:
705:
701:
697:
693:
689:
685:
681:
677:
672:
670:
666:
662:
658:
642:
634:
630:
623:
618:
614:
607:
604:
593:
589:
585:
581:
565:
560:
556:
549:
544:
540:
533:
530:
522:
517:
513:
506:
502:
497:
495:
492:for formulas
491:
487:
483:
479:
475:
471:
468: ≡
467:
463:
459:
455:
451:
446:
442:
440:
436:
432:
429: ≡
428:
424:
420:
416:
411:
403:
401:
399:
395:
391:
387:
379:
377:
375:
371:
370:by definition
367:
359:
357:
350:
343:
338:
334:
330:
327:
323:
319:
314:
310:
306:
303:
299:
218:
217:
215:
209:
205:
198:
193:
189:
182:
178:
174:
170:
163:
160: ∃
156:
153: ∃
151:
147:
140:
137: ∀
133:
127:
108:
104:
100:
99:
98:
95:
89:
87:
85:
84:with equality
81:
77:
72:
70:
66:
61:
59:
53:
50:
48:
45:We work with
40:
38:
36:
31:
27:
24:The proof of
18:
8295:Proof theory
8280:Model theory
8205:
8201:
8188:
8157:
7970:
7960:
7956:
7902:
7029:
7014:
7007:
7000:
6994:
6990:
6986:
6978:
6974:
6968:
6964:
6960:
6952:
6948:
6942:
6938:
6934:
6926:
6922:
6916:
6912:
6908:
6900:
6896:
6892:
6887:
6883:
6879:
6872:
6865:
6860:
6856:
6854:
6845:there is a D
6837:
6833:
6828:
6824:
6820:
6813:
6805:
6801:
6794:
6789:
6785:
6781:
6777:
6771:
6767:
6760:
6753:
6746:
6744:
6739:
6735:
6730:
6726:
6719:
6714:
6710:
6703:
6698:
6694:
6692:
6534:
6344:
6312:
6254:
6144:
6052:
5970:) affecting
5834:
5801:, such that
5717:
5713:
5682:
5653:
5648:
5359:
4857:
4853:
4852:
4814:
4813:: For every
4810:
4809:
4477:
3987:as follows:
3976:
3974:
3824:
3820:
3818:
3696:
3691:
3664:
3660:
3659:replaced by
3656:
3652:
3610:
3341:
3172:
3143:
2984:
2960:
2938:
2905:and we have
2904:
2720:
2670:
2666:
2662:
2658:
2654:
2598:
2412:
2258:
2254:
2202:
2173:
1990:
1986:
1982:
1978:
1974:
1970:
1966:
1964:
1832:
1828:
1827:denote here
1824:
1820:
1816:
1812:
1768:
1744:
1742:
1651:
1647:
1646:
1640:
1457:
1453:
1449:
1445:
1441:
1437:
1433:
1297:
1293:
1289:
1282:
1278:
1274:
1270:
1266:
1262:
1261:
1192:
1190:
922:
918:
916:
723:
719:
715:
711:
707:
703:
699:
695:
691:
687:
683:
679:
675:
673:
668:
664:
660:
656:
591:
587:
583:
579:
520:
519:are free in
515:
511:
504:
500:
498:
493:
489:
485:
481:
477:
473:
469:
465:
461:
457:
449:
447:
443:
434:
430:
426:
422:
418:
414:
409:
407:
397:
393:
389:
385:
383:
373:
369:
365:
363:
354:
341:
336:
332:
325:
321:
317:
312:
308:
298:truth values
207:
203:
196:
191:
187:
180:
176:
172:
168:
161:
154:
149:
145:
138:
131:
96:
93:
83:
79:
75:
73:
62:
54:
51:
44:
23:
8260:Kurt Gödel.
6734:) for some
5651:is proven.
4668:. Then put
2663:furthermore
478:normal form
462:normal form
454:prenex form
107:quantifiers
103:prenex form
41:Assumptions
8269:Categories
8249:Kurt Gödel
8222:56.0046.04
8178:References
8164:well-order
7021:Extensions
6921:there are
6055:for which
4860:; we have
1296:of degree
1281:of degree
1273:of degree
726:) we form
694:unused in
523:, we form
464:such that
259:...∃
238:...∀
30:Kurt Gödel
8230:123343522
8123:…
8102:…
8081:…
7981:φ
7940:…
7914:…
7881:φ
7859:∧
7819:…
7800:≡
7784:…
7762:→
7721:∧
7718:⋯
7715:∧
7658:…
7632:…
7619:∀
7595:∧
7592:⋯
7589:∧
7549:…
7530:≡
7514:…
7492:→
7451:∧
7448:⋯
7445:∧
7388:…
7362:…
7349:∀
7325:∧
7277:→
7250:→
7205:∀
7199:∧
7153:→
7126:→
7081:∀
7075:∧
7045:∀
6832:s within
6596:…
6575:φ
6559:…
6546:∃
6473:…
6450:Ψ
6417:…
6384:Ψ
6098:−
5616:…
5577:…
5561:φ
5539:…
5526:∃
5520:≡
5498:…
5447:…
5419:φ
5397:…
5384:∃
5378:≡
5345:∧
5337:−
5294:−
5264:…
5237:∀
5201:…
5163:…
5135:φ
5119:…
5106:∃
5075:…
5050:∀
5044:∧
5036:−
5025:⇐
4990:…
4970:−
4956:∃
4930:−
4916:…
4903:∀
4897:∧
4889:−
4878:⇐
4828:→
4825:φ
4779:∧
4776:⋯
4773:∧
4760:∧
4722:…
4709:∃
4634:…
4614:−
4580:−
4541:…
4513:φ
4445:…
4394:…
4372:Σ
4307:precedes
4282:…
4236:…
4214:Σ
4194:…
4172:Σ
4138:…
4116:Σ
4096:…
4074:Σ
4040:…
4008:…
3944:…
3918:…
3902:φ
3886:…
3873:∃
3854:…
3841:∀
3795:Ψ
3753:∣
3738:ψ
3720:∃
3708:∀
3678:φ
3675:¬
3639:∧
3619:∧
3590:ψ
3572:∃
3560:∀
3554:→
3551:ψ
3533:∃
3521:∀
3506:∀
3494:∀
3488:∧
3463:∣
3448:ψ
3430:∃
3418:∀
3401:∃
3384:∀
3375:¬
3352:Φ
3349:¬
3327:ψ
3309:∃
3297:∀
3252:∣
3237:ψ
3219:∃
3207:∀
3184:Φ
3181:¬
3156:Φ
3153:¬
3130:Φ
3127:¬
3107:Φ
3104:¬
3084:Φ
3064:Ψ
3044:φ
3024:φ
3021:→
3018:Φ
3015:∧
3012:Φ
3009:≡
3002:Φ
2998:≡
2995:Ψ
2971:Ψ
2947:Ψ
2924:Ψ
2921:≡
2914:Φ
2887:ψ
2884:→
2860:∧
2814:∃
2797:∃
2785:∀
2773:∀
2761:∀
2744:∀
2735:Ψ
2700:ρ
2696:∧
2693:ρ
2637:ρ
2619:∧
2616:ρ
2581:ψ
2578:→
2539:∃
2527:∀
2515:∀
2503:∀
2497:∧
2455:∃
2438:∀
2425:Φ
2395:ψ
2392:→
2353:∃
2341:∀
2335:≡
2329:ψ
2311:∃
2299:∀
2293:→
2226:∃
2214:∀
2188:φ
2185:→
2182:Φ
2174:Clearly,
2156:ψ
2138:∃
2126:∀
2120:→
2090:∀
2078:∀
2072:∧
2030:∃
2013:∀
2004:Φ
1940:…
1900:∀
1897:⋯
1884:∀
1871:∀
1845:∀
1799:φ
1779:ψ
1755:φ
1728:ψ
1710:∃
1698:∀
1686:∃
1674:∀
1665:φ
1624:ψ
1621:→
1592:∧
1536:∃
1524:∃
1512:∀
1500:∀
1488:∀
1471:∀
1420:φ
1400:ψ
1371:ψ
1353:∃
1341:∀
1329:∃
1317:∀
1308:φ
1247:φ
1223:φ
1203:φ
1173:Φ
1147:∃
1144:⋯
1128:−
1112:∃
1096:−
1080:∀
1077:⋯
1061:−
1045:∀
1039:⋯
1016:∃
1013:⋯
987:∃
961:∀
958:⋯
945:∀
936:φ
897:ψ
891:φ
856:¬
853:∨
832:∃
826:∀
788:¬
785:∨
767:∧
764:Φ
755:∃
740:∀
734:ψ
643:φ
640:¬
627:∀
624:⋯
611:∀
605:ψ
602:¬
566:φ
553:∃
550:⋯
537:∃
531:ψ
490:Theorem 2
476:being in
410:Theorem 2
398:Theorem 1
394:Theorem 2
390:Theorem 2
386:Theorem 1
224:= ∀
28:given by
8198:Gödel, K
8187:(1929).
8185:Gödel, K
7884:′
6255:n > k
6082:through
4363:. [Here
3771:′
3760:′
3481:′
3470:′
3408:′
3391:′
3270:′
3259:′
3005:′
2917:′
2853:′
2842:′
2804:′
2751:′
2719:, where
2703:′
2653:, where
2640:′
2629:′
2490:′
2479:′
2462:′
2445:′
2428:′
2065:′
2054:′
2037:′
2020:′
1965:Let now
1602:′
1585:′
1574:′
1563:′
1543:′
1478:′
1444:′(
1383:, where
818:. Since
669:sentence
667:to be a
5654:Now if
4261:, and
1290:Comment
659:, thus
590:and if
400:holds.
266:φ(
252:∃
245:∃
231:∀
130:∀
123:∀
119:∀
115:∃
111:∀
67:or the
8228:
8220:
3981:tuples
1922:where
1829:tuples
1743:where
1648:Proof.
1294:φ
1265:. Let
1193:degree
720:matrix
706:.. If
676:prefix
435:φ
374:φ
366:φ
344:holds.
177:φ
8275:Logic
8251:"—by
8226:S2CID
7903:Here
6745:Take
6702:as Φ(
5649:Lemma
4854:Proof
4811:Lemma
4163:, or
3821:Lemma
3692:Lemma
1263:Lemma
578:. If
6172:and
5285:<
4695:as
4112:<
4024:<
3663:and
3655:and
2939:Now
2671:(S')
2659:(S')
2657:and
1989:and
1977:and
1969:and
1833:e.g.
1823:and
712:(P)Φ
702:and
423:i.e.
113:and
8247:: "
8218:JFM
8210:doi
6985:...
6959:...
6933:...
6907:...
6766:...
6725:...
6709:...
6532:).
5357:φ.
4505:as
4359:in
3983:of
2936:.
2721:(T)
2667:(S)
2655:(S)
2257:or
1745:(P)
1438:Q'
1195:of
678:of
510:...
460:in
425:, (
384:If
287:...
273:...
8271::
8224:.
8216:.
8206:37
7961:Eq
7957:Eq
7017:.
7006:,
6871:,
6800:,
6774:+1
5832:.
4850:.
4817:,
4475:.
3694:.
3665:y'
3661:x'
3339:.
3170:)
1971:y'
1967:x'
1819:,
1815:,
1811:.
710:=
372:"¬
294:)
280:,
195:,
86:.
71:.
60:.
8255:.
8232:.
8212::
8136:k
8131:k
8127:B
8118:k
8113:1
8109:B
8105:,
8099:,
8094:1
8089:k
8085:B
8076:1
8071:1
8067:B
8044:k
8040:D
8017:i
8012:k
8008:B
7985:i
7943:m
7937:k
7917:Z
7911:A
7888:.
7838:]
7835:)
7832:)
7827:m
7823:y
7814:1
7810:y
7806:(
7803:Z
7797:)
7792:m
7788:x
7779:1
7775:x
7771:(
7768:Z
7765:(
7759:)
7756:)
7751:m
7747:y
7743:,
7738:m
7734:x
7730:(
7727:q
7724:E
7712:)
7707:1
7703:y
7699:,
7694:1
7690:x
7686:(
7683:q
7680:E
7677:(
7674:[
7671:)
7666:m
7662:x
7653:1
7649:y
7645:,
7640:m
7636:x
7627:1
7623:x
7616:(
7568:]
7565:)
7562:)
7557:k
7553:y
7544:1
7540:y
7536:(
7533:A
7527:)
7522:k
7518:x
7509:1
7505:x
7501:(
7498:A
7495:(
7489:)
7486:)
7481:k
7477:y
7473:,
7468:k
7464:x
7460:(
7457:q
7454:E
7442:)
7437:1
7433:y
7429:,
7424:1
7420:x
7416:(
7413:q
7410:E
7407:(
7404:[
7401:)
7396:k
7392:x
7383:1
7379:y
7375:,
7370:k
7366:x
7357:1
7353:x
7346:(
7304:]
7301:)
7298:)
7295:y
7292:,
7289:z
7286:(
7283:q
7280:E
7274:)
7271:x
7268:,
7265:z
7262:(
7259:q
7256:E
7253:(
7247:)
7244:y
7241:,
7238:x
7235:(
7232:q
7229:E
7226:[
7223:)
7220:z
7217:,
7214:y
7211:,
7208:x
7202:(
7180:]
7177:)
7174:)
7171:z
7168:,
7165:y
7162:(
7159:q
7156:E
7150:)
7147:z
7144:,
7141:x
7138:(
7135:q
7132:E
7129:(
7123:)
7120:y
7117:,
7114:x
7111:(
7108:q
7105:E
7102:[
7099:)
7096:z
7093:,
7090:y
7087:,
7084:x
7078:(
7072:)
7069:x
7066:,
7063:x
7060:(
7057:q
7054:E
7051:)
7048:x
7042:(
7015:φ
7011:2
7008:z
7004:1
7001:z
6995:m
6991:q
6987:z
6982:1
6979:q
6975:z
6973:,
6969:k
6965:p
6961:z
6956:1
6953:p
6949:z
6943:m
6939:q
6935:z
6930:1
6927:q
6923:z
6917:k
6913:p
6909:z
6904:1
6901:p
6897:z
6893:k
6888:j
6884:B
6880:k
6876:2
6873:z
6869:1
6866:z
6861:n
6857:D
6849:i
6847:n
6843:i
6838:n
6834:D
6829:j
6825:B
6821:k
6817:1
6814:B
6809:1
6806:n
6802:D
6798:1
6795:n
6790:j
6786:B
6782:j
6778:k
6772:m
6768:z
6764:3
6761:z
6759:,
6757:2
6754:z
6750:1
6747:B
6740:y
6736:x
6731:m
6727:y
6723:1
6720:y
6718:,
6715:k
6711:x
6707:1
6704:x
6699:i
6695:B
6671:n
6667:a
6646:)
6641:m
6637:y
6633:.
6630:.
6627:.
6622:1
6618:y
6614:,
6609:n
6604:k
6600:a
6591:n
6586:1
6582:a
6578:(
6572:)
6567:m
6563:y
6554:1
6550:y
6543:(
6518:k
6514:D
6493:)
6486:i
6482:u
6477:z
6466:1
6462:u
6457:z
6453:(
6430:)
6425:i
6421:u
6412:1
6408:u
6404:(
6358:k
6354:D
6328:n
6324:D
6313:n
6297:k
6293:D
6270:h
6266:E
6239:n
6235:D
6212:k
6208:B
6185:k
6181:D
6158:k
6154:B
6128:h
6124:E
6101:1
6095:h
6091:E
6068:1
6064:E
6053:n
6037:1
6033:E
6010:1
6006:E
5983:1
5979:E
5956:n
5952:D
5929:n
5925:D
5902:h
5898:E
5875:n
5871:D
5848:h
5844:E
5814:n
5810:D
5787:k
5783:B
5760:n
5756:D
5733:h
5729:E
5718:n
5714:n
5698:n
5694:D
5683:n
5667:n
5663:D
5635:)
5630:1
5627:+
5624:m
5620:z
5611:3
5607:z
5603:,
5598:2
5594:z
5590:,
5585:1
5581:z
5572:1
5568:z
5564:(
5558:)
5553:1
5550:+
5547:m
5543:z
5534:1
5530:z
5523:(
5517:)
5512:1
5509:+
5506:m
5502:z
5493:3
5489:z
5485:,
5480:2
5476:z
5472:,
5465:1
5460:k
5456:a
5451:z
5440:1
5435:1
5431:a
5426:z
5422:(
5416:)
5411:1
5408:+
5405:m
5401:z
5392:1
5388:z
5381:(
5373:1
5369:D
5340:1
5334:n
5330:D
5309:2
5306:+
5303:m
5300:)
5297:1
5291:n
5288:(
5282:)
5277:n
5272:k
5268:a
5259:n
5254:1
5250:a
5246:(
5243:)
5240:k
5234:(
5214:)
5209:m
5205:y
5196:1
5192:y
5188:,
5181:n
5176:k
5172:a
5167:z
5156:n
5151:1
5147:a
5142:z
5138:(
5132:)
5127:m
5123:y
5114:1
5110:y
5103:(
5100:)
5093:n
5088:k
5084:a
5079:z
5068:n
5063:1
5059:a
5054:z
5047:(
5039:1
5033:n
5029:D
5020:n
5016:B
5012:)
5007:1
5004:+
5001:m
4998:n
4994:z
4985:2
4982:+
4979:m
4976:)
4973:1
4967:n
4964:(
4960:z
4953:(
4950:)
4945:1
4942:+
4939:m
4936:)
4933:1
4927:n
4924:(
4920:z
4911:1
4907:z
4900:(
4892:1
4886:n
4882:D
4873:n
4869:D
4858:n
4836:n
4832:D
4815:n
4795:.
4792:)
4787:n
4783:B
4768:2
4764:B
4755:1
4751:B
4747:(
4744:)
4739:1
4736:+
4733:m
4730:n
4726:z
4717:1
4713:z
4706:(
4681:n
4677:D
4656:)
4651:1
4648:+
4645:m
4642:n
4638:z
4629:3
4626:+
4623:m
4620:)
4617:1
4611:n
4608:(
4604:z
4600:,
4595:2
4592:+
4589:m
4586:)
4583:1
4577:n
4574:(
4570:z
4566:,
4559:n
4554:k
4550:a
4545:z
4534:n
4529:1
4525:a
4520:z
4516:(
4491:n
4487:B
4463:)
4458:n
4453:k
4449:a
4440:n
4435:1
4431:a
4427:(
4407:)
4402:k
4398:x
4389:1
4385:x
4381:(
4376:k
4347:)
4342:k
4338:y
4334:.
4331:.
4328:.
4323:1
4319:y
4315:(
4295:)
4290:k
4286:x
4277:1
4273:x
4269:(
4249:)
4244:k
4240:y
4231:1
4227:y
4223:(
4218:k
4210:=
4207:)
4202:k
4198:x
4189:1
4185:x
4181:(
4176:k
4151:)
4146:k
4142:y
4133:1
4129:y
4125:(
4120:k
4109:)
4104:k
4100:x
4091:1
4087:x
4083:(
4078:k
4053:)
4048:k
4044:y
4035:1
4031:y
4027:(
4021:)
4016:k
4012:x
4003:1
3999:x
3995:(
3979:-
3977:k
3960:.
3957:)
3952:m
3948:y
3939:1
3935:y
3931:,
3926:k
3922:x
3913:1
3909:x
3905:(
3899:)
3894:m
3890:y
3881:1
3877:y
3870:(
3867:)
3862:k
3858:x
3849:1
3845:x
3838:(
3825:R
3775:)
3768:y
3764:,
3757:x
3750:y
3747:,
3744:x
3741:(
3735:)
3732:P
3729:(
3726:)
3723:v
3717:(
3714:)
3711:u
3705:(
3657:y
3653:x
3596:)
3593:)
3587:)
3584:P
3581:(
3578:)
3575:v
3569:(
3566:)
3563:u
3557:(
3548:)
3545:P
3542:(
3539:)
3536:v
3530:(
3527:)
3524:u
3518:(
3515:(
3512:)
3509:y
3503:(
3500:)
3497:x
3491:(
3485:)
3478:y
3474:,
3467:x
3460:y
3457:,
3454:x
3451:(
3445:)
3442:P
3439:(
3436:)
3433:v
3427:(
3424:)
3421:u
3415:(
3412:)
3405:y
3398:(
3395:)
3388:x
3381:(
3378:(
3324:)
3321:P
3318:(
3315:)
3312:v
3306:(
3303:)
3300:u
3294:(
3274:)
3267:y
3263:,
3256:x
3249:y
3246:,
3243:x
3240:(
3234:)
3231:P
3228:(
3225:)
3222:v
3216:(
3213:)
3210:u
3204:(
2985:M
2961:k
2890:)
2881:)
2878:y
2875:,
2872:x
2869:(
2866:Q
2863:(
2857:)
2850:y
2846:,
2839:x
2835:(
2832:Q
2829:)
2826:P
2823:(
2820:)
2817:v
2811:(
2808:)
2801:y
2794:(
2791:)
2788:u
2782:(
2779:)
2776:y
2770:(
2767:)
2764:x
2758:(
2755:)
2748:x
2741:(
2738:=
2707:)
2690:(
2687:)
2684:T
2681:(
2633:)
2626:S
2622:(
2613:)
2610:S
2607:(
2584:)
2575:)
2572:y
2569:,
2566:x
2563:(
2560:Q
2557:(
2554:)
2551:P
2548:(
2545:)
2542:v
2536:(
2533:)
2530:u
2524:(
2521:)
2518:y
2512:(
2509:)
2506:x
2500:(
2494:)
2487:y
2483:,
2476:x
2472:(
2469:Q
2466:)
2459:y
2452:(
2449:)
2442:x
2435:(
2432:=
2398:)
2389:)
2386:y
2383:,
2380:x
2377:(
2374:Q
2371:(
2368:)
2365:P
2362:(
2359:)
2356:v
2350:(
2347:)
2344:u
2338:(
2332:)
2326:)
2323:P
2320:(
2317:)
2314:v
2308:(
2305:)
2302:u
2296:(
2290:)
2287:y
2284:,
2281:x
2278:(
2275:Q
2272:(
2259:y
2255:x
2241:)
2238:P
2235:(
2232:)
2229:v
2223:(
2220:)
2217:u
2211:(
2159:)
2153:)
2150:P
2147:(
2144:)
2141:v
2135:(
2132:)
2129:u
2123:(
2117:)
2114:y
2111:,
2108:x
2105:(
2102:Q
2099:(
2096:)
2093:y
2087:(
2084:)
2081:x
2075:(
2069:)
2062:y
2058:,
2051:x
2047:(
2044:Q
2041:)
2034:y
2027:(
2024:)
2017:x
2010:(
2007:=
1991:y
1987:x
1983:Q
1979:y
1975:x
1948:n
1944:x
1935:1
1931:x
1908:n
1904:x
1892:2
1888:x
1879:1
1875:x
1851:)
1848:x
1842:(
1825:v
1821:u
1817:y
1813:x
1769:k
1725:)
1722:P
1719:(
1716:)
1713:v
1707:(
1704:)
1701:u
1695:(
1692:)
1689:y
1683:(
1680:)
1677:x
1671:(
1668:=
1652:k
1627:)
1618:)
1615:y
1612:,
1609:x
1606:(
1599:Q
1595:(
1589:)
1582:y
1578:,
1571:x
1567:(
1560:Q
1556:)
1553:P
1550:(
1547:)
1540:y
1533:(
1530:)
1527:v
1521:(
1518:)
1515:u
1509:(
1506:)
1503:y
1497:(
1494:)
1491:x
1485:(
1482:)
1475:x
1468:(
1458:k
1454:y
1450:y
1448:,
1446:x
1442:Q
1434:k
1397:)
1394:P
1391:(
1368:)
1365:P
1362:(
1359:)
1356:v
1350:(
1347:)
1344:u
1338:(
1335:)
1332:y
1326:(
1323:)
1320:x
1314:(
1311:=
1298:k
1283:k
1279:R
1275:k
1271:R
1267:k
1176:)
1170:(
1167:)
1160:n
1156:k
1151:x
1139:1
1136:+
1131:1
1125:n
1121:k
1116:x
1109:(
1106:)
1099:1
1093:n
1089:k
1084:x
1072:1
1069:+
1064:2
1058:n
1054:k
1049:x
1042:(
1036:)
1029:2
1025:k
1020:x
1008:1
1005:+
1000:1
996:k
991:x
984:(
981:)
974:1
970:k
965:x
953:1
949:x
942:(
939:=
923:R
919:R
894:=
871:)
868:)
865:z
862:(
859:F
850:)
847:y
844:(
841:F
838:(
835:z
829:y
806:)
803:]
800:)
797:z
794:(
791:F
782:)
779:y
776:(
773:F
770:[
761:(
758:z
752:)
749:P
746:(
743:y
737:=
724:φ
716:φ
708:φ
704:z
700:y
696:φ
692:F
688:φ
684:φ
680:φ
665:φ
661:φ
657:φ
635:n
631:x
619:1
615:x
608:=
592:ψ
588:φ
584:M
580:ψ
561:n
557:x
545:1
541:x
534:=
521:φ
516:n
512:x
508:1
505:x
501:φ
494:φ
486:ψ
482:ψ
474:ψ
472:(
470:ψ
466:φ
458:ψ
450:φ
431:ψ
427:φ
419:C
415:C
364:"
342:φ
337:n
333:D
326:φ
322:B
318:n
316:(
313:n
309:D
291:m
289:y
284:1
282:y
277:k
275:x
270:1
268:x
263:m
261:y
256:2
254:y
249:1
247:y
242:k
240:x
235:2
233:x
228:1
226:x
222:B
211:)
208:m
204:y
200:1
197:y
192:k
188:x
184:1
181:x
179:(
173:m
169:y
165:2
162:y
158:1
155:y
150:k
146:x
142:2
139:x
135:1
132:x
125:.
109:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
