Editing Axiom (section)

===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>