On 24 Sep 2014, at 12:00, Alberto G. Corona wrote:
I still don't know what this theorem add to common sense. I mean,
what it add out of his universe of formalizations in order to better
formalize the obvious.
It is not obvious at all. Replace p by false, and you get the
incompleteness theorem: <>t -> <>[]f (if I am consistent, then it is
consistent that I am inconsistent).
It is a theorem in the math of self-reference.
In the other side, using the curry-howard isomorphism in which for
each theorem there is a program:
http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html
I understand the curry-howard isomorphism for intuitionist logic. For
classical logic, there are different extensions of the idea, and I
have not yet arrive to a definite opinion.
What you describe below seems interesting, and when I have more time,
I will take a look. It might not fit with my own way to see the
propositions of G and G* as type. This is not an easy subbranch for me.
This people found the type of a program in the haskell language that
is isomorphic. The loeb formula:
loeb :: Functor a => a (a x -> x) -> a x
Which indeed can be used to compute spreadsheets using lazy
evaluation. That is, to calculate/prove the value of a cell written
as an expression that is a function of the values of other cells and
so on.
Compared with löb :
□(□P→P)→□P
in the formula 'a' means "the solution for". In this case 'a x' is
a list of the values of the cells. and it tells that "if you give me
a list of expressions , each one a function of the resulting values,
I will return the list of resulting values.
That is not uninteresting.
The above expression are the types of the parameters
The complete formula is:
loeb :: Functor a => a (a x -> x) -> a x
loeb x = fmap (\a -> a (loeb x)) x
where 'fmap' is a haskell function that match with the parameter
types and loeb is called recursively. The expression was found
almost experimentally, without knowing well what the final result was.
I created a real spreadsheet-like program using haskell running in a
web browser that uses the loeb expression and it works as expected:
It is interesting, senn as some attempt, and I am afraid it could take
a lot of time (notably for me) to see the significance of this.
Krivine (a french logician) similarly implemented the "Gödel's
incompleteness theorem", seen as a type, and a program, but I am not
yet well versed in that part of logic to be convinced he got the
"natural" part, which in the "theological context of computationalism"
the type should be motivated by self-reference and he mind-body
problem. The meaning of the Curry-Howard isomorphism still eludes me
in the classical logic context.
It was a permanent subject of discussion with my late friend Eric
Vandenbussche, he was far better than me on that.
Bruno
http://tryplayg.herokuapp.com/try/spreadsheet.hs/edit
2014-09-22 13:56 GMT+02:00 Telmo Menezes <[email protected]>:
http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%83%C6%92%C3%86%E2%80%99%C3%83%E2%80%A0%C3%A2%E2%82%AC%E2%84%A2%C3%83%C6%92%C3%A2%E2%82%AC%C5%A1%C3%83%E2%80%9A%C3%82%C2%B6bs_theorem/
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
--
Alberto.
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
