3
$\begingroup$

I am just starting to learn about formal systems, and have learnt that the many axiom systems in Mathematics, such as those of plane geometry, Peano's axioms, vector axioms, etc. can each be used to form different formal systems. However, in informal mathematics, we often couple multiple branches together, e.g. like when we use the concepts of plane geometry to prove statements about vectors. This has led me to wonder what the underlying formal system is when we are drawing upon axioms which seem to be usually regarded as different formal systems. I have a few questions regarding this point:

  1. Is it valid to regard the underlying formal system here as a single formal system whose axioms are all of the axioms of the individual axiomatic systems concatenated together, and whose language is all of the symbols of the individual formal systems concatenated together also? (In this approach, the set of deductive rules for each of the individual formal systems would have to be the same, and the "concatenated" formal system would just have this set of deductive rules also).

  2. Is it valid for the formal system we are working in here to have multiple formal systems (and thus multiple theories) "nested inside of it", as in formal system $1$ can talk about formal system $2$, formal system $2$ can talk about formal system $3$, etc.?

  3. What is the canonical way to view what the formal system is when drawing upon multiple axiom systems in mathematics?

  4. Formally, when we do mathematics is this always done in the overarching context of there being a single formal system we are using?

$\endgroup$
6
  • 1
    $\begingroup$ Vast majority of maths is based on ZF set theory. And vast majority of axiomatic systems is coupled with it, and arises from it. Which brings a common background for cross axiomatic work. $\endgroup$
    – freakish
    Commented Jun 21 at 7:21
  • $\begingroup$ @freakish what exactly do you mean by "vast majority of axiomatic systems is coupled with it [ZFC]"? How is this usually done? $\endgroup$
    – Princess Mia
    Commented Jun 21 at 7:26
  • 1
    $\begingroup$ Well, if we look at say Peano arithmetic, then you can consider it as a standalone axiomatic system. But in practice we use a variant starting with "natural numbers is a set together with a special function such that..." which implicitly assumes the notion of sets and functions, i.e. some set theory. And if so, then we can use other tools from set theory to study it. $\endgroup$
    – freakish
    Commented Jun 21 at 8:57
  • $\begingroup$ More formal example is entire model theory. Which studies formal theories on top of sets. So it does assume some set theory under the hood. $\endgroup$
    – freakish
    Commented Jun 21 at 8:59
  • 1
    $\begingroup$ Usually, we formalize a single theory. A usual mathematical treatise is semi-formal: topology needs set theory, the same for calculus. $\endgroup$
    – Mauro ALLEGRANZA
    Commented Jun 21 at 12:58

2 Answers 2

Reset to default
0
$\begingroup$

First, we would do best to define or clarify what a formal system consists of. A formal system has all of the correct forms specified a priori. In informal mathematics, that doesn't get done. For instance, someone might write 2*3 + 4 = 14. Now, it would not be difficult to specify an order of operations (and forbid all other operations) where that works out alright. But, in informal mathematics it's hard to imagine that as anything but false. Or even more simply is 2 + 2 + 2 + 2 = 8 a correct form or 2 + (2 +2) + 2 = 8? What is the calculation order for either of those? Or do people mean something like SUM(2, 2, 2, 2) = 8 and thus calculation order becomes irrelevant?

In informal mathematics, such ambiguities persist and can't get answered there.

In informal mathematics, likely, there isn't a formal system when many different axiom systems come into play. Perhaps there could exist a formal system, but likely the authors didn't use a system which had correct forms specified a priori. That said, perhaps there could exist in the future some formal system where the claims could get rigorously proved. But that doesn't mean that in the past when the authors wrote their work they specifically had a system with all correct forms specified a priori. And thus there was no formal system.

$\endgroup$
5
  • $\begingroup$ Of course, most math does not use an explicit set of axioms. However, it is supposed to be formalizable in a certain foundational system, most often ZFC. $\endgroup$
    – Keplerto
    Commented Jun 23 at 21:17
  • $\begingroup$ @Keplerto ZFC doesn't have a specific set of axioms/rule(s) of inference for classical propositional and classical predicate calculus. So, "formalizable in ZFC" is not precise. Thus again, there does not exist an underlying formal system. $\endgroup$
    – Doug Spoonwood
    Commented Jun 25 at 21:16
  • $\begingroup$ It is true that the study of logical systems may not rely on ZFC. However, I think there's a point that might be relevant to the OP, and it's that we usually don't consider mathematical structures such as groups as formal systems. Because in the language of groups one cannot easily express some simple theorems such as Lagrange's theorem. For that we use the language of sets. There are also successful formalization of many theorems in a single language such as coq. So several branches of math can be combined without problem. Just not via the naive 'concatenate the axioms of each system'. $\endgroup$
    – Keplerto
    Commented Jun 25 at 23:37
  • $\begingroup$ @Keplerto I'm not claiming that formalization is not possible. However, mathematical claims usually don't have an exact formal system in mind. And even when someone claims something is "formalizable" that doesn't mean we have a specific system. As I allued to above, "ZFC" isn't even a precise system, nor "set theory", because the underling logic isn't specified. Even "first-order logic" isn't precise, because we don't have a specified list of axioms and/or rules known just from that phrase, since many different axiom sets work out sufficiently similarly. $\endgroup$
    – Doug Spoonwood
    Commented Jun 25 at 23:49
  • $\begingroup$ Commented Note that my previous comment is not really an answer to the question as it is. I just thought it might shed some light on it. So to be clear I don't think mathematics is always done over a single formal system, I just think that set theory or other foundations is the closest thing to what they are suggesting. For example, to the question of whether a formal system can talk about another, it sounds similar to a theory having a model inside another like ZFC. So even if they had in mind something more literal I still think it's relevant. (Models from another comment.) $\endgroup$
    – Keplerto
    Commented Jun 26 at 0:37
0
$\begingroup$

A formal system behind such mathematical structures would usually be one or another type of logic. The two types usually considered are (1) classical logic (incorporating the law of excluded middle, abbreviated LEM), and (2) intuitionistic logic of which there are several varieties, the common feature being the rejection of LEM. There are other types of logics but I believe they are less frequently used, and at any rate I don't know much about them.

Thus, Peano Arithmetic (PA) would be typically expressed in classical logic. It has an intuitionistic analog called Heyting Arithmetic (HA).

The classical Zermelo-Fraenkel set theory is I believe always expressed in classical logic, and tends to be rejected by constructivists (who use intuitionistic logic).

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .