Re: decidable

bargiax wrote:
"MoeBlee" wrote:
There is an algorithm such that for any given statement A, if there is
a proof of A, then the algorithm verifies that there is a proof of A ,
and if there is not a proof of A, then the algorithm verifies that
there is not a a proof of A .

One more little comment. You used the statement "if there is a proof of A".
However, I read that this algorithm can tell if a formula is valid or not
even when we are *not* assuming that there is a proof of A:

Where 'theory' is defined as 'a set of sentences closed under
entailment', in the context of my definition, "proof of A" means a
proof from some axioms for the theory (even if the theory is not
recursively axiomatizable, the theory is still non-recursively
axiomatized by itself, i.e., every member of the theory is an axiom for
the theory). I'm not attached to using the notion of 'proof' here (as I
recall, proof had been previously mentioned, so I was just going along
with using the notion.) In fact, it is more direct just to say:

There is an algorithm such that for any given statement A, if A is a
member of the theory, then the algorithm verifies that A is a member of
the theory, and if A is not a member of the theory, then the algorithm
verifies that A is not a member of the theory.

So for theories, the algorithm determines whether a sentence is or is
not a member of the theory. Trivially, to be a member of a theory is to
be entailed by the theory, whether the theory is recursively
axiomatizable or not. But, by the completeness and compactness theorems
(I presume that we're talking about first order theories), a sentence
is entailed by a set of sentences iff the sentence is provable from a
finite subset of that set of sentences. We don't need to mention
'proof' and it might be more economical not to mention 'proof', but for
first order theories, it is not incorrect, though perhaps unnecessarily
complicating to refer to 'proof' thus to discuss the theory in
syntactical rather than semantic terrms.

But the sense of 'validity' here is that of consequence (recall that a
sentence is a consequence of the theory iff the sentence is a member of
the theory), not that a sentence is or is not a valid sentence. In
other words, decidable theories have sentences as members that might
not be valid sentences but that are a consequence of the theory, and in
paticular, a consequence of a recursive set of axioms if the theory is
recursively axiomatizable.

The only theory that has as members only valid sentences is indeed the
set of valid sentences, and, by Church's theorem, that theory is not
decidable. There is no algorithm to determine of an arbitrary sentence
whether it is or is not valid.

MoeBlee

.

Relevant Pages

  • Re: MY LIST of the subsets of N
    ... I haven't gone through all the details of your algorithm, ... but I wonder of it's odd or even. ... S is the number fitself a member of S? ... Very curious function this f. ...
    (sci.math)
  • Re: Recursively enumerable sets
    ... If n is not a member of the ... If an r.e. set happens to have the property that its complement is also ... exactly one of the two lists. ... this algorithm may run forever." ...
    (comp.theory)
  • Re: Recursively enumerable sets
    ... If n is not a member of the ... this algorithm may run forever." ... I know you already wrote me that the algorithm may run forever. ... What about evens plus "3"? ...
    (comp.theory)
  • Re: Recursively enumerable sets
    ... If n is not a member of the ... If an r.e. set happens to have the property that its complement is also ... this algorithm may run forever." ... I know you already wrote me that the algorithm may run forever. ...
    (comp.theory)
  • Re: decidable
    ... we have an algorithm to verify this". ... That entails that every statement ... a proof of A, then the algorithm verifies that there is a proof of A, ...
    (sci.logic)