Formula (FOL)

From Maths
Revision as of 05:37, 8 September 2016 by Alec (Talk | contribs) (Created initial version of page.)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search
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]:

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

See next

References

  1. 1.0 1.1 Mathematical Logic - Foundations for Information Science - Wei Li

Template:Formal logic navbox