Formula (FOL)

Stub grade: A

This page is a stub

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
     • 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
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 ....)

---

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

See next

• Free variables
• Term substitution
• Formula substitution
• Model
• Assignment
• Structure