Kleene fixed-point theorem: Difference between revisions

Content deleted Content added
fix reference url
Citation bot (talk | contribs)
Altered volume. Add: doi, issue, authors 1-1. Removed parameters. Some additions/deletions were parameter name changes. | Use this bot. Report bugs. | Suggested by Abductive | Category:Order theory | #UCB_Category 105/179
 
(8 intermediate revisions by 7 users not shown)
Line 1:
{{Short description|Theorem in order theory and lattice theory}}
{{otheruses4|Kleene's fixed-point theorem in lattice theory|the fixed-point theorem in computability theory|Kleene's recursion theorem}}
[[File:Kleene fixpoint svg.svg|thumb|Computation of the least fixpoint of ''f''(''x'') = {{sfrac|1|10}}''x''<sup>2</sup>+[[arctangent|atan]](''x'')+1 using Kleene's theorem in the real [[interval (mathematics)|interval]] [0,7] with the usual order]]
 
In the [[mathematics|mathematical]] areas of [[order theory|order]] and [[lattice theory]], the '''Kleene fixed-point theorem''', named after American mathematician [[Stephen Cole Kleene]], states the following:
 
Line 16 ⟶ 17:
 
Although [[Tarski's fixed point theorem]]
does not consider how fixed points can be computed by iterating ''f'' from some seed (also, it pertains to [[monotone function]]s on [[complete lattices]]), this result is often attributed to [[Alfred Tarski]] who proves it for additive functions .<ref>{{cite journal | author=Alfred Tarski | url=http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.pjm/1103044538 | title=A lattice-theoretical fixpoint theorem and its applications | journal = [[Pacific Journal of Mathematics]] | volume=5:2 | year=1955 | issue=2 | pages=285&ndash;309| doi=10.2140/pjm.1955.5.285 }}, page 305.</ref> Moreover, the Kleene Fixedfixed-Pointpoint Theoremtheorem can be extended to [[monotone function]]s using transfinite iterations .<ref>{{cite journal | author=Patrick Cousot and Radhia Cousot | url=https://projecteuclid.org/euclid.pjm/1102785059 | title=Constructive versions of Tarski's fixed point theorems | journal = Pacific Journal of Mathematics | volume=82:1 | year=1979 | issue=1 | pages=43&ndash;57| doi=10.2140/pjm.1979.82.43 }}</ref>.
 
== Proof ==
== ProofSource:<ref>{{Cite book|title=Mathematical Theory of Domains by V. Stoltenberg-Hansen|lastlast1=Stoltenberg-Hansen|firstfirst1=V.|last2=Lindstrom|first2=I.|last3=Griffor|first3=E. R.|publisher=Cambridge University Press|year=1994|isbn=0521383447|___location=|pages=[https://archive.org/details/mathematicaltheo0000stol/page/24 24]|language=en|doi=10.1017/cbo9781139166386|quote=|url=https://archive.org/details/mathematicaltheo0000stol/page/24}}</ref> ==
 
We first have to show that the ascending Kleene chain of <math>f</math> exists in <math>L</math>. To show that, we prove the following: