User:Physis/Gödel-Herbrand-Kleene equational calculus
Appearance
Definition
[edit]Defined in the follwing way.[1][2]
The calculus consists of a set (or system) of equations. An equation is of form <term> = <term>, where the left-hand side term may be required to contain a principial letter. Let the set of nonlogical symbols contain the unary f (besides the arithmetical ones 0 and s). This f is just an example of a particular signature, in generally, an arbitrary signature must be considered (which contains the signature of natural numbers at least as an 0 and s).
Syntax
[edit]- <equation> ::= <lhsterm> = <term>
- <lhsterm> ::= 0
- <lhsterm> ::= s <term>
- <lhsterm> ::= f <term>
- <lhsterm> ::= g <term> <term>
- <term> ::= <variable>
- <term> ::= <lhsterm>
Rules
[edit]
Expressing power
[edit]Equivalent power with the theory of partial recursive functions.[3][2]
Notes
[edit]References
[edit]- Bezem, Marc (2003). Term Rewriting Systems. Cambridge University Press. ISBN 0521391156.
{{cite book}}
: Unknown parameter|coauthors=
ignored (|author=
suggested) (help) - Monk, J. Donald (1976). Mathematical Logic. Graduate Texts in Mathematics. New York • Heidelberg • Berlin: Springer-Verlag.