# Formula (FOL)

**Stub grade: A**

## Definition

The logical formulas of a FOL are (like terms) defined inductively by the following 5 rules^{[1]}:

- If [ilmath]t_1[/ilmath] and [ilmath]t_2[/ilmath] are terms then [ilmath]t_1\doteq t_2[/ilmath] is a formula
- If [ilmath]t_1,\ldots,t_m[/ilmath] are terms and [ilmath]P[/ilmath] is an [ilmath]m[/ilmath]-ary predicate symbol then [ilmath]Pt_1\cdots t_m[/ilmath] is a formula
- If [ilmath]A[/ilmath] is a formula, then [ilmath](\neg A)[/ilmath] is a formula
- If [ilmath]A[/ilmath] and [ilmath]B[/ilmath] are formulas then:
- [ilmath](A\wedge B)[/ilmath], [ilmath](A\vee B)[/ilmath], [ilmath](A\rightarrow B)[/ilmath] and [ilmath](A\leftrightarrow B)[/ilmath] are all formulas too
- Note, as mentioned on the FOL page, we can define some of these logical connective symbols in terms of the others. Keep that in mind here

- [ilmath](A\wedge B)[/ilmath], [ilmath](A\vee B)[/ilmath], [ilmath](A\rightarrow B)[/ilmath] and [ilmath](A\leftrightarrow B)[/ilmath] are all formulas too
- If [ilmath]A[/ilmath] is a formula and [ilmath]x[/ilmath] is a variable symbol then both:
- [ilmath]\forall xA[/ilmath] and [ilmath]\exists xA[/ilmath] are formulas
- Again from the FOL page recall that we can define [ilmath]\forall [/ilmath] using [ilmath]\exists[/ilmath] and [ilmath]\exists[/ilmath] using [ilmath]\forall[/ilmath]

- [ilmath]\forall xA[/ilmath] and [ilmath]\exists xA[/ilmath] are formulas

We have been rather lax in how we use brackets here. In practice we shall use them whenever they help readability, and also discard them whenever it helps, for example:

- [ilmath]\exists x(x\doteq y)[/ilmath] is easier to read than [ilmath]\exists xx\doteq y[/ilmath]
- [ilmath]A\vee B\vee C\vee D[/ilmath] is easier to read than [ilmath](((A\vee B)\vee C)\vee D)[/ilmath]

If we fixed (1) by changing rule 5 to [ilmath]\forall x(A)[/ilmath] and [ilmath]\exists x(A)[/ilmath] then we'd have lots of things that look like:

- [ilmath]\exists x((\ldots \rightarrow \ldots)) [/ilmath]

So just be comfortable that we *could* write everything out totally unambiguously using lots of brackets without having to address the issue of parsing.

### BNF Definition

I don't like this (as it is written now), it needs cleaning up. But using^{[1]} we get:

- Formula ::= Term [ilmath]\doteq[/ilmath] Term | PREDICATE (Term)
_{[ilmath]n[/ilmath]-times}| [ilmath]\neg[/ilmath] Formula | Formula ([ilmath]\wedge[/ilmath]|[ilmath]\vee[/ilmath]|[ilmath]\rightarrow[/ilmath]|[ilmath]\leftrightarrow[/ilmath]) Formula | ([ilmath]\forall[/ilmath]|[ilmath]\exists[/ilmath]) VARIABLE Formula

TODO: Clean this up, write a grammar that is "correct". For example there should be brackets on everything between the [ilmath]\vert[/ilmath]s. This reads like "term followed by [ilmath]\doteq[/ilmath] followed by (Term or PREDICATE ....)

## Terminology

- Any formula given by rules [ilmath]1[/ilmath] or [ilmath]2[/ilmath] is called an atomic formula.
- Any other formula is called a composite formula