Are axioms assumed to be true in a formal system?

In a logical system, there is assignment of truth values to the sentences in the language, and axioms are assigned the true value.

A logical system is a formal system.

In a formal system, there is no truth value assignment, but there are still axioms. Does that imply that axioms in a formal system are not assumed to be true?

THanks.

Solution 1:

For a formal system to be of much interest, it needs to be consistent -- it needs to have at least one model. In that model, the axioms of the system will be true. It doesn't make much sense to talk about the truth of axioms apart from models.

The formal systems of the most interest -- such as Peano arithmetic and Zermelo-Fraenkel set theory - come with particular "intended" models in which the axioms are true. Indeed, a common way of coming up with axioms is to begin with a model and then try to isolate some of its properties as axioms.

Solution 2:

I agree with Carl's answer: a formal system is the "syntactic specification" of a mathematical theory. We are interested in it because we are interested into the theory and its models.

But we can study also formal sysems per se; see for example : Formal grammar.

Thus, I will suggest some further hints,following the answer to this previous post.

According to :

Richard Kaye, The Mathematics of Logic, (Cambridge U.P., 2007), page 24 :

Formal systems are kinds of mathematical games with strings of symbols and precise rules. They mimic the idea of a ‘proof’. [... Consider the system] based on finite sequences, or strings, of $0$s and $1$s. The set of all such strings is denoted $2^*$ or $2^{<ω}$ [...]. We shall write the empty string of length zero as $\bot$.

Now consider a game starting from a subset $Σ \subseteq 2^*$ with the following rules specifying when a string may be written down.

(Given Strings Rule) You may write down any string $σ \in Σ$.

(Lengthening Rule) Once a string σ has been written down, you may also write down one or both of the strings $σ0$ or $σ1$.

(Shortening Rule) For any string $σ$, once you have written down both $σ0$ and $σ1$ then you may write down $σ$.

Definition 3.1 Let $Σ ⊆ 2^*$ and $τ \in 2^*$. We write $Σ \vdash τ$ to mean that it is possible to write down $τ$ in a finite number of steps that follow the rules of the game for $Σ$.

If $Σ \vdash τ$, then there is a list of strings that can be written down in the game, each of which is written down according to one of the three rules, the last one in the list being $τ$. Sometimes this list of strings is called a formal proof or formal derivation of $τ$ from strings in $Σ$ following the rules given.

Thus $Σ \vdash τ$ can be expressed as saying ‘there is a formal proof of $τ$ from strings in $Σ$’.

Until we do not define an interpretation to the system [see page 30 for a definition of semantics for the above system] it makes little sense to say that :