On 19 Aug 2011, at 23:32, meekerdb wrote:

On 8/19/2011 2:18 AM, Bruno Marchal wrote:So do you have a LISP program that will make my computer Lobian?It would be easier to do it by hands:1) develop a first order logic specification for your computer(that is a first order axiomatic for its data structures, includingthe elementary manipulations that your computer can do on them)2) add a scheme of induction axioms on those data structure. Forexample, for the combinators, it would be like this"if P(K) and P(S) and if for all X and Y P(X) & P(Y) impliesP((X,Y)) then for all X and Y P((X,Y))". And this for all "P"describable in your language.Just to clarify P is some predicate, i.e. a function that returns #Tor #F and X and Y are some data stuctures (e.g. lists) and ( , ) isa combinator, i.e. a function from DxD =>D for D the domain of X andY. Right?

`Predicate are more syntactical object. They can be interpreted as`

`function or relation, but in logic we distinguish explicitly the`

`syntax and the semantics. So an arithmetical predicate is just a`

`formula written with the usual symbols. Its intended meaning will be`

`true or false, relatively to some model. For example, the predicate "x`

`is greater than y" is "Ez(y+z = x)".`

`The semantics of combinators is rather hard, and it took time before`

`mathematicians find one. D^D needs to be isomorphic to D, because`

`there is only one domain (the collection of all combinators). But Dana`

`Scott has solved the problem, and found a notion of continuous`

`function making D^D isomorphic with D. Recursion theory provides also`

`an intuitive model, where a number can be seen both as a function and`

`a number: just define a new operation on the natural numbers: "@" by i`

`@ j = phi_i(j). It is a bit nasty, given that such an operation will`

`be partial (in case phi_i(j) does not stop).`

Bruno

BrentIt will be automatically Löbian. And, yes, it should not be todifficult to write a program in LISP, doing that. That is, startingfrom a first order logical specification of an interpreter,extending it into a Löbian machine.Bruno--You received this message because you are subscribed to the GoogleGroups "Everything List" group.To post to this group, send email to everything-list@googlegroups.com.To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com.For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.

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@googlegroups.com. To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.