> None of this matters much for most of us who read this list, but I
> think your reference from 1950 is not quite right, or rather its a
> non-standard way of putting it:
> A Remark Concerning Decidability of Complete Theories, Antoni
> Janiczak, The Journal of Symbolic Logic, Vol. 15, No. 4 (Dec.,
> 1950), pp. 277-279:
> "A formalized theory is called complete if for each sentence
> expressible in this theory either the sentence itself or its
> negation is provable."
> Completeness normally (see e.g. Wikipedia) means that for every
> sentence S expressible in a language either S or ~S is derivable
> from the associated axioms, and that all sentences so derived are
> true (i.e. theorems). That is not the same at all as the system/set/
> language being decidable--i.e. that for any S there is an effective
> procedure for determining whether or not it is derivable.
> "provable" in that quote fudges this issue.
I think you're just re-stating what Rob's quote says: as far as I know, a sentence S is called "provable" if it can be derived from the axioms of the theory by applying the "proof rules" of the theory. That does not imply it has to be decidable in finite time whether S or ~S is provable.
A happy weekend to everyone on the list, Stefan Evert