You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
In[]:=
eucdef=ResourceData[ResourceObject[CloudObject[
https://www.wolframcloud.com/obj/s.wolfram/DeployedResources/Data/
Structure-of-Euclid's-Elements
]]];In[]:=
eucdef[<|"Book"13,"Theorem"18|>]["Text"]
Out[]=
To set out the sides of the five figures and to compare them with one another.
In[]:=
eucdef[<|"Book"13,"Theorem"18|>]["GreekText"]
Out[]=
τὰς πλευρὰς τῶν πέντε σχημάτων ἐκθέσθαι καὶ συγκρῖναι πρὸς ἀλλήλας.
In[]:=
Text[Column[(RightArrow@@(EuclidVertexName/@FindLongestPath[ReverseGraph[euc],#,<|"Book"13,"Theorem"18|>]))&/@axioms,FrameAll]]
Out[]=
CN1→1.1→1.2→1.3→1.5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
CN2→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
CN3→1.2→1.3→1.5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
CN4→1.4→1.5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
CN5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
P1→1.1→1.2→1.3→1.5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
P2→1.2→1.3→1.5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
P3→1.1→1.2→1.3→1.5→1.7→1.8→1.11→1.13→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
P4→1.15→1.16→1.18→1.19→1.20→1.22→1.23→1.31→1.37→1.41→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
P5→1.29→1.34→1.35→1.36→1.38→6.1→6.2→6.11→6.19→6.20→10.9→10.29→10.30→10.33→10.76→10.94→13.11→13.16→13.18 |
In[]:=
Length/@(FindLongestPath[ReverseGraph[euc],#,<|"Book"13,"Theorem"18|>]&/@axioms)
Out[]=
{33,26,32,31,29,33,32,33,25,20}
In[]:=
Position[%,33]
Out[]=
{{1},{6},{8}}
In[]:=
axioms[[{1,6,8}]]
Out[]=
{Common Notion1,Postulate1,Postulate3}
In[]:=
Rule[a,b,c]
Out[]=
Rule[a,b,c]
In[]:=
RightArrow[a,b,c]
Out[]=
a→b→c
In[]:=
ppp=FindLongestPath[ReverseGraph[euc],#,<|"Book"13,"Theorem"18|>]&/@axioms;
In[]:=
SameQ@@Take[ppp,All,-5]
Out[]=
True
In[]:=
Table[SameQ@@Take[ppp,All,-n],{n,20}]
Out[]=
{True,True,True,True,True,True,True,True,True,True,True,True,True,True,False,False,False,False,False,False}
In[]:=
Take[ppp,All,-14]
Out[]=
In[]:=
Take[ppp,All,-15]
Out[]=
In[]:=
Rest[Map[EuclidVertexName[First[#]]&,SplitBy[SortBy[Transpose[{VertexList[euc],tlens}],Last],Last],{2}]]
Out[]=
{{1.1,1.4,3.5,3.6,5.1,5.2,5.7,5.11,5.13,7.1,7.5,7.23,7.28,7.29,7.31,7.35,9.7,9.21,9.24,9.33,9.34,10.1,10.2,10.15,10.16,11.1,11.3},{1.2,5.3,5.5,5.6,5.8,5.12,5.17,6.21,7.2,7.6,7.7,7.32,9.20,9.22,9.25,9.26,9.27,9.28,10.3,11.2,11.7,11.13,11.16},{1.3,5.4,5.9,5.10,5.15,7.3,7.4,7.8,7.9,7.12,9.23,10.4},{1.5,1.6,4.1,5.14,5.20,5.21,7.10,7.11,7.15,9.29,9.30},{1.7,5.16,5.18,5.22,7.13,7.16,7.37,7.38,9.11,9.31},{1.8,5.19,5.23,5.24,7.14,7.17,7.20,9.35,10.5},{1.9,1.11,4.9,5.25,7.18,7.21,7.22,8.13,8.18,10.6,10.8,13.7},{1.10,1.13,4.14,7.19,8.1,8.10,8.11,8.12,8.19,9.16,9.17,10.7,11.19},{1.12,1.14,1.15,3.1,7.24,7.30,7.33,9.18,10.11},{1.16,1.29,3.9,3.10,7.25,7.26,7.34,8.20,9.14,9.19},{1.17,1.18,1.26,1.27,1.30,3.23,7.27,7.36,8.4,8.22},{1.19,1.28,1.33,1.34,3.3,3.24,7.39,8.2,8.5,8.24,10.12,11.4,11.14},{1.20,1.35,1.43,3.2,3.4,3.16,3.18,3.26,8.3,8.9,8.26,8.27,10.13,11.5,11.8,11.28},{1.21,1.22,1.36,3.11,3.12,3.17,3.19,3.28,4.4,4.7,4.13,8.6,8.8,8.21,11.6,11.18,12.16},{1.23,3.13,3.30,8.7,8.23,9.1,9.2,11.9,11.29},{1.24,1.31,3.25,8.14,8.15,8.25,9.3,9.6,9.8,11.10,11.30,11.38},{1.25,1.32,1.37,1.38,1.46,2.1,3.7,3.8,4.8,8.16,8.17,9.4,9.5,9.9,9.10,9.12,11.11,11.22,11.24},{1.39,1.40,1.41,2.2,2.3,2.4,2.5,2.6,2.7,2.8,3.20,4.3,9.13,11.12,11.15,11.20,11.25,13.3},{1.42,1.47,3.21,3.27,6.1,9.15,9.32,9.36,10.17,10.36,10.73,10.74,10.77,11.21,11.26,11.31},{1.44,1.48,2.9,2.10,2.11,2.12,2.13,3.14,3.22,3.29,3.35,3.36,6.2,6.14,6.15,6.33,10.18,10.19,10.20,10.21,10.37,10.106,11.39,13.2},{1.45,3.15,3.31,3.37,4.15,6.3,6.4,6.9,6.10,6.11,6.12,6.16,6.24,10.55,10.115,11.17,11.35,12.3},{2.14,3.32,4.5,4.6,6.5,6.6,6.7,6.8,6.17,6.18,6.19,6.23,6.26,11.27,11.32,11.36,13.8,13.9,13.12,13.14,13.15},{3.33,3.34,4.2,4.10,6.13,6.20,6.22,6.27,6.31,6.32,10.54,10.92,10.95,11.23,11.33,11.34,13.1,13.4,13.5,13.10},{4.11,6.25,10.9,10.14,10.22,10.91,10.109,11.37,12.1,12.4,13.13},{4.12,4.16,6.28,6.29,10.10,10.23,10.25,10.26,10.29,10.38,10.49,10.50,10.51,10.52,10.53,10.60,10.66,10.85,10.86,10.87,10.88,10.89,10.90,10.97,10.101,10.103,10.112,10.113,12.2},{6.30,10.24,10.27,10.28,10.30,10.42,10.43,10.44,10.45,10.56,10.61,10.62,10.67,10.79,10.80,10.83,10.98,10.111,10.114,12.5,13.6},{10.31,10.32,10.33,10.47,10.48,10.75,12.6,12.7,13.17},{10.34,10.35,10.39,10.76,10.81,10.93,10.99,10.104,12.8,12.9,12.10},{10.40,10.41,10.57,10.63,10.68,10.78,10.82,10.94,10.100,10.105,12.11,12.12,12.17},{10.46,10.58,10.59,10.64,10.65,10.69,10.70,10.84,10.96,10.102,10.107,10.108,12.13,12.18,13.11},{10.71,10.72,10.110,12.14,12.15,13.16},{13.18}}
In[]:=
Length/@%77
Out[]=
{27,23,12,11,10,9,12,13,9,10,10,13,16,17,9,12,19,18,16,24,18,21,20,11,29,21,9,11,13,15,6,1}
In[]:=
ListLinePlot[%]
Out[]=
In[]:=
EuclidVertexName[First[#]]&/@%
Out[]=
{CN1,CN2,CN3,CN4,CN5,P1,P2,P3,P4,P5,1.1,1.4,3.5,3.6,5.1,5.2,5.7,5.11,5.13,7.1,7.5,7.23,7.28,7.29,7.31,7.35,9.7,9.21,9.24,9.33,9.34,10.1,10.2,10.15,10.16,11.1,11.3,1.2,5.3,5.5,5.6,5.8,5.12,5.17,6.21,7.2,7.6,7.7,7.32,9.20,9.22,9.25,9.26,9.27,9.28,10.3,11.2,11.7,11.13,11.16,1.3,5.4,5.9,5.10,5.15,7.3,7.4,7.8,7.9,7.12,9.23,10.4,1.5,1.6,4.1,5.14,5.20,5.21,7.10,7.11,7.15,9.29,9.30,1.7,5.16,5.18,5.22,7.13,7.16,7.37,7.38,9.11,9.31,1.8,5.19,5.23,5.24,7.14,7.17,7.20,9.35,10.5,1.9,1.11,4.9,5.25,7.18,7.21,7.22,8.13,8.18,10.6,10.8,13.7,1.10,1.13,4.14,7.19,8.1,8.10,8.11,8.12,8.19,9.16,9.17,10.7,11.19,1.12,1.14,1.15,3.1,7.24,7.30,7.33,9.18,10.11,1.16,1.29,3.9,3.10,7.25,7.26,7.34,8.20,9.14,9.19,1.17,1.18,1.26,1.27,1.30,3.23,7.27,7.36,8.4,8.22,1.19,1.28,1.33,1.34,3.3,3.24,7.39,8.2,8.5,8.24,10.12,11.4,11.14,1.20,1.35,1.43,3.2,3.4,3.16,3.18,3.26,8.3,8.9,8.26,8.27,10.13,11.5,11.8,11.28,1.21,1.22,1.36,3.11,3.12,3.17,3.19,3.28,4.4,4.7,4.13,8.6,8.8,8.21,11.6,11.18,12.16,1.23,3.13,3.30,8.7,8.23,9.1,9.2,11.9,11.29,1.24,1.31,3.25,8.14,8.15,8.25,9.3,9.6,9.8,11.10,11.30,11.38,1.25,1.32,1.37,1.38,1.46,2.1,3.7,3.8,4.8,8.16,8.17,9.4,9.5,9.9,9.10,9.12,11.11,11.22,11.24,1.39,1.40,1.41,2.2,2.3,2.4,2.5,2.6,2.7,2.8,3.20,4.3,9.13,11.12,11.15,11.20,11.25,13.3,1.42,1.47,3.21,3.27,6.1,9.15,9.32,9.36,10.17,10.36,10.73,10.74,10.77,11.21,11.26,11.31,1.44,1.48,2.9,2.10,2.11,2.12,2.13,3.14,3.22,3.29,3.35,3.36,6.2,6.14,6.15,6.33,10.18,10.19,10.20,10.21,10.37,10.106,11.39,13.2,1.45,3.15,3.31,3.37,4.15,6.3,6.4,6.9,6.10,6.11,6.12,6.16,6.24,10.55,10.115,11.17,11.35,12.3,2.14,3.32,4.5,4.6,6.5,6.6,6.7,6.8,6.17,6.18,6.19,6.23,6.26,11.27,11.32,11.36,13.8,13.9,13.12,13.14,13.15,3.33,3.34,4.2,4.10,6.13,6.20,6.22,6.27,6.31,6.32,10.54,10.92,10.95,11.23,11.33,11.34,13.1,13.4,13.5,13.10,4.11,6.25,10.9,10.14,10.22,10.91,10.109,11.37,12.1,12.4,13.13,4.12,4.16,6.28,6.29,10.10,10.23,10.25,10.26,10.29,10.38,10.49,10.50,10.51,10.52,10.53,10.60,10.66,10.85,10.86,10.87,10.88,10.89,10.90,10.97,10.101,10.103,10.112,10.113,12.2,6.30,10.24,10.27,10.28,10.30,10.42,10.43,10.44,10.45,10.56,10.61,10.62,10.67,10.79,10.80,10.83,10.98,10.111,10.114,12.5,13.6,10.31,10.32,10.33,10.47,10.48,10.75,12.6,12.7,13.17,10.34,10.35,10.39,10.76,10.81,10.93,10.99,10.104,12.8,12.9,12.10,10.40,10.41,10.57,10.63,10.68,10.78,10.82,10.94,10.100,10.105,12.11,12.12,12.17,10.46,10.58,10.59,10.64,10.65,10.69,10.70,10.84,10.96,10.102,10.107,10.108,12.13,12.18,13.11,10.71,10.72,10.110,12.14,12.15,13.16,13.18}
In[]:=
eucdef["Book"10,"Theorem"11]["Text"]
Out[]=
If four magnitudes be proportional, and the first be commensurable with the second, the third will also be commensurable with the fourth; and, if the first be incommensurable with the second, the third will also be incommensurable with the fourth.
In[]:=
eucdef["Book"1,"Theorem"31]["Text"]
Axiom dependence
Axiom dependence
How many axioms does a given theorem depend on?
How many axioms does a given theorem depend on?
https://www.mathpages.com/home/kmath053.htm
https://www.mathpages.com/home/kmath053.htm
“Machine Code”
“Machine Code”
But let’s imagine we
Intermediate Theorems
Intermediate Theorems
Superaxioms
Superaxioms