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
