At 07:09 30/11/04 -0800, James N Rose wrote:

If there any viable system in which you -can- both derive, and find useful application for, the equation 0=1 ?

Of course there is. (As I said it all depends of the beliefs and the deduction rule).

Here is one theory. Just the axiom: 0=1. No rules of inference!

`Semantics: INTERPRETATION("0") = The money you will send me soon.`

INTERPRETATION("1") = 42 billion euros (usual meaning of 42, ...)

INTERPRETATION("=") = usual equality.

INTERPRETATION("1") = 42 billion euros (usual meaning of 42, ...)

INTERPRETATION("=") = usual equality.

0=1 is derivable in that theory!

`A yes! It is not a theory of everything (TOE) but I do find that that theory could`

have some application!

have some application!

`°°°°°°°°°°°°°°°°°°`

Let me give you one of my (oldest) favorite TOE (discovered by Schoenfinkel in 1924):

Let me give you one of my (oldest) favorite TOE (discovered by Schoenfinkel in 1924):

`There is just two atomic term S and K.`

A general term is either a variable or an atomic term or a compound (term term).

A general term is either a variable or an atomic term or a compound (term term).

And two deduction rule: ((Kx)y) gives x (((Sx)y)z) gives ((xz)(yz))

`Exercice: find a closed term (that is a term without variable) such that applied`

to x, it gives x. Solution: ((SK)K) (indeed (((SK)K)x) gives ((Kx)(Kx)) by the

second rule, and now ((Kx)(Kx)) gives x, by the first rule.

to x, it gives x. Solution: ((SK)K) (indeed (((SK)K)x) gives ((Kx)(Kx)) by the

second rule, and now ((Kx)(Kx)) gives x, by the first rule.

`Exercice: find a closed term which emulate the universal dovetailer. That is find`

a term with only K and S which does the emulation when the rule above are applied

in some fixed order.

a term with only K and S which does the emulation when the rule above are applied

in some fixed order.

`K and S are Schoefinkel combinators. They are a shortcut between the abstraction`

and application. When typed then leads to categorical description of the first persons.

Untyped they give aspects of platonia; and some partial control.

Combinators eliminate the need of variable in programs. (Like ((SK)K) compute

the identity function).

and application. When typed then leads to categorical description of the first persons.

Untyped they give aspects of platonia; and some partial control.

Combinators eliminate the need of variable in programs. (Like ((SK)K) compute

the identity function).

`We could use it to help making things clear?`

Here to, Raymond Smullyan wrote a little chef-d'oeuvre: "To Mock a Mockingbird" (1985).

(It is not a coincindence!).

Here to, Raymond Smullyan wrote a little chef-d'oeuvre: "To Mock a Mockingbird" (1985).

(It is not a coincindence!).

Bruno

http://iridia.ulb.ac.be/~marchal/