David, Your value L7 is a function (type THM -> THM) not a theorem (type THM). You need to apply it to another theorem to get a new theorem. ] Regards,
Rob. On Tue, March 17, 2015 12:59 am, David Topham wrote: > Thank you so much Rob! That works! If you don't mind another question: > I > had gotten format_thm to work without quantifiers, but with the quantifier > I get an exception. (attached). I don't see anything about format_thm in > user029.pdf (the main HOL reference). -Dave > > On Mon, Mar 16, 2015 at 2:51 PM, Rob Arthan <[email protected]> wrote: > > >> David, >> >> >>> On 16 Mar 2015, at 04:22, David Topham <[email protected]> wrote: >>> >>> >>> With my recent success learning to encode Propositional Calculus >>> using >> ProofPower (for my Discrete Math course), I have pressed on to >> Predicate >> Calculus. >> >>> >>> So far, I have figured out the basics, but stuck on quantifiers from >>> >> what I intuitively thought might work. Attached is my error message >> trying to quantify a negation. >> >> ProofPower syntax needs a bullet between the bound variables and the >> predicate in a quantification. You have to write: >> >> â x⦠¬ P(x) >> >> rather than: >> >> â x ¬ P(x) >> >> This follows what is now common practice in logical languages used in >> CS >> and reflects a decision to make quantifiers have lower precedence than >> the propositional operators, so that the scope of a quantifier extends >> as far to the right as possible (as opposed to traditional mathematical >> logic practice which requires brackets around the matrix of a >> quantification if the matrix is not a literal). So the brackets around >> the implication in: >> >> â x⦠(¬ P(x) â Q(x)) >> >> are unnecessary. (I think of the bullet as being like a big version of >> Russell & Whiteheadâs convention of using a dot to adjust the >> precedence of a connective.) Unfortunately, this is probably at odds >> with the conventions you have been using in your course. >> >> Regards, >> >> >> Rob. >> >> >> > _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
