Bruno, here is my "out of order and off topic" remark.
We are here in theoretical theorizing by theory-laden theoretic ways.
It is ALL the product of a mental exercise. Even a Loebian kick in
the ass can be a theoretical halucination.
"... - ...
But does 'M" exist? ,,, - ..."
(Never mind in what context. )
"exist" is a hard word. Contemplating in a generalized way, I would say:
"Everything (not in Hal's sense) exists what we THINK of, if not
otherwise: in our ideas.
Does 'K' or 'S' have a better than mental existential veracity? We can
think of a symbol that it does or does not exist, it does not change
that it DOES indeed exist in our mental domain.
Do you have a better 'domain' (e.g. a physical existence)? I doubt.
In our 1st person world it would not make sense.
Excuse my rambling and please, consider it 'entertainment' rather than
On Wed, Feb 6, 2008 at 10:40 AM, Bruno Marchal <[EMAIL PROTECTED]> wrote:
> 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
> 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
> 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?>>
> <<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 ...
> 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
> 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
> 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 ....).
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