# Formula (FOL)

(Redirected from Atomic formula (FOL))
This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:
Created so I wouldn't have to sift through notes or scour PDFs. It requires more references and some fleshing out to link to other pages. But will suffice for now

## 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
2. 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
3. If [ilmath]A[/ilmath] is a formula, then [ilmath](\neg A)[/ilmath] is a formula
4. 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
5. 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]

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:

1. [ilmath]\exists x(x\doteq y)[/ilmath] is easier to read than [ilmath]\exists xx\doteq y[/ilmath]
2. [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 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 ....)