Information Technology Reference
In-Depth Information
Theorem 1.
Let
Q
be a prefix, and
S
be a set of
Q
-sequents. For every substi-
Q ,
tution
ϕ
we have:
ϕ
is a
Q
-substitution satisfying
iff there is a prefix
Q -substitution
ϕ such that
a substitution
ρ
and a
ρ∗ (
Q , ∅
(
Q, S
)
)
,
ρ ◦ ϕ )
ϕ
=(
Q .
Examples. 1. The sequent
∀y.∀zRyz → Q, ∀y 1 ,y 2 Ry 1 y 2 ⇒ Q
leads first to
∀y 1 ,y 2 Ry 1 y 2 ⇒ Ryz
under
∃y∀z
,thento
y 1 =
y ∧y 2 =
z
under
∃y∀z∃y 1 ,y 2 ,and
finally to
Y 1 z
=
y ∧Y 2 z
=
z
under
∃y, Y 1 ,Y 2 ∀z
, which has the solution
Y 1 =
λzy
,
Y 2 =
λzz
.
2.
∀y.∀zRyz → Q, ∀y 1 Ry 1 y 1 ⇒ Q
leads first to
∀y 1 1
Ry 1 y 1 ⇒ Ryz
under
∃y∀z
,thento
y 1 =
y ∧ y 1 =
z
under
∃y∀z∃y 1 , and finally to
Y 1 z
=
y ∧ Y 1 z
=
z
∃y, Y 1 ∀z
under
, which has no solution.
3. Here is a more complex example (derived from proofs of the Orevkov-
formulas), for which we only give the derivation tree.
(
)
R
0
zRz
∀zS
0
z→⊥
1
S
0
z 1 →⊥
S
0
z 1
Rzz 1 →⊥
∀z 1 Rzz 1 →⊥
∀y.
(
∀z 1 Ryz 1 →⊥
)
→⊥
∀z 1 Rzz 1 →⊥
→⊥
(
)
∀y.
(
∀zRyz→⊥
)
→⊥
z→⊥
∀zR
R
0
(
∀zR
0
z→⊥
)
→⊥
0
z→⊥
where (
) is a derivation from Hyp 1 :
∀z, z 1 .R
0
z → Rzz 1 → S
0
z 1 .
5Ex en onby and
The extension by conjunction is rather easy; it is even superfluous in princi-
ple, since conjunctions can always be avoided at the expense of having lists of
formulas instead of single formulas.
However, having conjunctions available is clearly useful at times, so let's add
it. This requires the notion of an elaboration path for a formula (cf. [1]). The
reason is that the property of a formula to have a unique atom as its head is
lost when conjunctions are present. An elaboration path is meant to give the
directions (left or right) to go when we encounter a conjunction as a strictly
positive subformula. For example, the elaboration paths of
∀xA ∧
(
B ∧ C →
D ∧∀yE
)are( left ), ( right , left )and( right , right ). Clearly, a formula is
equivalent to the conjunction (over all elaboration paths) of all formulas obtained
from it by following an elaboration path (i.e., always throwing away the other
part of the conjunction). In our example,
∀xA ∧
(
B ∧ C → D ∧∀yE
)
↔∀xA ∧
(
B ∧ C → D
)
(
B ∧ C →∀yE
)
.
Search WWH ::




Custom Search