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.