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, $\mathscr{L}$ 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 $f$ is an $n$-ary function symbol and $t_1,\ldots,t_n$ are terms, then $ft_1\cdots t_n$ is a term

The collection of all terms of the FOL is denoted: $\mathscr{L}_T$

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