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
<https://www.dropbox.com/s/7kd7dsd2erg0hi1/pred_calc.png?dl=0>

On Tue, Mar 17, 2015 at 1:45 PM, Rob Arthan <r...@lemma-one.com> 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 <dtop...@gmail.com> 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" <r...@lemma-one.com> 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 <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