On Thu, 2008-01-31 at 15:47 -0500, Lockwood Morris wrote:

Yes, highly possible, as the following shows. (I apologize for having forgotten how to get HOL to show the assumptions as other than dots; that accounts for the DISCH_ALL's just so we can see where we are. The key move is t1: DISCH is willing to introduce a superfluous hypothesis. val t1 = DISCH (Term`A:bool`) (ASSUME (Term`B:bool`)); (* [.] |- A ==> B *) DISCH(Term`B:bool`) t1; (* |- B ==> A ==> B *) val t2 = MP (ASSUME (Term`B ==> A`)) (ASSUME (Term`B:bool`)); (* [..] |- A *) DISCH_ALL t2; (* |- (B ==> A) ==> B ==> A *) val t3 = MP (ASSUME (Term`(A ==> B) ==> A ==> C`)) (ASSUME (Term`A ==> B`)); (* [..] |- A ==> C *) DISCH_ALL t3; (* t3' = |- ((A ==> B) ==> A ==> C) ==> (A ==> B) ==> A ==> C *) val t4 = MP t3 t2; (* [....] |- C *) DISCH_ALL t4; (* |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> (A ==> B) ==> B ==> C *) val t5 = DISCH (Term`A ==> B`) t4; (* [...] |- (A ==> B) ==> C *) DISCH_ALL t5; (* |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> B ==> (A ==> B) ==> C *) val t6 = MP t5 t1; (* [...] |- C *) val t7 = DISCH (Term`(A ==> B) ==> A ==> C`) (DISCH (Term`B ==> A`) (DISCH (Term`B:bool`) t6)); (* t7 = |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> B ==> C *) Best wishes, Lockwood |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- Lockwood Morris lockwood@ecs.syr.edu (315)443-3046 Rm. 4-125 CST Emeritus Professor Dept. of EECS Syracuse University Syracuse NY On Thu, 31 Jan 2008 tjohnson2059@comcast.net wrote: > Hi, > > Given, > > - val thm1 = DECIDE (--`((A ==> B) ==> (A ==> C)) ==> ((B ==> A) ==> (B ==> C))`--); > > val thm1 = [] |- ((A ==> B) ==> A ==> C) ==> (B ==> A) ==> B ==> C : thm > > is it possible to prove this theorem using only ASSUME, DISCH, and MP?