Re: [ProofPower] Predicate Calculus

2015-03-17 Thread David Topham 
Ah! Of course! Thank you again!  I think I got it now. For completeness
sake, in case anyone else is pursuing this line of learning ProofPower, I
have a link here to the working version with those pieces in place. I do
think there is a lot of potential for using this tool to teach Discrete
Math.
  Sample predicate calculus proof


On Tue, Mar 17, 2015 at 1:45 PM, Rob Arthan  wrote:

> David,
>
> The proof isn’t complete, as you will see if you look at the output when
> you execute the lines that bind L6 and L7. You have just bound L6 to a term
> not a theorem. You have bound L7 to the the applicatio of %forall%_intro to
> L6, which does not give you a theorem (but rather a function from theorems
> that will always fail, because %forall%_intro requires its first argument
> to be (something akin to) a variable). The last line of your proof should
> be something like:
>
> val L6 = %forall%_intro %<%x%>% L5;
>
> Regards,
>
> Rob.
>
> > On 17 Mar 2015, at 13:45, David Topham  wrote:
> >
> > That makes sense, but the "proof" is completed, so what can I apply it
> to? i
> > .e. The goal of the proof is just to derive L7. Perhaps put it the form
> of a conditional? ...conjunction of premises model the conclusion?
> >
> > On Mar 17, 2015 5:02 AM, "Rob Arthan"  wrote:
> > 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  wrote:
> > >
> > >
> > >> David,
> > >>
> > >>
> > >>> On 16 Mar 2015, at 04:22, David Topham  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

Re: [ProofPower] Predicate Calculus

2015-03-17 Thread Rob Arthan 
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  wrote:
>
>
>> David,
>>
>>
>>> On 16 Mar 2015, at 04:22, David Topham  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

Re: [ProofPower] Predicate Calculus

2015-03-16 Thread Rob Arthan 
David,

> On 16 Mar 2015, at 04:22, David Topham  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

[ProofPower] Predicate Calculus

2015-03-15 Thread David Topham 
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.

Any suggestions?  Thank you, Dave
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com