Style Guide

Style Guide

This page provides information on preferred style for inputs, so that the Proof Assistant correctly parses your formulas. If you follow the style here, you should not encounter errors related to bad inputting.

In general, rules are as follows:

• Always use brackets around binary operators such as &, ⊃, ≡ and ∨.
• Never use brackets around the argument of ~, unless the argument contains a binary operator.
• Do not place brackets between quantifiers. That is, input ∀x∀y(Rxy), not ∀x(∀y(Rxy)).
• You may use brackets and commas around terms as you wish, but ensure that the arities are correct.

Examples of good and bad style

Good Style	Bad Style
~p
~~p	~(~p)
(p&q)	p&q
~(p&q)	~ p&q
~(~p&q)	~((~p)&q)
~~(p&q)	~(~(p&q))
∀x∀y(Rxy)	∀x(∀y(Rxy))