Re: decidable


bargiax wrote:
"MoeBlee" <jazzmobe@xxxxxxxxxxx> ha scritto nel messaggio
news:1150489607.451354.158510@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
bargiax wrote:
In the section 1.4 Mendelson's book cites the decidability of a theory
saying that a formal theory is decidable if, given a statement A, there
exist a proof of A and we have an effective procedure (or algorithm) to
verify this.

You've mistated the definition of 'decidable theory'. Roughly put, a
theory is decidable iff there is an algorithm to determine, for any
given sentence of the language, whether or not the sentence is a
theorem of the theory.



Hmm... I read that the procedure is going to know wether a proof exists or
not. A theorem is the last proposition in a proof, right?

Yes, but you said "given a statement A, there exists a proof of A and
we have an algorithm to verify this". That entails that every statement
is a theorem and we have an algorithm to verify that every statement is
a theorem. You might have meant "given a statement A, if there exists a
proof of A then there exists an algorithm to verify that there is a
proof of A", and that would make more sense. But still, for a
decidability we need not just an algorithm to verify that a sentence
has a proof if it has a proof, but rather the algorithm should ALSO
verify that the sentence does not have a proof if it does not have a
proof.

MoeBlee

.

Relevant Pages

  • Re: decidable
    ... saying that a formal theory is decidable if, given a statement A, ... exist a proof of A and we have an effective procedure (or algorithm) ... we have an algorithm to verify this". ...
    (sci.logic)
  • Re: Why NP Problem is Important and Practical Examples
    ... there is a poly-time algorithm to verify a particular solution. ... My student was working as a software developer and he was meeting ...
    (comp.theory)
  • Re: Is code duplication allowed in this instance?
    ... code duplication, I suppose such terms like 'DRY' are meant to back ... So in this scenario is it OK to duplicate the algorithm to be tested ... within test codes to verify itself. ... as rigorous as preparing the data set with the known ...
    (comp.lang.python)
  • Re: Licensing Components
    ... Suppose you have an "Algorithm A" that creates a short hash of something ... Verify if the first part of the two match, ... you can use the second part to grant licenses, unlock versions, etc. ...
    (borland.public.delphi.thirdpartytools.general)