Logiweb aspects of propositional theory in pyk

Up Help

The predefined "pyk" aspect

define pyk of propositional theory as text unicode start of text unicode small p unicode small r unicode small o unicode small p unicode small o unicode small s unicode small i unicode small t unicode small i unicode small o unicode small n unicode small a unicode small l unicode space unicode small t unicode small h unicode small e unicode small o unicode small r unicode small y unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of propositional theory as text unicode start of text unicode newline unicode capital t unicode underscore unicode left brace unicode capital p unicode small r unicode small o unicode small p unicode right brace unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of propositional theory as ( all metavar var a end metavar indeed all metavar var b end metavar indeed ( metavar var a end metavar infer ( ( metavar var a end metavar imply metavar var b end metavar ) infer metavar var b end metavar ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed ( ( metavar var a end metavar imply ( metavar var b end metavar imply metavar var c end metavar ) ) imply ( ( metavar var a end metavar imply metavar var b end metavar ) imply ( metavar var a end metavar imply metavar var c end metavar ) ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed ( ( metavar var c end metavar free for metavar var b end metavar in metavar var a end metavar ) endorse all metavar var b end metavar indeed ( metavar var a end metavar imply sub metavar var a end metavar set metavar var b end metavar to metavar var c end metavar end sub ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed ( ( not ( metavar var c end metavar free in metavar var a end metavar ) ) endorse ( ( all metavar var c end metavar indeed ( metavar var a end metavar imply metavar var b end metavar ) ) imply ( metavar var a end metavar imply all metavar var c end metavar indeed metavar var b end metavar ) ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed ( metavar var a end metavar imply ( metavar var b end metavar imply metavar var a end metavar ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed ( ( ( not metavar var a end metavar ) imply not metavar var b end metavar ) imply ( ( ( not metavar var a end metavar ) imply metavar var b end metavar ) imply metavar var a end metavar ) ) ) rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed ( metavar var a end metavar infer all metavar var b end metavar indeed metavar var a end metavar ) ) ) ) ) ) end define