I'm a really beginner in Mathematical Logic.I'm currently reading Shoenfield Mathematical's Logic He say theorems of formal system F should satisfy the two laws :
1) The axioms of F are theorems of F .
2) If all the hypotheses of a rule (mean rule of inference ) of F are theorems of F then the conclusion of the rule is a theorem of F .
first question how we consider axioms as theorems ?
second thing he say
if we let $S_0$ be the set of axioms so by (i) they are theorems Let $S_1$ be the set of formulas which are conclusions of rules whose hypotheses are all in $S_0$ ; then they are theorems by (ii) and let $S_w$ be the set of formulas which are conclusions of rules whose hypotheses are all in at least one of $S_0,S_1,....$; these are again theorems by (ii) . we continue this way until no new theorems can by obtained by (ii) and we have all of the theorems.
can it possible we derive all theorems in formal system and we can't derive more theorems ?
First question: Conceptually, 'theorem' is something that we consider to be true once we assume certain axioms to be true. And yes, typically, those theorems are inferred from the axioms, so it seems unintuitive to consider axioms as theorems, but once we assume certain axioms to be true, then ... those axioms are true. And so yes, axioms are theorems.
Second question: If you are asking whether we can practically derive all theorems until we're done, then for almost any logic system the answer is no. For example, suppose you have as an axiom $A$, and suppose you have inference rule:
$$\varphi$$
$$\psi$$
$$\therefore \varphi \land \psi$$
Then:
$S_0 = \{ A \}$
$S_1 = \{A, A \land A \}$
$S_2 = \{A, A \land A, A \land A \land A, A \land A \land A \land A \}$
etc.
That is, there is no $n$ such that $S_{n+1} = S_n$, and so you are never 'done' if you generate this step by step by hand or using some computer.