Difference between revisions of "Formula (FOL)"

Latest revision as of 05:37, 8 September 2016

Definition

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

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^[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

See next

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

References

1. ↑ ^{1.0 1.1} Mathematical Logic - Foundations for Information Science - Wei Li

Template:Formal logic navbox