I was puzzeling with the almost standard definition of completeness:
In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be incomplete.
[From http://en.wikipedia.org/wiki/Completeness_%28logic%29, bold added]
Normal for prooftheory that particular property just is that the formula (or its negation) is also true (or false) false in some (or every or none) model (or world or frame) of modeltheory.
Other properties (for example something like "the formula contains an P" ) are definitly not the kind of property that is mend here, but still the definition doesn't indicate that such a property is not a particular property as we would like.
So therefore my question:
What are those particular properties that are mend here?, Is there a more succinct definition of what kind of properties are allowable here?
added later after studying RINDphi's answer (Thanks!) is the word derive right in the description. is it not much more about production rules of formal grammar?
see see en.wikipedia.org/wiki/Formal_grammar and en.wikipedia.org/wiki/Production_%28computer_science%29
( a deduction rule is just an production rule with more than one input line )
Well, I guess that "particular property" is just a placeholder for the properties that follow in the same Wikipedia page:
The definition must, in my opinion, be understood with respect to the section that follows. To my knowledge, completeness normally refers to "strong completeness", i.e. if a formula is true, it must be derivable.
/edit:
In a formal proof system, you usually derive from a set of axioms, using the rules, further formulas, which are theorems of the system. This may probably also be understood in the sense of a grammar, with the axioms as initial symbol and the rules as productions. However, this does in my opinion not render the term "derive" actually improper.
Regarding the properties: I think that you may really choose any property you like. For example, "the formula contains exactly two occurrences of the predicate P". Then the system is complete w.r.t. that property, if every formula containing exactly two occurrences of P can be derived. The question whether or not this is a sensible property does not matter here: Of course there are more and less interesting completeness properties one may wish to investigate.