Wolfram Cloud Document

In[]:=

SetDirectory[NotebookDirectory[]]

Out[]=

/Users/sw/Dropbox/Physics/WorkingMaterial/2022

In[]:=

metamathGraph=CloudGet["https://wolfr.am/PLbmdhRv"];

In[]:=

metamathAssoc=CloudGet["https://wolfr.am/PLborw8R"];

In[]:=

metamathDomains=Union[Values[metamathAssoc]];

In[]:=

metamathInfrastructure={"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","GUIDES AND MISCELLANEA"};

(*setmm=ResourceFunction["MetamathImport"][URL["https://raw.githubusercontent.com/metamath/set.mm/master/set.mm"]];*)

(*"DATA/setmm-basic.wxf"*)

In[]:=

setmm=Import["DATA/setmm-basic.wxf"];

In[]:=

defassoc=KeySelect[setmm["Statements"],StringStartsQ["df-"]];

In[]:=

axiomassoc=KeySelect[setmm["Statements"],StringStartsQ["ax-"]];

In[]:=

RulesFromDefs[("Axiom"|"EssentialHypothesis")[_,x_List,___]]:=With[{xx=DeleteCases[DeleteCases[x,Alternatives@@mmvars],"("|")"|""|"{"|"}"]},Thread[xx[[2]]->Drop[xx,2]]]

In[]:=

mmvars=Keys[Select[setmm["Symbols"],Head[#]==="Variable"&]];

In[]:=

mmconsts=Keys[Select[setmm["Symbols"],Head[#]==="Constant"&]];

In[]:=

famous=Select[{{"The Irrationality of the Square Root of 2","sqrt2irr"},{"The Fundamental Theorem of Algebra","fta"},{"The Denumerability of the Rational Numbers","qnnen"},{"Pythagorean Theorem","pythag"},{"The Prime Number Theorem","pnt"},{"Law of Quadratic Reciprocity","lgsquad"},{"The Area of a Circle","areacirc"},{"Euler's Generalization of Fermat's Little Theorem","eulerth"},{"The Infinitude of Primes","infpn2"},{"Euler's Summation of 1 +","1/2)^2 + (1/3)^2 + .... (basel"},{"The Fundamental Theorem of Integral Calculus","ftc1 and ftc2"},{"De Moivre's Theorem","demoivreALT"},{"Liouville's Theorem and the Construction of Transcendental Numbers","aaliou"},{"Four Squares Theorem","4sq"},{"All Primes","1 mod 4) Equal the Sum of Two Squares (2sq"},{"The Non-Denumerability of the Continuum","ruc"},{"Formula for Pythagorean Triples","pythagtrip"},{"Schroeder-Bernstein Theorem","sbth"},{"Leibniz' Series for Pi","leibpi"},{"Sum of the Angles of a Triangle","ang180"},{"The Ballot Problem","aka Bertrand's ballot problem) (ballotth"},{"Ramsey's Theorem","ramsey"},{"Divergence of the Harmonic Series","harmonic"},{"Taylor's Theorem","taylth"},{"The Solution of a Cubic","cubic"},{"Arithmetic Mean/Geometric Mean","amgm"},{"Solutions to Pell's Equation","rmxycomplete"},{"Sum of the Reciprocals of the Triangular Numbers","trirecip"},{"The Binomial Theorem","binom"},{"The Partition Theorem","by Euler) (eulerpart"},{"The Solution of the General Quartic Equation","quart"},{"Dirichlet's Theorem","dirith"},{"The Cayley-Hamilton Theorem","cayleyhamilton"},{"Wilson's Theorem","wilth"},{"The Number of Subsets of a Set","pw2en"},{"The Konigsberg Bridge Problem","konigsberg"},{"Product of Segments of Chords","chordthm by David Moews"},{"Heron's Formula","heron by Mario Carneiro based on work by Jon Pennant and Thierry Arnoux"},{"Formula for the Number of Combinations","hashbc"},{"Bezout's Theorem","bezout"},{"Theorem of Ceva","cevath"},{"Cantor's Theorem","canth2"},{"L'Hôpital's Rule","lhop"},{"Isosceles Triangle Theorem","isosctr"},{"Sum of a Geometric Series","geoser"},{"e is Transcendental","etransc"},{"Sum of an arithmetic series","arisum"},{"Greatest Common Divisor Algorithm","eucalg"},{"The Perfect Number Theorem","perfect"},{"Order of a Subgroup","lagsubg"},{"Sylow's Theorem","sylow1 and sylow2 and sylow2b and sylow3"},{"Ascending or Descending Sequences","erdsze and erdsze2"},{"The Mean Value Theorem","mvth"},{"Fourier Series","fourier"},{"Sum of kth powers","fsumkthpow"},{"The Cauchy-Schwarz Inequality","sii"},{"The Intermediate Value Theorem","ivth"},{"Fundamental Theorem of Arithmetic","1arith2"},{"Erdős's proof of the divergence of the inverse prime series","prmrec"},{"The Friendship Theorem","friendship"},{"Divisibility by 3 Rule","3dvds"},{"Lebesgue Measure and Integration","itgcl"},{"Desargues's Theorem","dath"},{"Derangements Formula","derangfmla and subfaclim"},{"The Factor and Remainder Theorems","facth and plyrem"},{"Stirling's Formula","stirling by Glauco Siliprandi"},{"The Triangle Inequality","abstrii"},{"The Birthday Problem","birthday"},{"The Law of Cosines","lawcos"},{"Ptolemy's Theorem","ptolemy"},{"Principle of Inclusion/Exclusion","incexc"},{"Cramer's Rule","cramer"},{"Bertrand's Postulate","bpos"}},Length[VertexOutComponent[metamathGraph,Last[#]]]>2&];//Quiet

In[]:=

Length[%]

Out[]=

Derived below:

In[]:=

usedaxioms={"ax-mp","ax-1","ax-2","ax-3","ax-gen","ax-4","ax-5","ax-6","ax-7","ax-8","ax-9","ax-10","ax-11","ax-12","ax-13","ax-ext","ax-rep","ax-sep","ax-nul","ax-pow","ax-pr","ax-un","ax-inf2","ax-cc","ax-cnex","ax-resscn","ax-1cn","ax-icn","ax-addcl","ax-addrcl","ax-mulcl","ax-mulrcl","ax-mulcom","ax-addass","ax-mulass","ax-distr","ax-i2m1","ax-1ne0","ax-1rid","ax-rnegex","ax-rrecex","ax-cnre","ax-pre-lttri","ax-pre-lttrn","ax-pre-ltadd","ax-pre-mulgt0","ax-pre-sup","ax-addf","ax-mulf"};

In[]:=

axiomnames=Association[#1->First[#2]&@@@{"ax-mp"{"modus ponens"},"ax-1"{"axiom of simplification"},"ax-2"{"Frege's axiom"},"ax-3"{"principle of transposition"},"ax-gen"{"rule of generalization"},"ax-4"{"axiom of quantified implication"},"ax-5"{"Axiom of Distinctness"},"ax-6"{"Axiom of Existence"},"ax-7"{"Axiom of Equality"},"ax-8"{"Axiom of Left Equality for Binary Predicate"},"ax-9"{"Axiom of Right Equality for Binary Predicate"},"ax-10"{"Axiom of Quantified Negation"},"ax-11"{"Axiom of Quantifier Commutation"},"ax-12"{"Axiom of Substitution"},"ax-13"{"Axiom of Quantified Equality"},"ax-ext"{"Axiom of Extensionality"},"ax-rep"{"Axiom of Replacement"},"ax-sep"{"Axiom of Separation"},"ax-nul"{"The Null Set Axiom"},"ax-pow"{"Axiom of Power Sets"},"ax-pr"{"Axiom of Pairing"},"ax-un"{"Axiom of Union"},"ax-inf2"{"Axiom of Infinity"},"ax-cc"{"Axiom of Countable choice"},"ax-cnex"{"Complex numbers form a set"},"ax-resscn"{"Real numbers are subset complex"},"ax-1cn"{"1 is a complex number"},"ax-icn"{"i is a complex number"},"ax-addcl"{"Closure for complex addition"},"ax-addrcl"{"Closure for real addition"},"ax-mulcl"{"Closure for complex multiplication"},"ax-mulrcl"{"Closure for real multiplication"},"ax-mulcom"{"Commutativity of complex multiplication"},"ax-addass"{"Associativity of complex addition"},"ax-mulass"{"Associativity of complex multiplication"},"ax-distr"{"Distributivity for complex numbers"},"ax-i2m1"{"i-squared equals -1"},"ax-1ne0"{"1 and 0 are distinct"},"ax-1rid"{"1 is identity for real multiplication"},"ax-rnegex"{"Existence of negative of real number"},"ax-rrecex"{"Existence of reciprocal of nonzero real number"},"ax-cnre"{"Complex numbers can be expressed in terms of two reals"},"ax-pre-lttri"{"Ordering on reals satisfies strict trichotomy"},"ax-pre-lttrn"{"Ordering on reals is transitive"},"ax-pre-ltadd"{"Ordering property of addition on reals"},"ax-pre-mulgt0"{"Product of two positive reals is positive"},"ax-pre-sup"{"Nonempty bounded-above set of reals has supremum"},"ax-addf"{"Addition is an operation on complex numbers"},"ax-mulf"{"Multiplication is an operation on complex numbers"}}];

[ total theorems on which it depends | total “sources” | total distinct axioms | total distinct definitions ]

In[]:=

Text[Grid[Flatten/@({#1,Length[VertexOutComponent[metamathGraph,#2]],{Length[#],Length[Select[#,StringStartsQ["ax-"]]],Length[Select[#,StringStartsQ["df-"]]]}&[With[{g=VertexOutComponentGraph[metamathGraph,#2]},Select[VertexList[g],VertexOutDegree[g,#]==0&]]]}&@@@famous),Frame->All]]

Out[]=

The Irrationality of the Square Root of 2	3723	152	44	108
The Fundamental Theorem of Algebra	7368	286	48	238
The Denumerability of the Rational Numbers	3842	153	45	108
Pythagorean Theorem	7099	279	48	231
The Prime Number Theorem	8292	295	48	247
Law of Quadratic Reciprocity	6292	261	48	213
The Area of a Circle	8279	296	48	248
Euler's Generalization of Fermat's Little Theorem	4340	166	45	121
The Infinitude of Primes	3300	143	45	98
De Moivre's Theorem	5070	180	48	132
Liouville's Theorem and the Construction of Transcendental Numbers	7003	285	48	237
Four Squares Theorem	4576	168	45	123
The Non-Denumerability of the Continuum	3412	146	45	101
Formula for Pythagorean Triples	4202	163	44	119
Schroeder-Bernstein Theorem	1411	70	21	49
Leibniz' Series for Pi	7694	285	48	237
Sum of the Angles of a Triangle	7123	279	48	231
Ramsey's Theorem	4783	174	46	128
Divergence of the Harmonic Series	4747	172	46	126
Taylor's Theorem	7080	296	48	248
The Solution of a Cubic	7320	281	48	233
Arithmetic Mean/Geometric Mean	7576	301	48	253
Solutions to Pell's Equation	7707	292	48	244
Sum of the Reciprocals of the Triangular Numbers	4537	171	46	125
The Binomial Theorem	4421	169	46	123
The Solution of the General Quartic Equation	7292	281	48	233
Dirichlet's Theorem	9814	359	48	311
The Cayley-Hamilton Theorem	6510	278	47	231
Wilson's Theorem	5393	222	48	174
The Number of Subsets of a Set	1669	80	21	59
The Konigsberg Bridge Problem	4504	176	45	131
Formula for the Number of Combinations	3857	154	44	110
Bezout's Theorem	3739	154	44	110
Theorem of Ceva	2580	120	42	78
Cantor's Theorem	1653	76	21	55
L'Hôpital's Rule	6333	265	48	217
Isosceles Triangle Theorem	7137	279	48	231
Sum of a Geometric Series	4360	167	46	121
e is Transcendental	8797	306	49	256
Sum of an arithmetic series	4444	169	46	123
Greatest Common Divisor Algorithm	3848	156	44	112
The Perfect Number Theorem	7401	285	48	237
Order of a Subgroup	4631	187	46	141
The Mean Value Theorem	6273	264	48	216
Fourier Series	8719	294	49	245
Sum of kth powers	4594	170	46	124
The Intermediate Value Theorem	3689	155	44	111
Fundamental Theorem of Arithmetic	4414	167	45	122
Erdős's proof of the divergence of the inverse prime series	5229	179	46	133
The Friendship Theorem	6330	211	46	165
Divisibility by 3 Rule	4457	175	46	129
Lebesgue Measure and Integration	4417	172	46	126
Desargues's Theorem	2636	102	22	80
The Triangle Inequality	3535	150	44	106
The Birthday Problem	7819	284	48	236
The Law of Cosines	7097	279	48	231
Ptolemy's Theorem	6927	277	48	229
Principle of Inclusion/Exclusion	4546	170	46	124
Cramer's Rule	6160	266	47	219
Bertrand's Postulate	7760	287	48	239

[ want to do same from all theorems ]

Pythagorean theorem

How many copies of each axiom are there in the Pythagorean theorem?

[[ Also look at this in Euclid ]]

Distance from all nodes to a particular axiom

Full Metamath set.mm Graph

pythag vs. pythi [[ probably not interesting; different spaces being used ]]

Definitions