W3C home > Mailing lists > Public > www-webont-wg@w3.org > January 2002

the decision stuff requirement

From: <jos.deroo.jd@belgium.agfa.com>
Date: Wed, 16 Jan 2002 22:12:08 +0100
To: www-webont-wg@w3.org
Message-Id: <41256B43.00747CAE.00@ambem5.eps.agfa.be>
I'm trying to follow the decision stuff requirement...
To begin with, I like the following from Alfred Tarski
[[[
We shall now consider two methodological concepts which are
of great importance from the theoretical point of view, while in
practical respects they are of little significance. They are the
concepts of CONSISTENCY and of COMPLETENESS.
A deductive theory is called CONSISTENT or NON-CONTRADICTORY
if no two asserted statements of this theory contradict each other,
or, in other words, if any two contradictory sentences at least one
*cannot* be proved. A theory is called COMPLETE, on the other hand,
if of any of two contradictory sentences formulated exclusively in
the terms of the theory under consideration (and the theories
preceding it) at least one sentence *can* be proved in this theory.
Of a sentence which has the property that its negation can be
proved in a given theory, it is usually said that it can be
DISPROVED in that theory. Both terms ``consistent'' and ``complete''
are applied, not only to the theory itself, but also to the
axiom system upon which it is based.
Closely connected with the problem of completeness is another,
more general, problem which concerns incomplete as well as
complete theories. It is the problem which consists in finding,
for the given deductive theory, a general method which would
enable us to decide whether ot not any particular sentence
formulated in the terms of this theory can be proved within
this theory. This important problem is known as the DECISION
PROBLEM.
]]]

A while ago I tried the Russell paradox (with the Euler proof method)
i.e. starting from
  this log:forAll :x .
  { :x a :R } log:implies { { :x a :x } a log:Falsehood } .
  { { :x a :x } a log:Falsehood } log:implies { :x a :R } .
we could neither prove
  :R a :R .
nor
  { :R a :R } a log:Falsehood .
so there is CONSISTENCY but INCOMPLETENESS

OK, this is a very controversial example, which is
also out of charter, so let's not discuss it further
all I wanted to say is that I (now) think that
  CONSISTENCY is a requirement
  COMPLETENESS is not a requirement
  DECISION PROBLEM: there must exist effective mechanisms

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Wednesday, 16 January 2002 16:12:43 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:47 GMT