First order Logic deducing theorems

Question

We are in First Order Logic and I have a set of rules and clauses ( = axioms).

I use a sound and complete deductive system and the rules of inference in order to derive some formulas from the initial set.

Is it correct to call "theorems" these derived formulas?

Answer 1

Yes: theorems are true statements that you can prove from inside the system.

Answer 2

Yes. To provide more context:

• A theory is a deductively closed collection of formulas
• We call the individual formulas the theorems of the theory

Any collection of formulas can be used to generate a theory, which is the smallest theory containing those axioms. When we do this, we call the individual formulas from the starting collection "axioms".

The theorems of the theory generated from a set of axioms are precisely the formulas that can be derived from the rules of inference.

(I assume throughout this post a fixed collection of rules of inference)

Answer 3

It would probably be better to call them theorems of the theory.

For example, $x(x^2)=(x^2)x$ is a theorem of first-order group theory - calling it just a "theorem" seems dubious.

Answer 4

'Theorems' are those things that you can derive from axioms.

The axioms specify the subject matter, and hence what the theorems are theorems 'of' or 'about'

Thus, if the axioms are basic logical tautologies, then the theorems are theorems of logic .. which are further tautologies.

If the axioms are about set theory, or number theory, then the theorems are about those areas. Etc.