|
[t/u ]P τ |
= P [t/u ]τ | |
|
[t/u ]τ 1 Rτ 2 |
= [t/u ]τ 1 R[t∕u ]τ 2 | |
|
[t/u](τ 1 is τ2 ) |
= [t/u]τ 1 is [t/u]τ2 | |
|
[t/u ]not Φ |
= not [t/u]Φ | |
|
[t/u ](Φ or Ψ) |
= [t/u ]Φ or [t/u ]Ψ | |
|
[t/u](φ ⇒ ψ) |
= [t/u]φ ⇒ [t/u]Ψ |
if u ∈∕ adr (Φ) |
|
[t/u](φ ⇒ ψ) |
= [t/u]φ ⇒ Ψ |
if u ∈ adr (Φ) |
|
[t∕u][~u | γ1, . . . ,γm] |
= [~u | [t∕u]γ1 , . . . , [t∕u]γm] |
if u ∈∕ {~u} |
|
[t∕u][~u | γ1, . . . ,γm] |
= [~u | γ1 , . . . , γm] |
if u ∈ {~u} |
|
[t∕u](Φ; Ψ) |
= [t∕u]Φ; [t∕u]Ψ |
if u ∈∕ adr(Φ) |
|
[t∕u](Φ; Ψ) |
= [t∕u]Φ; Ψ |
if u ∈ adr(Φ) |
The next definition gives our translation function ↑ from boxes and condi-
tions to first-order formulae. The variable x that is appearing in the sixth
and eighth clauses is supposed to be fresh in both cases, i.e. it is defined to
be the first variable in some fixed ordering that does not occur (at all) in
Φ or in Ψ. Note that the sequencing operation ; is associative: Φ; (Ψ; Ξ) is
equivalent with (Φ; Ψ); Ξ for all Φ, Ψ and Ξ. This means that we may assume
that all boxes are either of the form [~u | ~γ]; Φ or of the form [~u | ~γ]. We shall
use the form [~u | ~γ]; Φ to cover both cases, thus allowing the possibility that
Φ is empty. If Φ is empty, Φ ⇒ Ψ denotes Ψ.
(P τ )t = P (τ )t
(τ 1 Rτ 2 )t = R(τ 1 )t(τ 2 )t
(τ 1 is τ2)t = (τ 1 )t = (τ2)t
(not Φ)t = — (Φ)t
(φ or Ψ)t = Φt ∨ Ψt
(([u~ | ~]; Φ) ⇒ Ψ)t = ∀x([x∕u](([~ | ~]5Φ) ⇒ Ψ))t
(([ | γι,...,Ym]5Φ) ⇒ Ψ)t = (7ιt ∧ ... ∧ .) → (Φ ⇒ Ψ)t
([u~u | ~γ]; Φ)t = ∃x([x∕u]([~u | ~γ]; Φ))t
([ | γ1, . . . , γm]; Φ)t = γ1t ∧ . . . ∧γmt ∧ Φt
By way of example, the reader may verify that the function f sends (14) to
(15).
(14) [ | [u1 u2 | man u1 , woman u2, u1 bores u2] ⇒ [ | u2 ignores u1]]
(15) ∀x1 x2 ((man(x 1 ) ∧ woman(x2) ∧ bores (x 1 )(x2)) → ignores (x 2)(x 1))
It is clear that the function f is algorithmic: at each stage in the reduction of
a box or condition it is determined what step should be taken. The following
12
More intriguing information
1. Testing the Information Matrix Equality with Robust Estimators2. Sex differences in the structure and stability of children’s playground social networks and their overlap with friendship relations
3. The Clustering of Financial Services in London*
4. Inflation and Inflation Uncertainty in the Euro Area
5. The constitution and evolution of the stars
6. The InnoRegio-program: a new way to promote regional innovation networks - empirical results of the complementary research -
7. The name is absent
8. Une Gestion des ressources humaines à l'interface des organisations : vers une GRH territoriale ?
9. TRADE NEGOTIATIONS AND THE FUTURE OF AMERICAN AGRICULTURE
10. A Bayesian approach to analyze regional elasticities