I was wondering if every closed formula is decidable (in a complete system). Clearly a non closed formula is not decidable, since it can take some values for which it is true, and other for which it is false. Let's assume the following definiton of decidability:
In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer.
Question 1
If however we add quantifier to the formula, is true that it can be either true or false, but in my opinion how can it be decidable, if I cannot prove it? (for example a conjecture still unproven).
Question 2
Given a specific and known algorithm, the question for every input does the program halts (which should be a closed question) is it decidable or not? Is the set of input a recursive set or not?
The definition of a complete system is that for every sentence (closed formula), either it or its negation is a theorem. Therefore it is "decidable", in an extended sense (see below) with this procedure: simply start churning out all possible theorems, and wait for the formula or its negation to show up.
The definition of decidable is that there is an algorithm to determine whether any given sentence (closed formula) is a theorem. Hence the caveat: for this procedure to be a true algorithm (effective procedure), you need a way to mechanically generate all the axioms. Otherwise, the procedure is computatable only "relative to the set of axioms".
So for example, so-call True Arithmetic (sometimes called Full Arithmetic), the set of all sentences (closed formulas) that are true in the standard model, isn't truly decidable, because we have no way of algorithmically (i.e., computably) generating all the axioms of this system.
The notion of relative computability is well-established in computability theory (aka recursion theory). So the extended sense is pretty natural. However, it's not the standard meaning of "decidable" for theories in logic.