5
votes
1answer
201 views

Can the proof of fixed point theorems ever be constructive?

Overall, Brouwer fixed point theorem and Kakutani fixed theorem are non-constructive. Is there any established paper that demonstrates that there exists constructive proofs that do exactly what these ...
4
votes
1answer
37 views

Transforming Nested Fixed-Point Formulas into Infinitary Logic Formulas with Finitely many Variables

There is a definition (actually a description of how it could be defined) of a fixed-point logic formula. The formula is in inflationary fixed point logic (IFP) in this case but it could also be ...
3
votes
2answers
285 views

Proving and understanding the Fixed point lemma (Diagonal Lemma) in Logic - used in proof of Godel's incompleteness theorem

http://en.wikipedia.org/wiki/Diagonal_lemma I am wondering about the proof of the "Fixed-Point Lemma" $\text{Mod } \Sigma$ is the class of all models of $ \Sigma$. $\text{Th Mod } \Sigma$ is the set ...
3
votes
1answer
81 views

Brouwer's fixed point theorem for infinite dimensional real space in subsystems of second order arithmetic

$\text{WKL}_0$ proves Brouwer's fixed point theorem for continuous functions on $\lbrack 0,1 \rbrack^n$, when $n$ is finite. What subsystem of second order arithmetic is needed to prove Brouwer's ...
2
votes
1answer
161 views

Differences between between concepts related to Gödel's Incompleteness theorems: self-referencing, diagonalization and fixed point theorem?

I am studying the proof of Gödel's first Incompleteness theorem at the moment and I don't understand the differences between self-referencing, diagonalization and fixed point related to Gödel's proof. ...
8
votes
1answer
332 views

Common knowledge as a fixed point

I read on a wikipedia page that from the modal logic formalization CK can be formulated as a fixed point. If it also holds for the set theory formalization? If it does, where I can find about it? ...