Take the 2-minute tour ×

From WIkipedia


According to the same link, a formal system consists of a finite alphabet, a formal grammar, a set of axioms and a set of inference rules.

  • I wonder if there are formal systems that are not logical systems?

  • Does the semantics in a logical system always assign truth values to sentences of its formal language?


share|improve this question
Sure, many sets of rewrite rules. But it is best not to worry about Wikipedia's attempts to define a term that is rarely used. –  André Nicolas Jul 15 '14 at 22:14
Does a set of rewrite rules have a set of axioms and a set of inference rules, as well as a formal language and a formal grammar? –  Tim Jul 15 '14 at 22:17
Would such a formal system be illogical? –  Squirtle Jul 15 '14 at 22:19
@Squirtle I don't know the definition of an illogical formal system. From the link "A logic system is sound if all sentences that can be derived are true in the interpretation, and complete if, conversely, all true sentences can be derived." –  Tim Jul 15 '14 at 22:21
@Tim: Of course I did not look up Wikipedia's notion of formal system. One does not go to dictionaries to find out about one's field. –  André Nicolas Jul 15 '14 at 22:29

2 Answers 2

The important fact to be aware of here is that "formal system" and "logical system" are not really technical terms.

Many a textbook in the area of mathematical logic or formal systems will contain something that looks in broad terms more or less like

Definition. By a formal system we mean a set $A$ of "judgments" together with a set of "inference rules" which are such-and-such things ...

However, textbook authors will usually not make any particular effort to make sure their definition matches (or is even equivalent to) the definition of "formal system" in the next textbook over. This is because the purpose of the definition is not to define a crisp class of mathematical objects for which properties can be proved in generality. It's there simply to suggest to the reader a way to think about the similarities and differences between the few concrete formal systems that it is the real goal of the textbook to present.

The definition is phrased in mathematical language because readers of formal logic textbooks are assumed to be "mathematically mature" enough that such a description will be easier for someone to grasp intuitively than a purely verbal prose discussion of what the similar features between different systems are.

However, people don't in general go around proving things like

Theorem. Let $\mathscr F$ be a formal system. Then such-and-such holds.


Theorem. Assume such-and-such. Then there exists a formal system $\mathscr F$ such that this-and-that.

In actual usage, "formal system" is mostly an informal concept of the I-know-one-when-I-see-one variety. The textbook attempts to define the term are usually rather broader than the class of things workers in the field are actually interested in, but that doesn't really bother anyone.

(Of course some people do prove theorems like the above ones, especially if they're writing about computer implementations of symbolic deduction systems. However, in that case they will be using a carefully constructed definition for "formal system" that's tailored to match the capabilities of the system they're talking about. Their notion may be broader or narrower than the informal notion of formal systems that is used outside their special context, such as in general logic textbooks).

All of the above about "formal system" hold true for "logical system" too.

Due to the nature and procedures of Wikipedia, it tends to latch on to the "definitions" in textbooks and present them as if they were more universal facts than they actually are (it is difficult for editors who know that the reality is more fluid than that to get text removed which can after all be sourced to respectable published textbooks!)

Internal consistency between different Wikipedia articles about such fluid terms-that-look-techincal-at-first-glance-but-really-aren't is more than anyone has a right to expect.

share|improve this answer

Yes there exist formal systems which are not logical systems according to that definition. Here's one:

The alphabet consists of the symbol "C" and all lower case letters of the Latin alphabet.

The grammar is

  1. All lower case letters of the Latin alphabet are well-formed formulas.
  2. If $\alpha$ and $\beta$ are well-formed formulas, then so is C$\alpha$$\beta$.
  3. Nothing else is a formula (in this language).

The only axiom is "CCabCCbcCac".

The only rule of inference is condensed detachment.

Now, for this formal system some theorems are CCCCabCcbdCCcad, CCaCbcCCdbCaCdc, and CCabCCCacdCCbcd. However, CCpqCCqrCpr is not a theorem of this system. It's not a logical system, because there is no intended semantics here.

share|improve this answer

Your Answer


