Le 05-déc.-07, à 23:08, Mirek Dobsicek a écrit :
"But thanks to that crashing, *Church thesis remains consistent*. I
would just say "An existence of a universal language is not ruled out".
I am ok with you. Consistent (in math) means basically "not rule out".
"Formally consistent" means "not formally ruled out", or "not
refutable".
That is:
"Consistent(p") is the same as "~ Provable(~ p)" " ~" = negation
like "Provable(p)" is equivalent with "~ Consistent( ~ p)"
Some thoughts:
Thanks to Godel "completeness" theorem for the first order theory
(1930) you can also read consistent(p) by there is a world satisfying p
(a world "where" p is true).
This relates a syntactical notion (the non existence of a chain of
formula derived from the axioms by the use of the inference rules and
ending with f) with a semantical: the existence of a mathematical
structure satisfying the formula.
At least in the frame of many formal classical theories, it is related
to the recurrent modal duality:
Permitted p <====> ~ Obligatory ~p
Obligatory p <====> ~ Permitted ~p
Somewhere p <====> ~ Everywhere ~p
Everywhere p <====> ~ Somewhere ~p
Sometimes p <====> ~ Always ~p
Always p <====> ~ Sometimes ~p
Like the usual first order quantifiers: (Ax = for all x; Ex = it exists
a x)
Ex F(x) <====> ~ Ax ~ F(x)
Ax F(x) <====> ~ Ex ~F(x)
(all cats are ferocious <====> it does not exist a non ferocious cat)
And with formal provability we have also:
Consistent p <====> ~ provable ~p
Provable p <====> ~ consistent ~p
But yes, it is by allowing the machine to crash, and actually by
allowing it to crash in a *necessarily* not always predictible way,
which makes it possible to be universal.
In a nutshell: Universality ==> insecurity ====> kicking back reality
and then
(knowledge of your universality) ==> (knowledge of your relative
insecurity) ====> (knowledge of a kicking back reality) ===>
anticipating an independent "reality"
(knowledge of your universality) = lobianity (this I intend to explain
later)
Mirek asked also in trhe same post:
<<And my last question, consider the profound function
f such that f(n) = 1 if there is a sequence of n consecutive fives in
the decimal expansion of PI, and f(n) = 0 otherwise
Is this an example of a partial computable function?>>
Yes.
<<Or is this function
as such already considered as un-computable function?>>
It could be uncomputable on some value, that is, everywhere the
function has value 1, you can in principle compute it (just search the
sequence: if it exists you will find it because PI is constructive). If
the value is zero, it could be that you will be able to know it, but it
could be that you will never know it ...
* * *
Something else:
Mirek, Brent, Barry, Tom (and all those inclined to do a bit of math):
don't read what is following unless you don't want to find the crashing
combinators by yourself.
I give the solution for the crashing combinators: it is enough to ...
mock a mockingbird.
Raymond Smullyan calls "mocking bird" a combinator M such that Mx = xx.
It is a sort of diagonalisor or duplicator. Now if you apply M on
itself, M, that is if you evaluate MM, this matches the left of
equation Mx = xx, so MM gives MM gives MM gives MM gives MM ...
(crashing!).
But does M exists? If you recall well, we know only the existence of K
and S, and their descendants: like KK, KS, S(KS), SK(KS)(S(KK)), ...
(Recall we don't write any left parenthesis, but something like
SK(KS)(S(KK)) really abbreviate the result of applying (SK) to (KS)
i.e. ((SK)(KS)) on (S(KK)), i.e.
(((SK)(KS))(S(KK))). each combinator can be thought as a function of
one variable (itself varying on the combinators).
We search a combinator playing the role of M (defined by its behavior
Mx = xx).
We have only K, S, and their combinations. And we have the two axioms
giving the behavior of K and S.
Kxy = x K axiom
and
Sxyz = xz(yz) S axiom
Explanation. You can see K as a projector sending (xy) on x, for any y.
(imo it is the *subjective* entity per excellence, in particular K
discards or eliminate informations like projection does. Church will
not allow K or any eliminators in its main systems).
Functionally K is Lx Ly . x The variable y is abstracted in some
irrelevant way.
We want Mx = xx.
But xx does not match either x or xz(yz), so that we could use the
axioms above directly.
But imagine we dispose of the subroutine combinators I such that Ix =
x. The identity combinators. Then Mx = xx = Ix(Ix), and this does match
xz(yz), so that Ix(Ix) is really SIIx (in Sxyz = xz(yz), so SIIx =
Ix(Ix) = xx. So SII can play the role of M, it behaves like M. We could
define M by SII.
Let us verify MM = SII(SII) does crash the system:
SII(SII) = I(SII)(I(SII)) = SII(SII) = I(SII)(I(SII)) = SII(SII) =
I(SII)(I(SII)) = SII(SII) = I(SII)(I(SII)) = SII(SII) = ... (crashing).
Now we have to still find an identity combinator I such that Ix = x.
Now x does match the right of the first axiom Kxy = x. Except that K on
x wait for a second argument. So let us give to it a second argument
such that we get something matching the second (S) axiom:
x = Kx(Kx) = SKKx
So SKK does the job. So we can take I = SKK.
So M = SII = S(SKK)(SKK)
and a crashing expression, sometimes called INFINITY is given by
MM = SII(SII) = S(SKK)(SKK)(S(SKK)(SKK))
So, a solution was
S(SKK)(SKK)(S(SKK)(SKK))
Remark:
Note that an existential quantification "ExP(x)" is a sort of
projection too. Eventually, the lobian machine observation-act-decision
is just that: projection by elimination of worlds (elimination of
accessibility of possibilities, a bit like when you get married, of get
a job, etc ....).
Bruno
http://iridia.ulb.ac.be/~marchal/
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to everything-list.domain.name.hidden
To unsubscribe from this group, send email to everything-list-unsubscribe.domain.name.hidden
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Wed Feb 06 2008 - 10:40:59 PST