Namespaces
Variants
Actions

Difference between revisions of "Equality axioms"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
(3 intermediate revisions by 2 users not shown)
Line 1: Line 1:
Axioms regularizing the use of the equality relation in mathematical proofs. These axioms assert the reflexivity of the equality relation and the possibility of substituting equals for equals. Symbolically the equality axioms are written:
+
<!--
 +
e0359101.png
 +
$#A+1 = 24 n = 0
 +
$#C+1 = 24 : ~/encyclopedia/old_files/data/E035/E.0305910 Equality axioms
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359101.png" /></td> </tr></table>
+
{{TEX|auto}}
 +
{{TEX|done}}
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359102.png" /></td> </tr></table>
+
[[Axiom|Axioms]] regularizing the use of the equality relation in mathematical proofs. These axioms assert the [[reflexivity]] of the equality relation and the possibility of substituting equals for equals. Symbolically the equality axioms are written:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359103.png" /></td> </tr></table>
+
$$
 +
= x ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359104.png" /> is a formula and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359105.png" /> is a term in the language in question, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359106.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359107.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359108.png" /> are variables having the same non-empty domain of variation, and expressions of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e0359109.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591010.png" /> denote the result of replacing all free occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591011.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591012.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591013.png" /> by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591014.png" />.
+
$$
 +
x = y \wedge \phi ( y | v)  \Rightarrow  \phi ( x | v),
 +
$$
  
Using equality axioms, the symmetry and transitivity of the equality relation can be proved. To do this take <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591015.png" /> to be the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591016.png" /> in the first case and the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591017.png" /> in the second.
+
$$
 +
x = y  \Rightarrow  t ( y | v) = t ( x | v),
 +
$$
  
If the formulas and terms of the language in question are constructed from atomic formulas and terms using logical connectives and superposition, then the reduced equality axioms can be derived from their particular cases when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591018.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591019.png" /> are atomic formulas and terms. Symbolically:
+
where  $  \phi $
 +
is a formula and $  t $
 +
is a [[term]] in the language in question,  $  x $,
 +
$  y $
 +
and  $  v $
 +
are variables having the same non-empty domain of variation, and expressions of the form  $  \phi ( x \mid  v) $
 +
and $  t ( x \mid  v) $
 +
denote the result of replacing all free occurrences of  $  v $
 +
in  $  \phi $
 +
or  $  t $
 +
by  $  x $.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591020.png" /></td> </tr></table>
+
Using equality axioms, the symmetry and transitivity of the equality relation can be proved. To do this take  $  \phi $
 +
to be the formula  $  y = v $
 +
in the first case and the formula  $  v = z $
 +
in the second.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591021.png" /></td> </tr></table>
+
If the formulas and terms of the language in question are constructed from atomic formulas and terms using logical connectives and superposition, then the reduced equality axioms can be derived from their particular cases when  $  \phi $
 +
and  $  t $
 +
are atomic formulas and terms. Symbolically:
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591022.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591023.png" /> are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e035/e035910/e03591024.png" />-place predicate and function symbols.
+
$$
 +
x _ {i} = y _ {i} \wedge
 +
P ( x _ {1} \dots x _ {i} \dots x _ {n} )  \Rightarrow \
 +
P ( x _ {1} \dots y _ {i} \dots x _ {n} ),
 +
$$
  
 +
$$
 +
x _ {i} = y _ {i}  \Rightarrow  f ( x _ {1} \dots x _ {i} \dots x _ {n} ) = f ( x _ {1} \dots y _ {i} \dots x _ {n} ),
 +
$$
  
 +
where  $  P $
 +
and  $  f $
 +
are  $  n $-
 +
place predicate and function symbols.
  
 
====Comments====
 
====Comments====
 
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1950)  pp. Chapt. XIV</TD></TR></table>
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1950)  pp. Chapt. XIV</TD></TR></table>

Latest revision as of 19:37, 5 June 2020


Axioms regularizing the use of the equality relation in mathematical proofs. These axioms assert the reflexivity of the equality relation and the possibility of substituting equals for equals. Symbolically the equality axioms are written:

$$ x = x , $$

$$ x = y \wedge \phi ( y | v) \Rightarrow \phi ( x | v), $$

$$ x = y \Rightarrow t ( y | v) = t ( x | v), $$

where $ \phi $ is a formula and $ t $ is a term in the language in question, $ x $, $ y $ and $ v $ are variables having the same non-empty domain of variation, and expressions of the form $ \phi ( x \mid v) $ and $ t ( x \mid v) $ denote the result of replacing all free occurrences of $ v $ in $ \phi $ or $ t $ by $ x $.

Using equality axioms, the symmetry and transitivity of the equality relation can be proved. To do this take $ \phi $ to be the formula $ y = v $ in the first case and the formula $ v = z $ in the second.

If the formulas and terms of the language in question are constructed from atomic formulas and terms using logical connectives and superposition, then the reduced equality axioms can be derived from their particular cases when $ \phi $ and $ t $ are atomic formulas and terms. Symbolically:

$$ x _ {i} = y _ {i} \wedge P ( x _ {1} \dots x _ {i} \dots x _ {n} ) \Rightarrow \ P ( x _ {1} \dots y _ {i} \dots x _ {n} ), $$

$$ x _ {i} = y _ {i} \Rightarrow f ( x _ {1} \dots x _ {i} \dots x _ {n} ) = f ( x _ {1} \dots y _ {i} \dots x _ {n} ), $$

where $ P $ and $ f $ are $ n $- place predicate and function symbols.

Comments

References

[a1] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1950) pp. Chapt. XIV
How to Cite This Entry:
Equality axioms. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Equality_axioms&oldid=18268
This article was adapted from an original article by V.N. Grishin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article