non equivalent transformation of axiom

[arademaker]

The axiom from the banana slug example:

(=>
  (and
   (instance ?A Animal)
   (not
     (exists (?PART)
       (and
        (instance ?PART SpinalColumn)
        (part ?PART ?A)))))
  (not
   (instance ?A Vertebrate)))

is transformed to the FOF/TPTP axiom below:

/*
(forall (?A)
 (exists (?PART)
  (and (instance ?PART Object)
   (=>
    (and 
       (instance ?A Animal)
       (not (and (instance ?PART SpinalColumn) (part ?PART ?A))))
    (not (instance ?A Vertebrate))))))
*/
fof(a72773,axiom,! [A] : (? [PART] : (
 (s_instance(PART, s_Object) & ((s_instance(A, s_Animal) & 
  (~ (s_instance(PART, s_SpinalColumn) & s_part(PART, A)))) => 
    (~ s_instance(A, s_Vertebrate))))))).

Despite the possible equivalence of these assertions, the incomplete proof below becomes much more complex than necessary with such translation:

lemma BSnotVert (hne : nonempty U) : ¬(ins BananaSlug10 Vertebrate) :=
begin
 cases id hne with a,
 have h₁, from a72773 BananaSlug10,
 _ 
end

a72772 : ins BananaSlug10 Animal,
a72773 :
  ∀ (a : U),
    ∃ (p : U), ins p Object ∧ (ins a Animal ∧ ¬(ins p SpinalColumn ∧ part p a) 
       → ¬ins a Vertebrate),
a72774 : ∀ (s : U), ins s Object → ¬(ins s SpinalColumn ∧ part s BananaSlug10),
hne : nonempty U,
a : U
⊢ ¬ins BananaSlug10 Vertebrate

[arademaker]

As @fcbr pointed out, the axioms in KIF and their versions after the transformation with the relativization of the variables are not equivalent A simple example:

(domain foo 1 Something)
(foo ?A)

is not equivalent to:

(=> 
 (instance ?A Something)
 (foo ?A))

To further convince ourselves, we can use Lean to show the incomplete proof:

/-
(=>
  (and
   (instance ?A Animal)
   (not
     (exists (?PART)
       (and
        (instance ?PART SpinalColumn)
        (part ?PART ?A)))))
  (not (instance ?A Vertebrate)))

(forall (?A)
 (exists (?PART)
  (and 
   (instance ?PART Object)
   (=>
    (and 
     (instance ?A Animal)
     (not (and (instance ?PART SpinalColumn) (part ?PART ?A))))
    (not (instance ?A Vertebrate))))))

simplifying 

 (not (instance ?A Vertebrate))                      = nv ?A
 (and (instance ?PART SpinalColumn) (part ?PART ?A)) = q ?PART ?A
 (instance ?PART Object)                             = io ?PART
 (instance ?A Animal)                                = ia ?A
-/

constant U : Type
constants q : U → U → Prop
constants nv ia io : U → Prop

example (hne : nonempty U) : 
  (∀ a : U, (ia a ∧ ¬ (∃ p : U, q p a)) → nv a) ↔
  (∀ a : U, ∃ p : U, io p ∧ ((ia a ∧ ¬ q p a) → nv a)) :=
begin
 apply iff.intro, 
 intro h, 
 intro x,
 have h₁, from h x,
 existsi x,
 split,
end

The proof state is:

3 goals
hne : nonempty U,
h : ∀ (a : U), (ia a ∧ ¬∃ (p : U), q p a) → nv a,
x : U,
h₁ : (ia x ∧ ¬∃ (p : U), q p x) → nv x
⊢ io x

hne : nonempty U,
h : ∀ (a : U), (ia a ∧ ¬∃ (p : U), q p a) → nv a,
x : U,
h₁ : (ia x ∧ ¬∃ (p : U), q p x) → nv x
⊢ ia x ∧ ¬q x x → nv x

hne : nonempty U
⊢ (∀ (a : U), ∃ (p : U), io p ∧ (ia a ∧ ¬q p a → nv a)) →
  ∀ (a : U), (ia a ∧ ¬∃ (p : U), q p a) → nv a

[fcbr]

Shall we close this then?

[arademaker]

No. The main problem here is not the equivalence of the pre and post relativization. But the transformation is suspicious. The assertion about a non existence of an entity is transformed into the existence of something with a particular type. I am still not convinced that it is the intensional meaning of the original axiom. Not that we need another terminology for the intensional semantics of suo-kif since we can’t talk about logical equivalence

[fcbr]

That's fine, just trying to make sure the issue is clear... (not really clear to me so far).

[arademaker]

Adam:

( ! [V__AGENT,V__OBJ] :
    ((s__instance(V__AGENT,s__Agent) & s__instance(V__OBJ,s__Object)) =>
     (s__exploits(V__OBJ,V__AGENT) =>
		 (? [V__PROCESS] :
		    (s__instance(V__PROCESS,s__Process) &
		     (s__agent(V__PROCESS,V__AGENT) &
			      s__resource(V__PROCESS,V__OBJ)))))) )

Our:

! [OBJ,AGENT] :
 (? [PROCESS] : 
   ((s_instance(PROCESS, s_Process) & 
   ((s_instance(OBJ, s_Object) & s_instance(AGENT, s_Agent)) =>
    (s_exploits(OBJ, AGENT) => (s_agent(PROCESS, AGENT) 
 & s_resource(PROCESS, OBJ)))))))