User:Physis/Gödel-Herbrand-Kleene equational calculus

From Wikipedia, the free encyclopedia

Contents

[edit] Definition

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).

[edit] Syntax

<equation> ::= <lhsterm> = <term>
<lhsterm> ::= 0
<lhsterm> ::= s <term>
<lhsterm> ::= f <term>
<lhsterm> ::= g <term> <term>
<term> ::= <variable>
<term> ::= <lhsterm>

[edit] Rules

\frac{\gamma \in \Gamma}{\Gamma \vdash \gamma}


\frac{\Gamma \vdash \phi}{\Gamma \vdash \phi[x := \mathbf m]}


\frac{\Gamma \vdash \sigma = \tau, m \in \mathbb N, n \in \mathbb N, \Gamma \vdash f \mathbf m = \mathbf n}{\Gamma \vdash \sigma = \tau[f \mathbf m \to_1 \mathbf n]}

[edit] Expressing power

Equivalent power with the theory of partial recursive functions.[3][2]

[edit] Notes

  1. ^ Bezem & Klop & de Vrijer: 62
  2. ^ a b Monk 1976: 67
  3. ^ Bezem & Klop & de Vrijer: 63

[edit] References

  • Bezem, Marc; Klop, Jan Willem; Roel de Vrijer (2003). Term Rewriting Systems. Cambridge University Press. ISBN 0521391156. 
  • Monk, J. Donald (1976). Mathematical Logic, Graduate Texts in Mathematics. New York • Heidelberg • Berlin: Springer-Verlag. 

[edit] External links