The text above includes direct links to specific documents and references. Here we’ll give a slightly more general bibliography, though most of it should be considered background, since the approach taken here represents a significant departure from traditional directions, and builds more or less directly on extremely low-level concepts.
The earliest known large-scale axiomatic presentation of mathematics was:
Euclid (300 BC), Στοιχεῖα (in Ancient Greek) [Elements].
Empirical metamathematics from this was given in:
The concept that there is underlying reality in mathematics was discussed in:
Plato (375 BC), πολιτεία (in Ancient Greek) [The Republic].
Plato (360 BC), Τίμαιος (in Ancient Greek) [Timaeus].
Modern explorations of these ideas include:
M. Balaguer (1998), Platonism and Anti-Platonism in Mathematics, Oxford University Press.
J. Gray (2008), Plato’s Ghost: The Modernist Transformation of Mathematics, Princeton University Press.
R. Tieszen (2011), After Gödel: Platonism and Rationalism in Mathematics and Logic, Oxford University Press.
The contemporary axiomatic formulation of mathematics was developed in:
F. L. G. Frege (1879), Begriffsschrift: eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (in German), Verlag von Louis Neber. (Translated in J. v. Heijenoort (1967), as “Begriffsschrift: A Formal Language, Modeled upon That of Arithmetic, for Pure Thought” in From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Harvard University Press, 1–82.)
R. Dedekind (1888), Was sind und was sollen die Zahlen? (in German), F. Vieweg und Sohn. (Translated in H. Pogorzelski, et al. (1995), as What Are Numbers and What Should They Be?, Research Institute for Mathematics.)
G. Peano (1889), Arithmetices principia, nova methodo exposita (in Italian), Fratres Bocca. (Translated by H. C. Kennedy (1973), as “The Principles of Arithmetic, Presented by a New Method”, in Selected Works of Giuseppe Peano, University of Toronto Press, 101–134.)
D. Hilbert (1903), Grundlagen der geometrie (in German), B. G. Teubner. (Translated by E. G. Townsend (1902), as The Foundations of Geometry, Open Court.)
E. Zermelo (1908), “Untersuchungen ü
ber die Grundlagen der Mengenlehre I” (in German), Mathematische Annalen
. (Translated by J. v. Heijenoort (1967), as “Investigations in the Foundations of Set Theory” in From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931
, Harvard University Press, 199–
A. N. Whitehead and B. A. W. Russell (1910–1913), Principia Mathematica, Volumes I–III, Cambridge University Press.
A standard collection of source documents is:
J. v. Heijenoort (1967), From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Harvard University Press.
Among general commentaries on axiomatic formalism are:
N. Bourbaki (1950), “The Architecture of Mathematics”, The American Mathematical Monthly
232. doi: 10.2307/2305937
S. Feferman, et al. (2000), “Does Mathematics Need New Axioms?”, The Bulletin of Symbolic Logic 6
446. doi: 10.2307/420965.
W. Sieg (2013), Hilbert’s Programs and Beyond, Oxford University Press.
Expositions of metamathematics and mathematical logic ideas appear for example in:
D. Hilbert and W. Ackermann (1928), Grundzüge der theoretischen Logik (in German), Springer. (Translated by L. M. Hammond, et al. (2000), as Principles of Mathematical Logic, AMS Chelsea.)
W. V. O. Quine (1940), Mathematical Logic, W. W. Norton & Company.
A. Church (1956), Introduction to Mathematical Logic, Princeton University Press.
H. Wang (1962), A Survey of Mathematical Logic, Science Press North-Holland.
H. B. Curry (1963), Foundations of Mathematical Logic, Dover.
H. Rasiowa (1963), The Mathematics of Metamathematics, Panstwowe Wydawnictwo Naukowe.
E . Mendelson (1964), Intro to Mathematical Logic, Van Nostrand Reinhold.
G. Kreisel and J. L. Krivine (1967), Elements of Mathematical Logic: Model Theory,
S. C. Kleene (1971), Introduction to Metamathematics, Wolters-Noordhoff.
H. B. Enderton (1972), A Mathematical Introduction to Logic, Harcourt/Academic Press.
A. Yasuhara (1975), “Recursive Function Theory and Logic”, Journal of Symbolic Logic
620. doi: 10.2307/2271829.
J. Barwise (1982), Handbook of Mathematical Logic, Elsevier.
G. E. Sacks (2003), Mathematical Logic in the 20th Century, World Scientific.
Works on the metamodeling of mathematics and on universal algebra include:
A. N. Whitehead (1898), A Treatise on Universal Algebra with Applications, Cambridge University Press.
A. Robinson (1963), Introduction to Model Theory and to the Metamathematics of Algebra, North-Holland.
N. G. de Bruijn (1970), “The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions”, in Symposium on Automatic Demonstration, M. Laudet, et al. (eds.), Springer.
A. I. Mal’Cev (1971), The Metamathematics of Algebraic Systems, Collected Papers: 1936–1967, North-Holland.
A. S. Toelstra (1973), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer.
S. Burris and H. P. Sankappanavar (1981), A Course in Universal Algebra, Springer.
Low-level symbolic representations of mathematics were developed in:
nfinkel (1924), “Ü
ber die Bausteine der mathematischen Logik” (in German), Mathematische Annalen
316. doi: 10.1007/BF01448013
. (Translated by S. Bauer-Mengelberg (1967), as “On the Building Blocks of Mathematical Logic”, in From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931
, J. v. Heijenoort, Harvard University Press, 357–
E. Post (1936), “Finite Combinatory Processes—
Formulation 1”, The Journal of Symbolic Logic
105. doi: 10.2307/2269031.
See also these commentaries:
S. Wolfram (2021), Combinators: A Centennial View, Wolfram Media.
Practical representation of mathematics using symbolic transformations was developed in:
S. Wolfram (1988), Mathematica: A System for Doing Mathematics by Computer, Addison-Wesley.
A proof of the “arithmeticization of metamathematics” was given in:
del (1931), “Ü
ber formal unentscheidbare Sä
tze der Principia Mathematica
und verwandter Systeme, I” (in German), Monatshefte für Mathematik und Physik
198. doi: 10.1007/BF01700692
. (Translated by B. Meltzer (1992), as On Formally Undecidable Propositions of Principia Mathematica and Related Systems
A major precursor to the current work is:
Our Physics Project is described in:
S. Wolfram (2020), A Project to Find the Fundamental Theory of Physics, Wolfram Media.
The concept of the ruliad was introduced in:
The concept of the mathematical observer was introduced in:
Automated theorem proving is discussed for example in:
A. Robinson and A. Voronkov (2001), Handbook of Automated Reasoning: Volume I, Elsevier.
Relevant Wolfram Language functions include:
A system for low-level proof-oriented formalized mathematics (used here for empirical
N. Megill and D. A. Wheeler (2019), Metamath: A Computer Language for Mathematical Proofs, Lulu.
Other systems for proof-oriented formalized mathematics include:
University of Cambridge and Technical University of Munich (1986), Isabelle [Software system]. isabelle.in.tum.de.
T. Coquand and G. Huet (1989), Coq [Software system]. coq.inria.fr
Discussions of formalized mathematics include:
H. Wang (1960), “Toward Mechanical Mathematics”, IBM Journal of Research and Development
22. doi: 10.1147/rd.41.0002
J. Avigad and J. Harrison (2014), “Formally Verified Mathematics”, Communications of the ACM
75. doi: 10.1145/2591012
M. Ganesalingam and W. T. Gowers (2017), “A Fully Automatic Theorem Prover with Human-Style Output”, Journal of Automated Reasoning
291. doi: 10.1007/s10817-016-9377-1
K. Buzzard (2021), “What Is the Point of Computers? A Question for Pure Mathematicians”. arXiv: 2112.11598
Books on the philosophy of mathematics and its foundations include:
P. Benacerraf and H. Putnam (eds.) (1964), Philosophy of Mathematics: Selected Readings, Prentice-Hall.
I. Lakatos (1976), Proofs and Refutations: The Logic of Mathematical Discovery, Cambridge University Press.
T. Tymoczko (1986), New Directions in the Philosophy of Mathematics, Birkhäuser.
S. Shapiro (2000), Thinking about Mathematics: The Philosophy of Mathematics, Oxford University Press.
R. Krömer (2007), Tool and Object: A History and Philosophy of Category Theory, Springer.
E. Grosholz and H. Breger (2013), The Growth of Mathematical Knowledge, Springer.
The philosophical study of mathematics in terms of interrelated structure is summarized in:
The structure of proof space is discussed in univalent foundations and homotopy
The Univalent Foundations Program (2013), Homotopy Type Theory, Institute for
S. Awodey, et al.
(2013), “Voevodsky’s Univalence Axiom in Homotopy Type Theory”, Notices of the AMS
1167. doi: 10.48550/arxiv.1302.4731
M. Shulman (2021), “Homotopy Type Theory: The Logic of Space” in New Spaces in Mathematics: Volume 1 Formal and Conceptual Reflections, M. Anel and G. Catren (eds.), Cambridge University Press.
Relations between category theory, mathematics and our Physics Project were explored in:
X. D. Arsiwalla, J. Gorard, and H. Elshatlawy (2021), “Homotopies in Multiway (Non-deterministic) Rewriting Systems as n
-Fold Categories”. arXiv:2105.10822
X. D. Arsiwalla and J. Gorard (2021), “Pregeometric Spaces from Wolfram Model Rewriting Systems as Homotopy Types”. arXiv:2111.03460