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 [EMAIL PROTECTED]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at 
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---

Reply via email to