At 22:43 27/08/04 -0700, George Levy wrote:

I am trying to visualize Lob formula as a block diagram to be implemented either in neural net, as computer program or as a digital cicuit. Digital circuits have the advantage of being very simple (binary) so let's try to express Lob's formula as a truth table that could be implemented with NAND gates.

Let's write Lob's formula as B2(B1p -> p) -> B1p
where B1, B2, and p are binary variables.

I am not sure I understand. It is better to see B as a (non truth functional) connector.

Note that B1 applies to p and B2 applies to the implication (B1p -> p). (Should I have done this differently?)
~ = NOT
+ = OR
. = AND

We can convert the implication B1p -> p   to    ~(B1.p) + p

The Boolean equivalent to Lob is

 ~B2(~(B1p)+ p) + B1p

The truth table is

B2   B1   p    B1p    ~B1p+p      ~B2(~(B1p)+ p))      ~B2(~(B1p)+ p) + B1p

0 0 0 0 1 1 1
0 0 1 0 1 1 1
0 1 0 0 1 1 1
0 1 1 1 1 1 1
1 0 0 0 1 0 0
1 0 1 0 1 0 0
1 1 0 0 1 0 0
1 1 1 1 1 0 1

I am now confused. The fifth column ~B1p+p surprisingly is all 1's. The last column ~B2(~(B1p)+ p) + B1p which is Lob's statement and which I expected to be all 1's is not. I have rechecked this table and I don't see anything wrong. Is there something wrong?

It may be that Boolean algebra is not adequate to express Lob. The question is how can Lob's formula be expressed simply by a digital circuit a block diagram or a neural net?

By making a system enough rich to represent B, like Godel did show
for provability in arithmetic. It is more comparable to a (lisp) interpretor
described in Lisp. In terme on electrical or neuronal nets it means it will
have feedback loops. Modal logic is not truth functional. You need delay and
close circuits (like flip-flop).
Boyer, if I remember well, as explicitly build Lobian theorem prover.
Smullyan presents toy systems in chapter 26 and 27 of FU. Of course
any reasonable formalisation of arithmetic is enough, so any universal
machine is Lobian extendible.


Reply via email to