1$( Modified version of demo0.mm from 1-Jan-04 $) 2 3$( 4 PUBLIC DOMAIN DEDICATION 5 6This file is placed in the public domain per the Creative Commons Public 7Domain Dedication. http://creativecommons.org/licenses/publicdomain/ 8 9Norman Megill - email: nm at alum.mit.edu 10$) 11 12$c 0 + = -> ( ) term wff |- $. 13 14$v t r s P Q $. 15 16tt $f term t $. 17tr $f term r $. 18ts $f term s $. 19wp $f wff P $. 20wq $f wff Q $. 21 22tze $a term 0 $. 23tpl $a term ( t + r ) $. 24 25weq $a wff t = r $. 26wim $a wff ( P -> Q ) $. 27 28a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. 29a2 $a |- ( t + 0 ) = t $. 30${ 31 $( Define the modus ponens inference rule $) 32 min $e |- P $. 33 maj $e |- ( P -> Q ) $. 34 mp $a |- Q $. 35$} 36 37th1 $p |- t = t $= 38 $( Here is its proof: $) 39 tt tze tpl tt weq tt tt weq tt a2 tt tze tpl 40 tt weq tt tze tpl tt weq tt tt weq wim tt a2 41 tt tze tpl tt tt a1 mp mp 42$. 43