- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 25 Sep 2003 16:51:50 -0500
- To: Jos De_Roo <jos.deroo@agfa.com>
- Cc: Pat Hayes <phayes@ai.uwf.edu>, www-rdf-logic@w3.org
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/
Received on Thursday, 25 September 2003 17:51:51 UTC