4 ms·

Can you explain the fixed point idea more in a beginner way? I'm curious to understand the result.

vorotato 9y ago
A function has a fixed point when for some value of x, x = f(x). This is interesting because it's some change, that doesn't change the result. in the lingua franca of javascript. var timesThree = (x => x * 3) //for this function 0 is a fixed point... var a = 0 console.log(a == timesThree(a)) //7 is not a fixed point var b = 7 console.log(b == timesThree(b))
- hackernewsacct 9y ago
  Thanks for the response. My question is how does fixed point relate to the incomplete theorems and decidability?
  - darkinvisible 9y ago
    The key to e.g. Goedel's results is the Fixed Point Lemma: if ψ is a formula with v free then there is a sentence φ such that, provably, φ <=> ψ(<φ>) [where <..> is the numerical code of .. ]. The proof, if you are interested, is not difficult. Let sub be the function that describes, via codes, substituting the (numeral n_ of the number) n for a free variable v of a formula χ : sub(<χv>, n_) = <χn_>. Then the PROOF is: consider ψ(sub(v,v)), call it θv, let m be <θv> and let φ be θm_. Then, provably, φ <=> ψ(sub(m_,m_)) <=> ψ(sub(<θv>,m_)) <=> ψ(<θm_>) <=> ψ(<φ>). Ta-da! Goedel used this to get the "formula that says I am not provable", φ <=> not Prov(<φ>).
mafribe 9y ago
explain the fixed point idea The Yanofsky paper explains is in quite gentle a manner. The key insight behind Lawvere's abstract framework to paradoxa is the the general existence of certain fixpoints. Definition. We say that a set B has the fixpoint property if any function f:B→B has a fixpoint (i.e. f b = b for some b in B). With this convenient definition, we are now ready to state and prove Lawvere's ridiculously simple and yet great theorem. Theorem (Lawvere). If e:A→(A→B) is a surjective function, then B has the fixed point property. The proof is quite easy. Let e:A→(A→B) be surjective. We have to show that B has the fixpoint property. That means for every f:B→B there is b∈B such that f(b)=b. Choose a function f:B→B and define the function g:A→B by setting a ↦ f (e a a) As e is surjective, there must be a0∈A such that e a0 = g. But then immediately f (g a0) = f (e a0 a0) = g a0 Hence g a0 is a fixpoint of f's. Now many/most paradoxa are special cases of Lawvere's theorem. But for each paradox, the specific functions involved are a bit different. Let's look at an example. Theorem (Cantor). There is no surjection e:A→Pow(A). To see why this is true, note that Pow(A) is isomorphic to A→Bool. But there is a function on Bool that has no fixpoints, for example negation ¬:Bool→Bool, contradicting Lawvere's theorem. --------------- What is the intuition behind Lawvere's theorem? At first worrying about A→(A→Bool) is a bit surprising. What does that have to do with paradoxa and self-reference? Well, what does it mean that A can speak about itself? To approach an answer, we could maybe first ask a simpler question: what does it mean to speak about A? How about this for an answer: to speak about A means to say something about A's elements. What does it mean to say something about A's elements? Maybe stating whether any given element a∈A has a property of interest? But what's a property? Easy: a property of A's elements is a function p:A→Bool But we don't want just a fixed property, we want arbitrary properties. To do so, we have to consider the function space A→Bool And how can we turn this into self-reference? What if each element a in A corresponded to a property over A? In other words, (with a lot of handwaving) self-reference means the existence of a surjective function A→(A→Bool) The next step is to wonder: why Bool? Why not any old set? Note that Cantor's theorem continues to hold if we replace Bool with a larger set, but does not hold, if B in A→(A→B) has cardinality 1. What Bool and larger sets have in common is that we can rearrange them, i.e. there is a permuation that doesn't have a fixpoint.
- ScottBurson 9y ago
  Fascinating! A couple of questions: Are there any non-singleton sets with the fixpoint property? > a ↦ f (e a a) Don't you mean a ↦ e a a ? Because later you expand (g a0) to (e a0 a0).
  - mafribe 9y ago
    No, g is given by a ↦ f (e a a). The expansion you refer to works because e a0 = g.

A function has a fixed point when for some value of x, x = f(x). This is interesting because it's some change, that doesn't change the result. in the lingua franca of javascript. var timesThree = (x => x * 3) //for this function 0 is a fixed point... var a = 0 console.log(a == timesThree(a)) //7 is not a fixed point var b = 7 console.log(b == timesThree(b))

hackernewsacct 9y ago
Thanks for the response. My question is how does fixed point relate to the incomplete theorems and decidability?
- darkinvisible 9y ago
  The key to e.g. Goedel's results is the Fixed Point Lemma: if ψ is a formula with v free then there is a sentence φ such that, provably, φ <=> ψ(<φ>) [where <..> is the numerical code of .. ]. The proof, if you are interested, is not difficult. Let sub be the function that describes, via codes, substituting the (numeral n_ of the number) n for a free variable v of a formula χ : sub(<χv>, n_) = <χn_>. Then the PROOF is: consider ψ(sub(v,v)), call it θv, let m be <θv> and let φ be θm_. Then, provably, φ <=> ψ(sub(m_,m_)) <=> ψ(sub(<θv>,m_)) <=> ψ(<θm_>) <=> ψ(<φ>). Ta-da! Goedel used this to get the "formula that says I am not provable", φ <=> not Prov(<φ>).

mafribe 9y ago

explain the fixed point idea The Yanofsky paper explains is in quite gentle a manner. The key insight behind Lawvere's abstract framework to paradoxa is the the general existence of certain fixpoints. Definition. We say that a set B has the fixpoint property if any function f:B→B has a fixpoint (i.e. f b = b for some b in B). With this convenient definition, we are now ready to state and prove Lawvere's ridiculously simple and yet great theorem. Theorem (Lawvere). If e:A→(A→B) is a surjective function, then B has the fixed point property. The proof is quite easy. Let e:A→(A→B) be surjective. We have to show that B has the fixpoint property. That means for every f:B→B there is b∈B such that f(b)=b. Choose a function f:B→B and define the function g:A→B by setting a ↦ f (e a a) As e is surjective, there must be a0∈A such that e a0 = g. But then immediately f (g a0) = f (e a0 a0) = g a0 Hence g a0 is a fixpoint of f's. Now many/most paradoxa are special cases of Lawvere's theorem. But for each paradox, the specific functions involved are a bit different. Let's look at an example. Theorem (Cantor). There is no surjection e:A→Pow(A). To see why this is true, note that Pow(A) is isomorphic to A→Bool. But there is a function on Bool that has no fixpoints, for example negation ¬:Bool→Bool, contradicting Lawvere's theorem. --------------- What is the intuition behind Lawvere's theorem? At first worrying about A→(A→Bool) is a bit surprising. What does that have to do with paradoxa and self-reference? Well, what does it mean that A can speak about itself? To approach an answer, we could maybe first ask a simpler question: what does it mean to speak about A? How about this for an answer: to speak about A means to say something about A's elements. What does it mean to say something about A's elements? Maybe stating whether any given element a∈A has a property of interest? But what's a property? Easy: a property of A's elements is a function p:A→Bool But we don't want just a fixed property, we want arbitrary properties. To do so, we have to consider the function space A→Bool And how can we turn this into self-reference? What if each element a in A corresponded to a property over A? In other words, (with a lot of handwaving) self-reference means the existence of a surjective function A→(A→Bool) The next step is to wonder: why Bool? Why not any old set? Note that Cantor's theorem continues to hold if we replace Bool with a larger set, but does not hold, if B in A→(A→B) has cardinality 1. What Bool and larger sets have in common is that we can rearrange them, i.e. there is a permuation that doesn't have a fixpoint.

ScottBurson 9y ago
Fascinating! A couple of questions: Are there any non-singleton sets with the fixpoint property? > a ↦ f (e a a) Don't you mean a ↦ e a a ? Because later you expand (g a0) to (e a0 a0).
- mafribe 9y ago
  No, g is given by a ↦ f (e a a). The expansion you refer to works because e a0 = g.