-
Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
Authors:
William M. Farmer,
Dennis Y. Zvigelsky
Abstract:
Alonzo is a practice-oriented classical higher-order logic that extends first-order logic and that admits undefined expressions. Named in honor of Alonzo Church, Alonzo is based on Church's type theory, Church's formulation of simple type theory. The little theories method is a method for formalizing mathematical knowledge as a network of theories called a theory graph consisting of theories as no…
▽ More
Alonzo is a practice-oriented classical higher-order logic that extends first-order logic and that admits undefined expressions. Named in honor of Alonzo Church, Alonzo is based on Church's type theory, Church's formulation of simple type theory. The little theories method is a method for formalizing mathematical knowledge as a network of theories called a theory graph consisting of theories as nodes and theory morphisms as directed edges. The development of a mathematical topic is done in the "little theory" in the theory graph that has the most convenient level of abstraction and the most convenient vocabulary, and then the definitions and theorems produced in the development are transported, as needed, to other theories via the theory morphisms in the theory graph. The purpose of this paper is to illustrate how a body of mathematical knowledge can be formalized in Alonzo using the little theories method. This is done by formalizing monoid theory -- the body of mathematical knowledge about monoids -- in Alonzo.
△ Less
Submitted 15 November, 2024; v1 submitted 9 December, 2023;
originally announced December 2023.
-
Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal
Authors:
Jacques Carette,
William M. Farmer,
Michael Kohlhase,
Florian Rabe
Abstract:
Over the last decades, a class of important mathematical results have required an ever increasing amount of human effort to carry out. For some, the help of computers is now indispensable. We analyze the implications of this trend towards "big mathematics", its relation to human cognition, and how machine support for big math can be organized. The central contribution of this position paper is an…
▽ More
Over the last decades, a class of important mathematical results have required an ever increasing amount of human effort to carry out. For some, the help of computers is now indispensable. We analyze the implications of this trend towards "big mathematics", its relation to human cognition, and how machine support for big math can be organized. The central contribution of this position paper is an information model for "doing mathematics", which posits that humans very efficiently integrate four aspects: inference, computation, tabulation, and narration around a well-organized core of mathematical knowledge. The challenge for mathematical software systems is that these four aspects need to be integrated as well. We briefly survey the state of the art.
△ Less
Submitted 22 October, 2019; v1 submitted 23 April, 2019;
originally announced April 2019.
-
A New Style of Proof for Mathematics Organized as a Network of Axiomatic Theories
Authors:
William M. Farmer
Abstract:
A theory graph is a network of axiomatic theories connected with meaning-preserving mappings called theory morphisms. Theory graphs are well suited for organizing large bodies of mathematical knowledge. Traditional and formal proofs do not adequately fulfill all the purposes that mathematical proofs have, and they do not exploit the structure inherent in a theory graph. We propose a new style of p…
▽ More
A theory graph is a network of axiomatic theories connected with meaning-preserving mappings called theory morphisms. Theory graphs are well suited for organizing large bodies of mathematical knowledge. Traditional and formal proofs do not adequately fulfill all the purposes that mathematical proofs have, and they do not exploit the structure inherent in a theory graph. We propose a new style of proof that fulfills the principal purposes of a mathematical proof as well as capitalizes on the connections provided by the theory morphisms in a theory graph. This new style of proof combines the strengths of traditional proofs with the strengths of formal proofs.
△ Less
Submitted 1 December, 2018; v1 submitted 3 June, 2018;
originally announced June 2018.
-
Andrews' Type Theory with Undefinedness
Authors:
William M. Farmer
Abstract:
${\cal Q}_0$ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, ${\cal Q}_0$ does not admit undefined terms. The "traditional approach to undefinedness" in mathematical practice is to treat undefined terms as legitimate, nondenoting terms that can be components of meaningful statements. ${\cal Q}^{\rm u}_{0}…
▽ More
${\cal Q}_0$ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, ${\cal Q}_0$ does not admit undefined terms. The "traditional approach to undefinedness" in mathematical practice is to treat undefined terms as legitimate, nondenoting terms that can be components of meaningful statements. ${\cal Q}^{\rm u}_{0}$ is a modification of Andrews' type theory ${\cal Q}_0$ that directly formalizes the traditional approach to undefinedness. This paper presents ${\cal Q}^{\rm u}_{0}$ and proves that the proof system of ${\cal Q}^{\rm u}_{0}$ is sound and complete with respect to its semantics which is based on Henkin-style general models. The paper's development of ${\cal Q}^{\rm u}_{0}$ closely follows Andrews' development of ${\cal Q}_0$ to clearly delineate the differences between the two systems.
△ Less
Submitted 29 June, 2014;
originally announced June 2014.
-
Simple Type Theory with Undefinedness, Quotation, and Evaluation
Authors:
William M. Farmer
Abstract:
This paper presents a version of simple type theory called ${\cal Q}^{\rm uqe}_{0}$ that is based on ${\cal Q}_0$, the elegant formulation of Church's type theory created and extensively studied by Peter B. Andrews. ${\cal Q}^{\rm uqe}_{0}$ directly formalizes the traditional approach to undefinedness in which undefined expressions are treated as legitimate, nondenoting expressions that can be com…
▽ More
This paper presents a version of simple type theory called ${\cal Q}^{\rm uqe}_{0}$ that is based on ${\cal Q}_0$, the elegant formulation of Church's type theory created and extensively studied by Peter B. Andrews. ${\cal Q}^{\rm uqe}_{0}$ directly formalizes the traditional approach to undefinedness in which undefined expressions are treated as legitimate, nondenoting expressions that can be components of meaningful statements. ${\cal Q}^{\rm uqe}_{0}$ is also equipped with a facility for reasoning about the syntax of expressions based on quotation and evaluation. Quotation is used to refer to a syntactic value that represents the syntactic structure of an expression, and evaluation is used to refer to the value of the expression that a syntactic value represents. With quotation and evaluation it is possible to reason in ${\cal Q}^{\rm uqe}_{0}$ about the interplay of the syntax and semantics of expressions and, as a result, to formalize in ${\cal Q}^{\rm uqe}_{0}$ syntax-based mathematical algorithms. The paper gives the syntax and semantics of ${\cal Q}^{\rm uqe}_{0}$ as well as a proof system for ${\cal Q}^{\rm uqe}_{0}$. The proof system is shown to be sound for all formulas and complete for formulas that do not contain evaluations. The paper also illustrates some applications of ${\cal Q}^{\rm uqe}_{0}$.
△ Less
Submitted 8 December, 2016; v1 submitted 25 June, 2014;
originally announced June 2014.
-
Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation
Authors:
William M. Farmer
Abstract:
Chiron is a derivative of von-Neumann-Bernays-Gödel (NBG) set theory that is intended to be a practical, general-purpose logic for mechanizing mathematics. Unlike traditional set theories such as Zermelo-Fraenkel (ZF) and NBG, Chiron is equipped with a type system, lambda notation, and definite and indefinite description. The type system includes a universal type, dependent types, dependent functi…
▽ More
Chiron is a derivative of von-Neumann-Bernays-Gödel (NBG) set theory that is intended to be a practical, general-purpose logic for mechanizing mathematics. Unlike traditional set theories such as Zermelo-Fraenkel (ZF) and NBG, Chiron is equipped with a type system, lambda notation, and definite and indefinite description. The type system includes a universal type, dependent types, dependent function types, subtypes, and possibly empty types. Unlike traditional logics such as first-order logic and simple type theory, Chiron admits undefined terms that result, for example, from a function applied to an argument outside its domain or from an improper definite or indefinite description. The most noteworthy part of Chiron is its facility for reasoning about the syntax of expressions. Quotation is used to refer to a set called a construction that represents the syntactic structure of an expression, and evaluation is used to refer to the value of the expression that a construction represents. Using quotation and evaluation, syntactic side conditions, schemas, syntactic transformations used in deduction and computation rules, and other such things can be directly expressed in Chiron. This paper presents the syntax and semantics of Chiron, some definitions and simple examples illustrating its use, a proof system for Chiron, and a notion of an interpretation of one theory of Chiron in another.
△ Less
Submitted 27 May, 2013;
originally announced May 2013.
-
The MathScheme Library: Some Preliminary Experiments
Authors:
Jacques Carette,
William M. Farmer,
Filip Jeremic,
Vincent Maccio,
Russell O'Connor,
Quang M. Tran
Abstract:
We present some of the experiments we have performed to best test our design for a library for MathScheme, the mechanized mathematics software system we are building. We wish for our library design to use and reflect, as much as possible, the mathematical structure present in the objects which populate the library.
We present some of the experiments we have performed to best test our design for a library for MathScheme, the mechanized mathematics software system we are building. We wish for our library design to use and reflect, as much as possible, the mathematical structure present in the objects which populate the library.
△ Less
Submitted 9 June, 2011;
originally announced June 2011.
