Term (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:

This page was quickly implemented to save me sifting through notes or PDFs to find the content. It will be expanded soon

Definition

Given a first order language, [ilmath]\mathscr{L} [/ilmath] we define the terms inductively using the following 3 rules:

1. Each constant symbol is a term
2. Each variable symbol is a term
3. If [ilmath]f[/ilmath] is an [ilmath]n[/ilmath]-ary function symbol and [ilmath]t_1,\ldots,t_n[/ilmath] are terms, then [ilmath]ft_1\cdots t_n[/ilmath] is a term

The collection of all terms of the FOL is denoted: [ilmath]\mathscr{L}_T[/ilmath]

BNF Definition

We may describe the terms using a BNF grammar:

• Term ::= c | x | ft₁...t_n

Caution:This isn't quite right, as we must know the arity of a function first. However there is something here

See next

• Formula