Re: log:forAll makes sense? [was: Can we agree on triples ?]

> >and the former is, say,
> >
> >         (log:forall '?a '(loves ?a mary))
> >
> >where log:forall is defined so that this expands to
> >
> >         (wtr '(forall (?a) (loves ?a mary)))
>
> Er, what's "wtr" meant to stand for here?

from http://logic.stanford.edu/kif/dpans.html
[[[
The KIF truth predicate is called wtr (which stands for ``weakly true'').
For example, we can say that a sentence of the form (=> (p ?x) (q ?x))
is true by writing the following sentence.

    (wtr '(=> (p ?x) (q ?x)))

This may seem of limited utility, since we can just write the sentence
denoted by the argument as a sentence in its own right. The advantage of
the metanotation becomes clear when we need to quantify over sentences,
as in the encoding of axiom schemata. For example, we can say that every
sentence of the form (=> p p) is true with the following sentence.
(The relation sentence can easily be defined in terms of quote, listof,
indvar, seqvar, and word.

    (=> (sentence ?p) (wtr ^(=> ,?p ,?p)))

Semantically, we would like to say that a sentence of the form (wtr 'p)
is true if and only if the sentence p is true. Unfortunately, this causes
serious problems. Equating a truth function with the meaning it ascribes
to wtr quickly leads to paradoxes. The English sentence ``This sentence
is false.'' illustrates the paradox. We can write this sentence in KIF
as shown below. The sentence, in effect, asserts its own negation.

    (wtr (subst (name ^(subst (name x) ^x ^(truth ,x)))
                ^x
                ^(not (wtr (subst (name x) ^x ^(not (wtr ,x)))))))

No matter how we interpret this sentence, we get a contradiction. If we
assume the sentence is true, then we have a problem because the sentence
asserts its own falsity. If we assume the sentence is false, we also have
a problem because the sentence then is necessarily true.
Fortunately, we can circumvent such paradoxes by slightly modifying the
proposed definition of wtr. In particular, we have the following axiom
schema for all p that do not contain any occurrences of wtr. For all p
that do contain occurrences, wtr is false.

    (<=> (wtr 'p) p)

With this modified definition, the paradox described above disappears,
yet we retain the ability to write virtually all useful axiom schemata
as metalevel axioms.
From the point of view of formalizing truth, wtr is a cheat, since it
fails to cover those interesting cases where sentences contain the
truth predicate. However, from the point of view of capturing axiom
schemata not involving the truth predicate, it works just fine.
Furthermore, unlike the solutions to the problem of formalizing truth,
the framework presented here is easy for users to understand, and it
is easy to implement.
]]]

I guess you would express that in N3 as
  {{stmts} log:implies {stmt}} a log:Truth; log:forAll vars.

[wrt to paradoxes and their negation, we would rather say no-proof-found]

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Tuesday, 3 April 2001 08:10:07 UTC