Axiom Systems and Formal Systems

I'm a really beginner in Mathematical Logic.I'm currently reading Shoenfield Mathematical's Logic and i'm having a hard time trying to relate the concept of Formal Systems with the concept of Axiom System ( or Axiomatic System ).

I know any Formal System has 3 constituents : a language, a set of axioms ( certain expressions in that language ) , and rules of inference.

What about an Axiom System ?
Shoenfield describes it more or less as :
"An axiom system is the entire eddifice which a mathematician constructs, consisting of basic concepts and axioms ( describing them ) and derived concepts and derived theorems ( describing them )."
I'm not well to sure how he defined it.
Did he mean an Axiom System is just a set ( of axioms and derived theorems ) ?

Is the reason he didn't introduce the need of a language in an Axiom System, the fact that an axiom is mainly idea ( which can or can not be formalized through a syntax ) ?

What is the reason he didn't introduce in the definition of Axiom Systems, the need of rules of inference ( to derive the Theorems ) ?

How does the concept of Axiom Systems differ from the concept of Formal Systems ?

P.S : I made a search and discovered Mathematical Logic is mainly divided into Proof Theory, Model Theory and Recursion Theory.Where would my question fit ? I also can't seem to solve my doubt by other Mathematical Logic books ( Stephen Klenee, Van Dallen, Machover ) because i couldn't find the description of Formal Systems and Axiom Systems, they usually start right away with some kind of Calculus and First-order. A book recommendation which would cover this ( formal system, language, axiom system, etc ) would also be really helpful.

• There is no need to define any of these things in general. For specific items, like first-order logic, language, logical axioms, logical rules of inference, theory-dependent axioms are all carefully defined in Shoenfield. His book is really quite good. Just doesn't get far enough in Model Theory. – André Nicolas Jun 1 '13 at 0:59
• Forget about Wikipedia, it often tries to define what there is no point in trying to define. Concentrate (for now at least) on first-order logic, that is where most of the serious progress has been since the $1930$'s. – André Nicolas Jun 1 '13 at 1:15
• I am suggesting only that you confine yourself for now to first-order logic. – André Nicolas Jun 1 '13 at 1:26
• Completeness has two almost unrelated meanings. The ordinary formulations of first-order logic (there are many, all equivalent) are complete, in that a sentence of a language $L$ is provable iff it is true in all $L$-structures. Various theories, such as the theory of algebraically closed fields of characteristic $0$, are complete in that any sentence $\varphi$ is either provable or refutable. – André Nicolas Jun 1 '13 at 1:29
• Different authors have different names for these things, so it's likely that you won't find these exact definitions in other books. I haven't read Schoenfield, so I don't know what his definitions are, but based on your descriptions, my guess is the following: Axiom Systems are sometimes call "Hilbert systems", and Formal Systems are sometimes called "Natural Deduction Systems." They're both proof systems, and they're usually equivalent (anything you can prove in the first type of system you can prove in the corresponding system of the second type, and vice versa). – Alex Kocurek Jun 1 '13 at 2:42

Euclid's Elements satisfies the criteria for being an axiomatic system. It does not, however, satisfy the criteria for being a formal system; the reason being that, from the point of view of formalism, certain steps in Euclid's proofs are left implied or tacit. In other words: all formal systems are axiomatic, but not all axiomatic systems are formal.

In nearly all practicality - except when studying formal systems - one would rarely do work in a bona fide formal system, but always in an axiomatic, or one is not doing math.

A useful suggestion is Richard Kaye, The Mathematics of Logic, (Cambridge U.P., 2007).

In Chapter 3 : Formal systems, he describes formal systems as :

kinds of mathematical games with strings of symbols and precise rules.

Rules are of two basic kind :

• rules of formation : how to generate well formed (i.e.admissible) strings

• rules of transformation : how to produce new (well formed) strings from existing ones.

The following chapters deal with the typical formal systems of Math Log : Propositional Logic and First-Order Logic.

• Thanks. +1. (1) Do "rules of formation" generate strings from nothing? (2) Are "rules of formation" the formal grammar? (3) Are "rules of transformation" used in defining a language inductively or recursively from some basic strings? (4) how do you transform between "rules of formation" or a formal grammar and "rules of transformation"? See also cs.stackexchange.com/q/28534/336 – Tim Jul 19 '14 at 17:49
• @Tim - (1) Yes; you can start from the null string or from an "assumed" string. (2) formation rules are like production rules in a formal language. The rules describe how to form strings from the language's alphabet that are valid according to the language's syntax. (3) in a logical system, transformation rules are deduction or inference rules : licence us to produce new well formed string (i.e. formulas) from already existing ones; in the end: generate theorems from axioms. See this post – Mauro ALLEGRANZA Jul 20 '14 at 17:00