+1 credit
| Version | Summary | Created by | Modification | Content Size | Created at | Operation |
|---|---|---|---|---|---|---|
| 1 | Dean Liu | -- | 2457 | 2022-12-01 01:47:38 |
Video Upload Options
In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact. A first-order term is recursively constructed from constant symbols, variables and function symbols. An expression formed by applying a predicate symbol to an appropriate number of terms is called an atomic formula, which evaluates to true or false in bivalent logics, given an interpretation. For example, [math]\displaystyle{ (x+1)*(x+1) }[/math] is a term built from the constant 1, the variable x, and the binary function symbols [math]\displaystyle{ + }[/math] and [math]\displaystyle{ * }[/math]; it is part of the atomic formula [math]\displaystyle{ (x+1)*(x+1) \ge 0 }[/math] which evaluates to true for each real-numbered value of x. Besides in logic, terms play important roles in universal algebra, and rewriting systems.
References
- C.C. Chang; H. Jerome Keisler (1977). Model Theory. Studies in Logic and the Foundation of Mathematics. 73. North Holland. ; here: Sect.1.3
- Hermes, Hans (1973). Introduction to Mathematical Logic. Springer London. ISBN 3540058192. ; here: Sect.II.1.3
- Since atomic formulas can be viewed as trees, too, and renaming is essentially a concept on trees, atomic (and, more generally, quantifier-free) formulas can be renamed in a similar way as terms. In fact, some authors consider a quantifier-free formula as a term (of type bool rather than e.g. int, cf. #Sorted terms below).
- Renaming of the commutativity axiom can be viewed as alpha-conversion on the universal closure of the axiom: "x+y=y+x" actually means "∀x,y: x+y=y+x", which is synonymous to "∀a,b: a+b=b+a"; see also #Lambda terms below.
- I.e., "symbol type" in the Many-sorted signatures section of the Signature (logic) article.
