Re: evidence for forall? [was: test based on OWL guide...]

Ouch; my brain hurts...

On Thu, 2003-09-25 at 16:41, Jos De_Roo wrote:
[...]
> no need for quantifiers in a language of logic of proof;
> they belong to the object language of predicate logic
> and they are for instance explicitly mentioned in proof
> term
> -->term<--
>  { { [ iw:Variable "?X" ] = :socrates.
>      [ iw:Variable "?X" ] a :Man } =>
>    { :socrates a :Man } }  =>
> { :socrates a :Mortal }.
> which is a proof of
> -->:formula<--
> :socrates a :Mortal.
> 
> hmm...

hmm... is that term a proof of { :socrates a :Mortal } from
no premises? Or is the proof term a sort of function
that takes a proof of
 { ?X a :Man } => { ?X a :Mortal }.
and a proof of
 :socrates a :Man.
and returns a proof of
 :socrates a :Mortal.
?


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/