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>

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
*