This guide explains the syntax rules for determining what constitutes a Well-Formed Formula (hence 'WFF') for JustInfer. To keep the program user friendly, some minor modifications to traditional syntax rules have been made.

1. Sentence Letters

An uppercase letter alone from the English alpahbet, (except 'A', 'E', and 'V') counts as a sentence letter, and so is a wff for this program. 'A', 'E', and 'V' are used for other purposes. Eventually I will allow subscripting a sentence letter with a number so that there are infinitely many sentence letters but for now this isn't the case. Examples:

• B
• P
• Q

2. Negation

If φ is a wff, then a negation symbol to the imediate left of φ will also be a wff. The default symbol for negation is '~', but this can be customized on the settings page. If you choose a symbol other than '~' for negation, you may still type '~' and '~' will be replaced by your chosen negation symbol when you enter your input. Examples:

• ~P
• ~Gab

3. Binary Connectives

If φ and ψ are wffs, you may put a binary connective between them and wrap the result in parentheses to form a WFF. To symbolize conjunction, disjunction, conditional, and biconditional you may use '&'', 'v', '->', and '<->', respectively and you may customize how these symbols are displayed by selecting the desired symbols on the settings page.. Even if you choose different symbols, you may use the default symbols when typing and they will be replaced with your chosen symbols when you enter the input. Examples:

• (P & Q)
• (Fx v Gy)
• (P -> R)
• (Hx <-> Jy)

4. Predicates and subjects

An uppercase letter from the English alpahbet (except 'A', 'E', and 'V') that is immediately followed by one or more lowercase letters is a WFF. In this case, the uppercase letter serves as a predicate (as opposed to a sentence letter) and the lowercase letter serves as constant (a - m) or a variable ([n - z] excluding 'v'). Examples:

• Fa
• Gyz

5. Quantifiers

The universal quantifer is symbolized by '∀', for easier typing, justinfer accepts and will translate 'A' and '@' as '∀'. The existential quantifer is symbolized by '∃', for easier typing, justinfer accepts and will translate 'E' and '$' as '∃'. A quantifer immediately followed by a variable(n,..., z)[excluding 'v'] and then a WFF, is a WFF. Examples:

• ∃yFx
• ∀x(Px & Qx)
• ∀xP

6. Informal WFFs

Strings that would be well-formed if wrapped in parenthesis are recognized as informal-WFFs (informal-WFFs can be used in problems but do not count as WFFs for purposes of the definitions above). Example:

• P & Q
• ∀x(Fx v Gx) & Ha

Examples

Below are some examples:

Expression	Will it count as a WFF for JustInfer?
P	Yes
B	Yes
~P	Yes
~(P)	No (because "(P)" is not a wff)
(~P)	No
(P & Q)	Yes
P v Q	Sort of. This is allowable because it is an informal-WFF but you can't subsitute this for a WFF in the definitions above.
Ba	Yes (in this case "B" will automatically serve as a predicate letter)
V	No (likely in your logic system this would be a WFF but for this website, 'V', 'A', and 'E' are reservered to symbolize disjunction, universal quantification, and existential quantification respectively)
∀x(Fx & Px)	Yes
∀bPb	No (because a quantifer cannot bind a constant [constants are a - m])
AxGx	Yes (justinfer will rewrite this as ∀xGx)
ExEyGxy	Yes (justinfer will rewrite this as ∃x∃yGxy)
Ax(Gx)	No (for similar to reason as why "~(P)" isn't a wff)

Check if Your Expression is a WFF for JustInfer