Open arademaker opened 5 years ago
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
Shall we close this then?
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
That's fine, just trying to make sure the issue is clear... (not really clear to me so far).
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)))))))
The axiom from the banana slug example:
is transformed to the FOF/TPTP axiom below:
Despite the possible equivalence of these assertions, the incomplete proof below becomes much more complex than necessary with such translation: