// tableau for godel-lob provability logic \l parse \l display parse:.parse.p unparse:.parse.u / t=tree, s=state, p=parent, w=wff prove:{[w]valid[w]outer truth[_n;state w:$[4:w;,w;w]]} state:{[w].+(`t`s`p`w;++(0,!-1+#w;0;0N;(inner parse@)'negate w))} monad:{[f;t;w]$[5=4:w;@[w;`w;_f[f;t]];~4:w;_f[f;t]'w;w _in f;t f?w;@w;w;_f[f;t]'w]} outer:monad["012";("~:";"&:";"|:")] inner:monad[("~:";"&:";"|:");"012"] negate:{[w].[w;-1+#w;"~",]} valid:{[w;s]`0:(,""),v'[w],(,"---"),,$`invalid`valid validate s;s} validate:{[s]$[@s;&/2=s[`s]leaves s`t;&/_f's 1]} truth:{[r;s]$[open z:close@true/s;modal[r]z;z]} open:{[s]~&/2=s[`s;leaves s`t]} true:{[s]$[#i:unchecked . s`w`s;add/[s;i];s]} unchecked:{[w;s]order[w;&~s|~in'w]} order:{[w;i]i@>ab'w i} ab:{[w]a~!#a:f[rule w][w]1} leaves:{[t]$[1<#t;(!#t)_dvl?t;t]} in:{[w](#o)>rule w} rule:{[w]({x~(#x)#,//w}'o)?1} add:{[s;i].[append[s;i]. f[rule w]w:s[`w]i;(`s;i);:;1]} append:{[s;i;w;j]$[#j;@[s;_n;,;rows[s;i;w]j];s]} rows:{[s;i;w;j]++(nodes[s`t;l]j;&n;i;(n:(#w)*#l:on[s]i)#w)} on:{[s;i]l@&i _in's[`t]\'l:leaves s`t} nodes:{[t;l;j]@[-1+(#t)+!c;&~(c:(#l)*#j)#j;:;l@&(#l)##&~j]} modal:{[r;s]$[r~s;s;s~t:worlds s;s;(s;truth[s]'?t)]} worlds:{[s]$[~#i:&(~s`s)&"01"~/:(2#,//)'s`w;s;world[s]'i]} world:{[s;i]under[base[s]i;,/boxd s`w]i} base:{[s;i].+(`t`s`p`w;(&2;&2;2#i;(n;b)@\:s[`w][i][1;1]))} under:{[t;w;i]$[#w:?w _dvl t`w;@[t;_n;,;++(1+!#w;0;i;w)];t]} boxd:{[w]unbox'w@&"1"=*:'w} unbox:{[w](w;w 1)} close:{[s]cross/[s;leaves s`t]} cross:{[s;l].[s;(`s;l);:;2*contra s[`w;s[`t]\l]]} contra:{[w]$["@"_in w;1;|/&/'+(w;n'w)_lin\:w]} a:{$[1=#x;*x;x]} n:{[w]k@$["@"~w;"0@";"0@"~w;"@";("0";a w)]} v:{[w]"",w} k:{[w]$["00"~2#,//w;k w[1;1];w]} b:{[w]("1";w)} o:(,"&";"0&";,"|";"0|";,"/";"0/";,"~";"0~";"00";,"2") f:({[w](v'w 1 2;!2)} {[w](n'w[1;1 2];&2)} {[w](v'w 1 2;&2)} {[w](n'w[1;1 2];!2)} {[w]((n;v)@'w 1 2;&2)} {[w]((v;n)@'w[1;1 2];!2)} {[w]((v;n;v;n)@'w 1 1 2 2;0 1 0 1)} {[w]((v;n;n;v)@'w[1;1 2 1 2];0 1 0 1)} {[w](,k w;,0)} {[w](,n b n w 1;,0)}) / godel's second incompleteness theorem d g2:"(|~@)/~&|~@" / lob's theorem d lob:"(&(&p)/p)/&p" / lob -> godel d(lob;g2) / boolos p.10-14 d"(&a)/&&a" / T18 d"(&((&a)/a)~a" / T19a d"(&((&a)/a)~&&a)&a" / T19b d"(&@)~&|p" / T21 d"(&|@)~&@" / T22 d"(&p~~&p)~&p~~&@" / T24a d"(&p~&p)~&p~~@" / T24b d"(&p~&~p)~&p~&@" / T24c d"(&p~~&~p)~&p~@" / T24d \ (|~@)/~&|~@ --- valid +--------------+ |0:~(|~@)/~&|~@| | | | | 1:|~@:0 | | | | | 2:&|~@:0 | | | | | 3:~&@:1 | |+--------+ | || 0:~@:3 | | || | | | || 1:&@:3 | | || | | | ||2:&|~@:3| | || | | | || 3:|~@:3| | || | | | || 4:~&@:3| | || | | | || X | | |+--------+ | +--------------+ (&(&p)/p)/&p --- valid +------------------+ |0:~(&(&p)/p)/&p | | | | | 1:&(&p)/p:0 | | | | | 2:~&p:0 | |+----------------+| || 0:~p:2 || || | || || 1:&p:2 || || | || || 2:&(&p)/p:2 || || | || || 3:(&p)/p:2 || || | || || +---+---+ || || | | || || 4:~&p:3 5:p:3 || || | | || || X X || |+----------------+| +------------------+ (&(&p)/p)/&p (|~@)/~&|~@ --- valid +---------------------------------+ | 0:(&(&p)/p)/&p | | | | | 1:~(|~@)/~&|~@ | | | | | 2:|~@:1 | | | | | 3:&|~@:1 | | | | | +-----+-----+ | | | | | | 4:~&(&p)/p:0 5:&p:0 | | | | | | 6:~&@:2 7:~&@:2 | |+-----------++--------++--------+| ||0:~(&p)/p:4|| 0:~@:6 || 0:~@:7 || || | || | || | || ||1:&(&p)/p:4|| 1:&@:6 || 1:&@:7 || || | || | || | || || 2:&|~@:4 ||2:&|~@:6||2:&|~@:7|| || | || | || | || || 3:|~@:4 || 3:|~@:6|| 3:|~@:7|| || | || | || | || || 4:&p:4 || 4:&p:6|| 4:&p:7|| || | || | || | || || 5:p:4 || 5:p:6 || 5:p:7 || || | || | || | || || 6:&p:0 || 6:~&@:3|| 6:~&@:3|| || | || | || | || || 7:~p:0 || X || X || || | |+--------++--------+| || 8:~&@:3 | | || | | | || X | | |+-----------+ | +---------------------------------+ (&a)/&&a --- valid +-----------+ |0:~(&a)/&&a| | | | | 1:&a:0 | | | | | 2:~&&a:0 | |+-------+ | ||0:~&a:2| | || | | | ||1:&&a:2| | || | | | || 2:&a:2| | || | | | || 3:a:2| | || | | | || X | | |+-------+ | +-----------+ (&((&a)/a)~a --- valid +------------------------------------------+ |0:~&(&a)/a~a | |+----------------------------------------+| || 0:~(&a)/a~a:0 || || | || || 1:&(&a)/a~a:0 || || | || || +-------+-------+ || || | | || || 2:(&a)/a:0 4:~(&a)/a:0 || || | | || || 3:~a:0 5:a:0 || || | | || || +---+---+ 6:&a:4 || || | | | || || 8:~&a:2 9:a:2 7:~a:4 || || | | || || X X || ||+--------------------------------------+|| ||| 0:~a:8 ||| ||| | ||| ||| 1:&a:8 ||| ||| | ||| ||| 2:&(&a)/a~a:8 ||| ||| | ||| ||| 3:(&a)/a~a:8 ||| ||| | ||| ||| 4:a:8 ||| ||| | ||| ||| +--------+---------+ ||| ||| | | ||| ||| 5:(&a)/a:3 7:a:3 ||| ||| | | ||| ||| 6:~(&a)/a:3 8:~a:3 ||| ||| | | ||| ||| 9:&a:6 X ||| ||| | ||| ||| 10:~a:6 ||| ||| | ||| ||| +---+----+ ||| ||| | | ||| ||| 11:~&a:5 12:a:5 ||| ||| | | ||| ||| X X ||| ||+--------------------------------------+|| |+----------------------------------------+| +------------------------------------------+ (&((&a)/a)~&&a)&a --- valid +----------------------------------------------------------------------------------+ | 0:~(&(&a)/a~&&a)&a | | | | | +-------+--------+ | | | | | | 1:~&(&a)/a~&&a:0 2:~a:0 | |+--------------------------------------------------------------------------------+| || 0:~(&a)/a~&&a:1 || || | || || 1:&(&a)/a~&&a:1 || || | || || +-------+-------+ || || | | || || 2:(&a)/a:0 4:~(&a)/a:0 || || | | || || 3:~&&a:0 5:&&a:0 || || | | || || +---+---+ 6:&a:4 || || | | | || || 8:~&a:2 9:a:2 7:~a:4 || ||+--------------------------------------++--------------------------------------+|| ||| 0:~&a:3 || 0:~a:8 ||| ||| | || | ||| ||| 1:&&a:3 || 1:&a:8 ||| ||| | || | ||| ||| 2:&(&a)/a~&&a:3 || 2:&(&a)/a~&&a:8 ||| ||| | || | ||| ||| 3:(&a)/a~&&a:3 || 3:(&a)/a~&&a:8 ||| ||| | || | ||| ||| 4:&a:3 || 4:&&a:8 ||| ||| | || | ||| ||| 5:a:3 || 5:a:8 ||| ||| | || | ||| ||| +--------+---------+ || +--------+---------+ ||| ||| | | || | | ||| ||| 6:(&a)/a:3 8:&&a:3 || 6:(&a)/a:3 8:&&a:3 ||| ||| | | || | | ||| ||| 7:~(&a)/a:3 9:~&&a:3 || 7:~(&a)/a:3 9:~&&a:3 ||| ||| | | || | | ||| ||| 10:&a:7 X || 10:&a:7 X ||| ||| | || | ||| ||| 11:~a:7 || 11:~a:7 ||| ||| | || | ||| ||| +---+----+ || +---+----+ ||| ||| | | || | | ||| ||| 12:~&a:6 13:a:6 || 12:~&a:6 13:a:6 ||| ||| | | || | | ||| ||| X X || X X ||| ||+--------------------------------------++--------------------------------------+|| |+--------------------------------------------------------------------------------+| +----------------------------------------------------------------------------------+ (&@)~&|p --- valid +--------------------+ | 0:~(&@)~&|p | | | | | +---+---+ | | | | | | 1:&@:0 3:~&@:0 | | | | | | 2:~&|p:0 4:&|p:0 | |+--------++--------+| || 0:~|p:2|| 0:~@:3 || || | || | || || 1:&|p:2|| 1:&@:3 || || | || | || || 2:&@:2 || 2:@:3 || || | || | || || 3:@:2 || 3:&|p:3|| || | || | || || 4:|p:2 || 4:|p:3 || || | || | || ||5:~&~p:4||5:~&~p:4|| || | || | || || X || X || |+--------++--------+| +--------------------+ (&|@)~&@ --- valid +--------------------+ | 0:~(&|@)~&@ | | | | | +----+----+ | | | | | | 1:&|@:0 3:~&|@:0 | | | | | | 2:~&@:0 4:&@:0 | |+--------++--------+| || 0:~@:2 || 0:~|@:3|| || | || | || || 1:&@:2 || 1:&|@:3|| || | || | || || 2:&|@:2|| 2:|@:3 || || | || | || || 3:|@:2 || 3:&@:3 || || | || | || || 4:@:2 || 4:@:3 || || | || | || ||5:~&~@:3||5:~&~@:2|| || | || | || || X || X || |+--------++--------+| +--------------------+ (&p~~&p)~&p~~&@ --- valid +----------------------------------------------------------------------------------------------------------------------------------------------------------------+ | 0:~(&p~~&p)~&p~~&@ | | | | | +-----+-----+ | | | | | | 1:&p~~&p:0 3:~&p~~&p:0 | | | | | | 2:~&p~~&@:0 4:&p~~&@:0 | |+------------------------------------------------------------------------------++------------------------------------------------------------------------------+| || 0:~p~~&@:2 || 0:~p~~&p:3 || || | || | || || 1:&p~~&@:2 || 1:&p~~&p:3 || || | || | || || 2:&p~~&p:2 || 2:p~~&p:3 || || | || | || || 3:p~~&p:2 || 3:&p~~&@:3 || || | || | || || 4:p~~&@:2 || 4:p~~&@:3 || || | || | || || +------------------+-------------------+ || +------------------+-------------------+ || || | | || | | || || 5:p:0 7:~p:0 || 5:p:0 7:~p:0 || || | | || | | || || 6:&@:0 8:~&@:0 || 6:&p:0 8:~&p:0 || || | | || | | || || +--------+---------+ +--------+---------+ || +--------+---------+ +--------+---------+ || || | | | | || | | | | || || 9:p:3 11:~&p:3 13:p:3 15:~&p:3 || 9:p:2 11:~&p:2 13:p:2 15:~&p:2 || || | | | | || | | | | || || 10:~p:3 12:&p:3 14:~p:3 16:&p:3 || 10:~p:2 12:&p:2 14:~p:2 16:&p:2 || || | | | | || | | | | || || +----+----+ +----+----+ +----+----+ +----+----+ || +----+----+ +----+----+ +----+----+ +----+----+ || || | | | | | | | | || | | | | | | | | || || 17:p:4 19:~&@:4 21:p:4 23:~&@:4 25:p:4 27:~&@:4 29:p:4 31:~&@:4|| 17:p:4 19:~&@:4 21:p:4 23:~&@:4 25:p:4 27:~&@:4 29:p:4 31:~&@:4|| || | | | | | | | | || | | | | | | | | || || 18:~p:4 20:&@:4 22:~p:4 24:&@:4 26:~p:4 28:&@:4 30:~p:4 32:&@:4|| 18:~p:4 20:&@:4 22:~p:4 24:&@:4 26:~p:4 28:&@:4 30:~p:4 32:&@:4|| || | | | | | | | | || | | | | | | | | || || X X X X X X X X || X X X X X X X X || |+------------------------------------------------------------------------------++------------------------------------------------------------------------------+| +----------------------------------------------------------------------------------------------------------------------------------------------------------------+ (&p~&p)~&p~~@ --- valid +------------------------------------------------------------------------------------------------------------------------------------------------+ | 0:~(&p~&p)~&p~~@ | | | | | +----+-----+ | | | | | | 1:&p~&p:0 3:~&p~&p:0 | | | | | | 2:~&p~~@:0 4:&p~~@:0 | |+----------------------------------------------------------------------++----------------------------------------------------------------------+| || 0:~p~~@:2 || 0:~p~&p:3 || || | || | || || 1:&p~~@:2 || 1:&p~&p:3 || || | || | || || 2:&p~&p:2 || 2:p~&p:3 || || | || | || || 3:p~&p:2 || 3:&p~~@:3 || || | || | || || 4:p~~@:2 || 4:p~~@:3 || || | || | || || +----------------+-----------------+ || +----------------+-----------------+ || || | | || | | || || 5:p:0 7:~p:0 || 5:p:0 7:~p:0 || || | | || | | || || 6:@:0 8:~@:0 || 6:~&p:0 8:&p:0 || || | | || | | || || +-------+--------+ +-------+--------+ || +-------+--------+ +-------+--------+ || || | | | | || | | | | || || 9:p:3 11:&p:3 13:p:3 15:&p:3 || 9:p:2 11:&p:2 13:p:2 15:&p:2 || || | | | | || | | | | || || 10:~p:3 12:~&p:3 14:~p:3 16:~&p:3 || 10:~p:2 12:~&p:2 14:~p:2 16:~&p:2 || || | | | | || | | | | || || +---+---+ +---+---+ +---+---+ +---+---+ || +---+---+ +---+---+ +---+---+ +---+---+ || || | | | | | | | | || | | | | | | | | || || 17:p:4 19:~@:4 21:p:4 23:~@:4 25:p:4 27:~@:4 29:p:4 31:~@:4|| 17:p:4 19:~@:4 21:p:4 23:~@:4 25:p:4 27:~@:4 29:p:4 31:~@:4|| || | | | | | | | | || | | | | | | | | || || 18:~p:4 20:@:4 22:~p:4 24:@:4 26:~p:4 28:@:4 30:~p:4 32:@:4|| 18:~p:4 20:@:4 22:~p:4 24:@:4 26:~p:4 28:@:4 30:~p:4 32:@:4|| || | | | | | | | | || | | | | | | | | || || X X X X X X X X || X X X X X X X X || |+----------------------------------------------------------------------++----------------------------------------------------------------------+| +------------------------------------------------------------------------------------------------------------------------------------------------+ (&p~&~p)~&p~&@ --- valid +----------------------------------------------------------------------------------------------------------------------------------------------------------------+ | 0:~(&p~&~p)~&p~&@ | | | | | +-----+-----+ | | | | | | 1:&p~&~p:0 3:~&p~&~p:0 | | | | | | 2:~&p~&@:0 4:&p~&@:0 | |+------------------------------------------------------------------------------++------------------------------------------------------------------------------+| || 0:~p~&@:2 || 0:~p~&~p:3 || || | || | || || 1:&p~&@:2 || 1:&p~&~p:3 || || | || | || || 2:&p~&~p:2 || 2:p~&~p:3 || || | || | || || 3:p~&~p:2 || 3:&p~&@:3 || || | || | || || 4:p~&@:2 || 4:p~&@:3 || || | || | || || +------------------+-------------------+ || +------------------+-------------------+ || || | | || | | || || 5:p:0 7:~p:0 || 5:p:0 7:~p:0 || || | | || | | || || 6:~&@:0 8:&@:0 || 6:~&~p:0 8:&~p:0 || || | | || | | || || +--------+---------+ +--------+---------+ || +--------+---------+ +--------+---------+ || || | | | | || | | | | || || 9:p:3 11:&~p:3 13:p:3 15:&~p:3 || 9:p:2 11:&~p:2 13:p:2 15:&~p:2 || || | | | | || | | | | || || 10:~p:3 12:~&~p:3 14:~p:3 16:~&~p:3 || 10:~p:2 12:~&~p:2 14:~p:2 16:~&~p:2 || || | | | | || | | | | || || +----+----+ +----+----+ +----+----+ +----+----+ || +----+----+ +----+----+ +----+----+ +----+----+ || || | | | | | | | | || | | | | | | | | || || 17:p:4 19:&@:4 21:p:4 23:&@:4 25:p:4 27:&@:4 29:p:4 31:&@:4|| 17:p:4 19:&@:4 21:p:4 23:&@:4 25:p:4 27:&@:4 29:p:4 31:&@:4|| || | | | | | | | | || | | | | | | | | || || 18:~p:4 20:~&@:4 22:~p:4 24:~&@:4 26:~p:4 28:~&@:4 30:~p:4 32:~&@:4|| 18:~p:4 20:~&@:4 22:~p:4 24:~&@:4 26:~p:4 28:~&@:4 30:~p:4 32:~&@:4|| || | | | | | | | | || | | | | | | | | || || X X X X X X X X || X X X X X X X X || |+------------------------------------------------------------------------------++------------------------------------------------------------------------------+| +----------------------------------------------------------------------------------------------------------------------------------------------------------------+ (&p~~&~p)~&p~@ --- valid +------------------------------------------------------------------------------------------------------------------------------------------------+ | 0:~(&p~~&~p)~&p~@ | | | | | +------+------+ | | | | | | 1:&p~~&~p:0 3:~&p~~&~p:0 | | | | | | 2:~&p~@:0 4:&p~@:0 | |+----------------------------------------------------------------------++----------------------------------------------------------------------+| || 0:~p~@:2 || 0:~p~~&~p:3 || || | || | || || 1:&p~@:2 || 1:&p~~&~p:3 || || | || | || || 2:&p~~&~p:2 || 2:p~~&~p:3 || || | || | || || 3:p~~&~p:2 || 3:&p~@:3 || || | || | || || 4:p~@:2 || 4:p~@:3 || || | || | || || +----------------+-----------------+ || +----------------+-----------------+ || || | | || | | || || 5:p:0 7:~p:0 || 5:p:0 7:~p:0 || || | | || | | || || 6:~@:0 8:@:0 || 6:&~p:0 8:~&~p:0 || || | | || | | || || +-------+--------+ +-------+--------+ || +-------+--------+ +-------+--------+ || || | | | | || | | | | || || 9:p:3 11:~&~p:3 13:p:3 15:~&~p:3 || 9:p:2 11:~&~p:2 13:p:2 15:~&~p:2 || || | | | | || | | | | || || 10:~p:3 12:&~p:3 14:~p:3 16:&~p:3 || 10:~p:2 12:&~p:2 14:~p:2 16:&~p:2 || || | | | | || | | | | || || +---+---+ +---+---+ +---+---+ +---+---+ || +---+---+ +---+---+ +---+---+ +---+---+ || || | | | | | | | | || | | | | | | | | || || 17:p:4 19:@:4 21:p:4 23:@:4 25:p:4 27:@:4 29:p:4 31:@:4|| 17:p:4 19:@:4 21:p:4 23:@:4 25:p:4 27:@:4 29:p:4 31:@:4|| || | | | | | | | | || | | | | | | | | || || 18:~p:4 20:~@:4 22:~p:4 24:~@:4 26:~p:4 28:~@:4 30:~p:4 32:~@:4|| 18:~p:4 20:~@:4 22:~p:4 24:~@:4 26:~p:4 28:~@:4 30:~p:4 32:~@:4|| || | | | | | | | | || | | | | | | | | || || X X X X X X X X || X X X X X X X X || |+----------------------------------------------------------------------++----------------------------------------------------------------------+| +------------------------------------------------------------------------------------------------------------------------------------------------+