Editing Axiom (section)

==Mathematical logic==
In the field of [[mathematical logic]], a clear distinction is made between two notions of axioms: ''logical'' and ''non-logical'' (somewhat similar to the ancient distinction between "axioms" and "postulates" respectively).

===Logical axioms===
These are certain [[Formula (mathematical logic)|formulas]] in a [[formal language]] that are [[tautology (logic)|universally valid]], that is, formulas that are [[satisfiability|satisfied]] by every [[Assignment (mathematical logic)|assignment]] of values.  Usually one takes as logical axioms ''at least'' some minimal set of tautologies that is sufficient for proving all [[tautology (logic)|tautologies]] in the language; in the case of [[predicate logic]] more logical axioms than that are required, in order to prove [[logical truth]]s that are not tautologies in the strict sense.

====Examples====

=====Propositional logic=====
In [[propositional logic]], it is common to take as logical axioms all formulae of the following forms, where <math>\phi</math>, <math>\chi</math>, and <math>\psi</math> can be any formulae of the language and where the included [[Logical connective|primitive connectives]] are only "<math>\neg</math>" for [[negation]] of the immediately following proposition and "<math>\to</math>" for [[Entailment|implication]] from antecedent to consequent propositions:

# <math>\phi \to (\psi \to \phi)</math>
# <math>(\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi))</math>
# <math>(\lnot \phi \to \lnot \psi) \to (\psi \to \phi).</math>

Each of these patterns is an ''[[axiom schema]]'', a rule for generating an infinite number of axioms.  For example, if <math>A</math>, <math>B</math>, and <math>C</math> are [[propositional variable]]s, then <math>A \to (B \to A)</math> and <math>(A \to \lnot B) \to (C \to (A \to \lnot B))</math> are both instances of axiom schema 1, and hence are axioms.  It can be shown that with only these three axiom schemata and ''[[modus ponens]]'', one can prove all tautologies of the propositional calculus.  It can also be shown that no pair of these schemata is sufficient for proving all tautologies with ''modus ponens''.

Other axiom schemata involving the same or different sets of primitive connectives can be alternatively constructed.<ref>Mendelson, "6. Other Axiomatizations" of Ch. 1</ref>

These axiom schemata are also used in the [[predicate calculus]], but additional logical axioms are needed to include a quantifier in the calculus.<ref>Mendelson, "3. First-Order Theories" of Ch. 2</ref>

=====First-order logic=====
<div style="border: 1px solid #CCCCCC; padding-left: 5px; ">
'''Axiom of Equality.'''<br>Let <math>\mathfrak{L}</math> be a [[first-order language]]. For each variable <math>x</math>, the below formula is universally valid.

<div class="center">
<math>x = x</math>
</div>
</div>

This means that, for any [[Free variables and bound variables|variable symbol]] <math>x</math>, the formula <math>x = x</math> can be regarded as an axiom. Additionally, in this example, for this not to fall into vagueness and a never-ending series of "primitive notions", either a precise notion of what we mean by <math>x = x</math> (or, for that matter, "to be equal") has to be well established first, or a purely formal and syntactical usage of the symbol <math>=</math>  has to be enforced, only regarding it as a string and only a string of symbols, and mathematical logic does indeed do that.

Another, more interesting example [[axiom scheme]], is that which provides us with what is known as '''Universal Instantiation''':

<div style="border: 1px solid #CCCCCC; padding-left: 5px; ">
'''Axiom scheme for Universal Instantiation.'''<br>Given a formula <math>\phi</math> in a first-order language <math>\mathfrak{L}</math>, a variable <math>x</math> and a [[First order logic#Terms|term]] <math>t</math> that is [[First-order logic#Rules of inference|substitutable]] for <math>x</math> in <math>\phi</math>, the below formula is universally valid.

<div class="center">
<math>\forall x \, \phi \to \phi^x_t</math>
</div>
</div>

Where the symbol <math>\phi^x_t</math> stands for the formula <math>\phi</math> with the term <math>t</math> substituted for <math>x</math>. (See [[Substitution of variables]].) In informal terms, this example allows us to state that, if we know that a certain property <math>P</math> holds for every <math>x</math> and that <math>t</math> stands for a particular object in our structure, then we should be able to claim <math>P(t)</math>. Again, ''we are claiming that the formula'' <math>\forall x \phi \to \phi^x_t</math> ''is valid'', that is, we must be able to give a "proof" of this fact, or more properly speaking, a ''metaproof''.  These examples are ''metatheorems'' of our theory of mathematical logic since we are dealing with the very concept of ''proof'' itself. Aside from this, we can also have '''Existential Generalization''':

<div style="border: 1px solid #CCCCCC; padding-left: 5px; ">
'''Axiom scheme for Existential Generalization.''' Given a formula <math>\phi</math> in a first-order language <math>\mathfrak{L}</math>, a variable <math>x</math> and a term <math>t</math> that is substitutable for <math>x</math> in <math>\phi</math>, the below formula is universally valid.

<div class="center">
<math>\phi^x_t \to \exists x \, \phi</math>
</div>
</div>

===Non-logical axioms===
'''Non-logical axioms''' are formulas that play the role of theory-specific assumptions. Reasoning about two different structures, for example, the [[natural number]]s and the [[integer]]s, may involve the same logical axioms; the non-logical axioms aim to capture what is special about a particular structure (or set of structures, such as [[group (algebra)|groups]]). Thus non-logical axioms, unlike logical axioms, are not ''[[Tautology (logic)|tautologies]]''. Another name for a non-logical axiom is ''postulate''.<ref name="properaxioms">Mendelson, "3. First-Order Theories: Proper Axioms" of Ch. 2</ref>

Almost every modern [[mathematical theory]] starts from a given set of non-logical axioms, and it was thought that, in principle, every theory could be axiomatized in this way and formalized down to the bare language of logical formulas.{{Citation needed|date=July 2011}}{{Explain|date=June 2019|reason=use of past tense without explanation of change}}<!-- This turned out to be impossible{{Citation needed|date=March 2010}} and proved to be quite a story (''[[#role|see below]]''); however recently this approach has been resurrected in the form of [[neo-logicism]].-->

Non-logical axioms are often simply referred to as ''axioms'' in mathematical [[discourse]]. This does not mean that it is claimed that they are true in some absolute sense. For instance, in some groups, the group operation is [[commutative]], and this can be asserted with the introduction of an additional axiom, but without this axiom, we can do quite well developing (the more general) group theory, and we can even take its negation as an axiom for the study of non-commutative groups.

====Examples====
This section gives examples of mathematical theories that are developed entirely from a set of non-logical axioms (axioms, henceforth). A rigorous treatment of any of these topics begins with a specification of these axioms.

Basic theories, such as [[arithmetic]], [[real analysis]] and [[complex analysis]] are often introduced non-axiomatically, but implicitly or explicitly there is generally an assumption that the axioms being used are the axioms of [[Zermelo–Fraenkel set theory]] with choice, abbreviated ZFC, or some very similar system of [[axiomatic set theory]] like [[Von Neumann–Bernays–Gödel set theory]], a [[conservative extension]] of ZFC. Sometimes slightly stronger theories such as [[Morse–Kelley set theory]] or set theory with a [[strongly inaccessible cardinal]] allowing the use of a [[Grothendieck universe]] is used, but in fact, most mathematicians can actually prove all they need in systems weaker than ZFC, such as [[second-order arithmetic]].{{citation needed|reason=This claim should include a citation |date=April 2016}}

The study of topology in mathematics extends all over through [[point set topology]], [[algebraic topology]], [[differential topology]], and all the related paraphernalia, such as [[homology theory]], [[homotopy theory]]. The development of ''abstract algebra'' brought with itself [[group theory]], [[ring (mathematics)|rings]], [[field (mathematics)|fields]], and [[Galois theory]].

This list could be expanded to include most fields of mathematics, including [[measure theory]], [[ergodic theory]], [[probability]], [[representation theory]], and [[differential geometry]].

=====Arithmetic=====
The [[Peano axioms]] are the most widely used ''axiomatization'' of [[first-order arithmetic]]. They are a set of axioms strong enough to prove many important facts about [[number theory]] and they allowed Gödel to establish his famous [[Gödel's second incompleteness theorem|second incompleteness theorem]].<ref>Mendelson, "5. The Fixed Point Theorem. Gödel's Incompleteness Theorem" of Ch. 2</ref>

We have a language <math>\mathfrak{L}_{NT} = \{0, S\}</math> where <math>0</math> is a constant symbol and <math>S</math> is a [[unary function]] and the following axioms:

# <math>\forall x. \lnot (Sx = 0) </math>
# <math>\forall x. \forall y. (Sx = Sy \to x = y) </math>
# <math>(\phi(0) \land \forall x.\,(\phi(x) \to \phi(Sx))) \to \forall x.\phi(x)</math> for any <math>\mathfrak{L}_{NT}</math> formula <math>\phi</math> with one free variable.

The standard structure is <math>\mathfrak{N} = \langle\N, 0, S\rangle</math> where <math>\N</math> is the set of natural numbers, <math>S</math> is the [[successor function]] and <math>0</math> is naturally interpreted as the number 0.

=====Euclidean geometry=====
Probably the oldest, and most famous, list of axioms are the 4 + 1 [[Euclid's postulates]] of [[Euclidean geometry|plane geometry]]. The axioms are referred to as "4 + 1" because for nearly two millennia the [[parallel postulate|fifth (parallel) postulate]] ("through a point outside a line there is exactly one parallel") was suspected of being derivable from the first four. Ultimately, the fifth postulate was found to be independent of the first four. One can assume that exactly one parallel through a point outside a line exists, or that infinitely many exist. This choice gives us two alternative forms of geometry in which the interior [[angle]]s of a [[triangle]] add up to exactly 180 degrees or less, respectively, and are known as Euclidean and [[hyperbolic geometry|hyperbolic]] geometries. If one also removes the second postulate ("a line can be extended indefinitely") then [[elliptic geometry]] arises, where there is no parallel through a point outside a line, and in which the interior angles of a triangle add up to more than 180 degrees.

=====Real analysis=====
The objectives of the study are within the domain of [[real numbers]]. The real numbers are uniquely picked out (up to [[isomorphism]]) by the properties of a ''Dedekind complete ordered field'', meaning that any nonempty set of real numbers with an upper bound has a least upper bound. However, expressing these properties as axioms requires the use of [[second-order logic]]. The [[Löwenheim–Skolem theorem]]s tell us that if we restrict ourselves to [[first-order logic]], any axiom system for the reals admits other models, including both models that are smaller than the reals and models that are larger. Some of the latter are studied in [[non-standard analysis]].

===<span id="role">Role in mathematical logic</span>===

====Deductive systems and completeness====
A '''[[deductive system]]''' consists of a set <math>\Lambda</math> of logical axioms, a set <math>\Sigma</math> of non-logical axioms, and a set <math>\{(\Gamma, \phi)\}</math> of ''rules of inference''.  A desirable property of a deductive system is that it be '''complete'''.  A system is said to be complete if, for all formulas <math>\phi</math>,
<div class="center">
<math>\text{if }\Sigma \models \phi\text{ then }\Sigma \vdash \phi</math>
</div>

that is, for any statement that is a ''logical consequence'' of <math>\Sigma</math> there actually exists a ''deduction'' of the statement from <math>\Sigma</math>.  This is sometimes expressed as "everything that is true is provable", but it must be understood that "true" here means "made true by the set of axioms", and not, for example, "true in the intended interpretation". [[Gödel's completeness theorem]] establishes the completeness of a certain commonly used type of deductive system.

Note that "completeness" has a different meaning here than it does in the context of [[Gödel's first incompleteness theorem]], which states that no ''recursive'', ''consistent'' set of non-logical axioms <math>\Sigma</math> of the Theory of Arithmetic is ''complete'', in the sense that there will always exist an arithmetic statement <math>\phi</math> such that neither <math>\phi</math> nor <math>\lnot\phi</math> can be proved from the given set of axioms.

There is thus, on the one hand, the notion of ''completeness of a deductive system'' and on the other hand that of ''completeness of a set of non-logical axioms''.  The completeness theorem and the incompleteness theorem, despite their names, do not contradict one another.

===Further discussion===
Early [[mathematician]]s regarded [[Foundations of geometry|axiomatic geometry]] as a model of [[physical space]], implying, there could ultimately only be one such model. The idea that alternative mathematical systems might exist was very troubling to mathematicians of the 19th century and the developers of systems such as [[Boolean algebra (logic)|Boolean algebra]] made elaborate efforts to derive them from traditional arithmetic. [[Évariste Galois|Galois]] showed just before his untimely death that these efforts were largely wasted. Ultimately, the abstract parallels between algebraic systems were seen to be more important than the details, and [[abstract algebra|modern algebra]] was born.  In the modern view, axioms may be any set of formulas, as long as they are not known to be inconsistent.