# List of theorems

List of theorems in peano_new/arithmetic/rationals/equality_min.gh:

df-al # <context> # This theorem is part of a series of proofs related to the # <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. This is the second part # in that process. The first part constructed the rationals from an ordered pair of integers. # However, it allows for the existence of NaN (not-a-number) which breaks several of the basic rules. # Now a new version of addition, multiplication, and equality are introduced which merges the number 0 # and the symbol NaN together, but the merging is done so that this number retains all the properties # of 0 and none of the properties of NaN. # </context> Briefly Add Back Predicate Calculus # <summary> # To be able to bind q.nat and nat we cannot import predicate because that would reintroduce nat. # So we have to prove everything in predicate_min from q. Here we redefine q.A. as A. # </summary>
(<-> (A. x ph) (q.A. x ph))
alnfi # <summary> Reproved for integers directly from the natural number versioq. </title>
(-> ph (A. x ph))
gen # <title> Generalization Axiom </title> # <table> # [ ph ] # (A. x [ ph ] ) # </table> # <summary> Reproved for integers directly from the natural number versioq. </title>
ph(A. x ph)
ax-4 roughly Margaris A5, but without the subst # <title> Axiom 4: Specialization </title> # <suggest> right('Remove', '∀') </suggest>
(-> (A. x ph) ph)
BiReplaceImp1Imp0 # <title> Substitution </title> # <table> # (-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (-> [ [ [ ch ] th)) # </table>
(-> ph (-> ps th)) , (<-> ps ch)(-> ph (-> ch th))
BiReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
ax-alim # <title> Axiom 5: Quantified Implication </title>
(-> (A. x (-> ph ps)) (-> (A. x ph) (A. x ps)))
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
ax-6 # <title> Axiom 6: Quantified Negation </title>
(-> (-. (A. x ph)) (A. x (-. (A. x ph))))
ax-7 # <title> Axiom 7: Quantifier Commutation </title>
(-> (A. x (A. y ph)) (A. y (A. x ph)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
qexex # <title> Natural and Integer Existence are the same </title>
(<-> (q.E. x ph) (E. x ph))
df-r # <title> Definition of Remove NaN </title> # <summary> # This maps NaN to 0 and leaves everything else unchanged. # </summary> # <suggest> left('Simplify', '/') right('Define', '/') </suggest>
(q.= (r A) (q.ifn (q.= A (q.NaN)) (q.0) A))
(-> (q.= A B) (q.= (r A) (r B)))
(q.= A B)(q.= (r A) (r B))
(-> ph (q.= A B))(-> ph (q.= (r A) (r B)))
(-> (q.= A (q.NaN)) (q.= (r A) (q.0)))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
(-> (-. (q.= A (q.NaN))) (q.= (r A) A))
(-. (q.= (r A) (q.NaN)))
(q.= (r (q.0)) (q.0))
(q.= (r (q.1)) (q.1))
(<-> (= A B) (q.= (r A) (r B)))
eqid # <title> Reflexive Property </title>
(= A A)
eqcom # <title> Symmetric Property </title>
(<-> (= A B) (= B A))
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
(-> (/\ (= A B) (= B C)) (= A C))
(E. x (= x A))
(-> (q.= A B) (= A B))
eqeqqi # <title> Convert Natural to Rational Equality </title>
(q.= A B)(= A B)
eqeqqd # <title> Convert Natural to Rational Equality </title>
(-> ph (q.= A B))(-> ph (= A B))
(q.= (r (r A)) (r A))