> 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.



Proofpower mailing list

Reply via email to