simpleSentences.het revision 81f49ee02aaa3bc870401f8883bf52742eb3ea7a
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder%% Page 66, Brauner's book on proof theory
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner%% some axioms
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder preds p,q : ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder . [M] (p /\ q) => ([M]p /\ [M]q) %implied
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner preds p,q : ()
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner . @N p %implied
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner preds p,q : ()
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner . @N (p /\ q) => (@N p /\ @N q) %implied
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner . @N (Here N) %implied
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner . !X (Here X) %implied
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner preds p : ()
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa nominals A,B
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa . (@A @B p) <=> (@B p) %implied
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa preds p : ()
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa . (Here A /\ p) => @A p %implied