The idea of proof-theoretic semantics beyond logic invites consideration of powerful inversion principles that extend the simple form of definitional reflection considered above. Although we mentioned clauses that contained variables, we formally defined definitional reflection only for propositional definitions of the form Da , where it says that everything that can be inferred from each definiens can be obtained from the definiendum of a definition. However, this is insufficient for the more general case which is the standard case in logic programming. We show this by means of an example. Suppose we have the following definition in which the atoms have a predicate-argument-structure:

⎧ child_of_tom(anna) ⇐ daughter_of_tom(anna)

⎪

⎨ child_of_tom(robert) ⇐ son_of_tom(robert)

tall(anna) ⇐ daughter_of_tom(anna)

⎩⎪ tall(robert) ⇐ son_of_tom(robert)

Given our propositional rule of definitional reflection, we could just infer propositional results such as child_of_tom(anna) ftall(anna) or child_of_tom(robert) ftall

(robert). However, what we would like to infer is the principle

child_of_tom(x ) ftall(x )

with free variable x , since anna and robert are the only objects for which the predicate child_of_tom is defined, and since for them the desired principle holds.

In an even more general case, we have clauses that contain variables the instances of which match instances of the claim we want to obtain by definitional reflection. Consider the definition

D r p(y, a) ⇐ q(y)

1 p(x , f (a)) ⇐ q( f (x ))

According to the principle of general definitional reflection, we obtain, with respect to D1,

p(a, z) fq(z)

The intuitive argument is as follows: Suppose p(a, z). Any, and in fact the only, substitution instance of p(a, z) that can be obtained by the first clause is generated by substituting a for y in the first clause, and a for z in p(a, z). We denote this substitution by [a/y, a/z] and call it σ1. Any, and in fact the only, substitution instance of p(a, z) that can be obtained by the second clause is generated by substituting a for x in the second clause, and f (a) for z in p(a, z). We denote this substitution by [a/x , f (a)/z] and call it σ2. When σ1 is applied to the body of the first clause, q(a) is obtained, which is also obtained when σ1 is applied to q(z). When σ2 is applied to the body of the second clause, q( f (a)) is obtained, which is also obtained when σ2 is applied to q(z). Therefore, we can conclude q(z). In the propositional case we could describe definitional reflection by saying that every C that is a consequence of each defining condition is a consequence of the definiendum a. We cannot now even identify a single formula as a definiendum, as any formula which is a substitution instance of a head of a definitional clause is considered to be defined. Therefore we should now say: Suppose a formula a is given. If for each substitution instance aσ that can be obtained as bσ from the head of a clause b ⇐ C, we have that Cσ implies Aσ for some A, then A can be inferred from a.

Formally, this leads to a principle of definitional reflection according to which, for the introduction of an atom a on the left side of the turnstile, the most general unifiers mgu(a, b) of a with the heads of all definitional clauses are considered:

{rσ,Cσ f Aσ :σ =mgu(a,b)for s ome clause b⇐ Cin D}fω

r, a fA

with the proviso: The variables free in r, a fA must be different from those in the b ⇐ C above the line. This means that we always assume that variables in clauses

are standardised apart. We call this principle the ω-version of definitional reflection, as it is in a certain way related to the ω-rule in arithmetic, a point that we cannot elaborate on here (see Schroeder-Heister [55]). This powerful principle is typical of applications outside logic. When we consider logical definitions such as Dlog, we see that each formula T (a), where a is a compound logical formula, determines exactly a single head b in one or two clauses (two in the case of disjunction), such that T (a) is a substitution instance of b. This means that (1) there is just matching and no unification between b and T (a), and (2) there is just a single substitution for the main logical connective in T (a) involved due to the strict separation between the clauses for the different logical connectives, implying that there is no overlap between substitution instances of clauses.

The power of the ω-version of definitional reflection is demonstrated, for example,

by the fact that the rules of free equality can be obtained from the definition consisting of the single clause

D= { x = x ⇐

For example, the transitivity of equality is derived by a single inference step as follows:

(D= f-) x 2 =x3 fx2 =x3

ω x1 = x2, x2 = x3 fx1 = x3

Here we use that the substitution [x2/x1, x2/x ] is an mgu of x1 = x2 with the head

x = x of the clause x = x ⇐ . In a similar way, all freeness axioms of Clark's

equational theory [35] can be derived.15

Found a mistake? Please highlight the word and press Shift + Enter