Mathematical theories and axioms

[Fredrik]

Maybe this is a dumb question. I'm a bit tired right now.

What is a "theory" in mathematics, and what kind of statements can we call "axioms"?

To be more specific, is "group theory" a mathematical theory, and if yes, what are its axioms? Should I think of the definition of "group" as an axiom of the theory, or as "just a definition"?

 

[HallsofIvy]

I wouldn't say that the definition of a group is an axiom, but rather that each of the properties required in the definition of a group is an axiom.

 

[Somefantastik]

If you would like to know about theory in Math, look at Chapter 2 of Douglas Hofstadter's Godel, Escher, and Bach. It's a down-and-dirty quick explanation that ties it all together globally for you. He talks about theory and axioms and how they fit together, before he launches into his murky tirade about incompleteness/endless loops/canons...

 

[Hurkyl]

There isn't an essential difference between a definition and an axiom. And in practical terms, there isn't any essential difference between axioms and theorems either.

 

[CRGreathouse]

There isn't an essential difference between a definition and an axiom.

In metamath, definitions are just a kind of axiom. To me, though, the two are epistemologically different -- a definition, properly written, is always a conservative extension -- they never add expressive power. Ideally, the given axioms for a system each add expressive power, though proving this is hard in the light of incompleteness.

 

[Hurkyl]

In metamath, definitions are just a kind of axiom. To me, though, the two are epistemologically different -- a definition, properly written, is always a conservative extension -- they never add expressive power. Ideally, the given axioms for a system each add expressive power, though proving this is hard in the light of incompleteness.

I agree that there is pedagogical value in separating the ideas of axiom, definition, theorem, lemma, and so forth. I just worry that, sometimes, people read too much into the distinction.

 

[Fredrik]

Thanks guys. Those answers are good enough for my purposes. (I'm just checking if I use those words the same as others).

 

[Dragonfall]

A "theory" is a set of formulas closed under logical deduction. A theory is "axiomatic" if there exists a finite (or countable) subset that are independent and from which every formula in the theory can be deduced. Think of it as a vector space with a "basis".

 

[Fredrik]

A "theory" is a set of formulas closed under logical deduction. A theory is "axiomatic" if there exists a finite (or countable) subset that are independent and from which every formula in the theory can be deduced. Think of it as a vector space with a "basis".

This is very interesting. It makes me want to learn more.

I have some follow-up questions:

a) Is there also a definition of what a "formula" is in this framework? Is it just a string of text?

b) Is there also a definition of what "logical deduction" is in this framework? Should we think of it as a set of rules that tell us how to construct a new formula from existing ones? (I guess "new" and "existing" are somewhat misleading terms here, since all the formulas of the theory already exist as members of the set). Wouldn't that make "logical deduction" a set of functions that take subsets of the theory (which is itself a set) to members of the theory?

c) Isn't set theory itself supposed to be an axiomatic theory? Then how can you use set-theoretic terms (e.g. subset) in the definitions of "theory" and "axiomatic"?

 

[Hurkyl]

(For the record, I'm not entirely convinced that the technical and informal uses of the word 'theory' are entirely the same)

a) Is there also a definition of what a "formula" is in this framework? Is it just a string of text?

Yes. You first define an alphabet to be a set of 'symbols'. Then, you define a string over that alphabet to be an ordered sequence of symbols. Finally, the 'language' of formulae is a set of strings specified by some grammar.

Is there also a definition of what "logical deduction" is in this framework? Should we think of it as a set of rules that tell us how to construct a new formula from existing ones?

Yes.

Wouldn't that make "logical deduction" a set of functions that take subsets of the theory (which is itself a set) to members of the theory?

Not quite; for any particular rule of deduction, only certain subsets of the language are in the domain of the rule.

Isn't set theory itself supposed to be an axiomatic theory? Then how can you use set-theoretic terms (e.g. subset) in the definitions of "theory" and "axiomatic"?

By being very careful about what you really mean. (And if you really want to talk about the ambient set theory, you invoke a metamathematical axiom that what mathematicians do is a model of formal logic)