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 <r...@lemma-one.com> wrote:
>
>
>> David,
>>
>>
>>> On 16 Mar 2015, at 04:22, David Topham <dtop...@ohlone.edu> 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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to