-
The Church numbers in NF set theory
Authors:
Michael Beeson
Abstract:
By INF we mean Quine's NF set theory, with intuitionistic logic. We define the Church numerals (or better, Church numbers) and elaborate their properties in INF. The Church counting axiom says that iterating successor $n$ times, starting at zero, results in $n$. With the aid of the counting axiom we prove that the set of Church numbers is infinite. This is a new result even with classical logic; t…
▽ More
By INF we mean Quine's NF set theory, with intuitionistic logic. We define the Church numerals (or better, Church numbers) and elaborate their properties in INF. The Church counting axiom says that iterating successor $n$ times, starting at zero, results in $n$. With the aid of the counting axiom we prove that the set of Church numbers is infinite. This is a new result even with classical logic; that is, just because there is some infinite set, it is not immediate that the set of Church numbers is infinite. Specker showed in 1953 that classical NF proves the existence of an infinite set. It has long been an open problem whether INF can prove that. Now we show that it can be done intuitionistically, with the aid of the Church counting axiom. We also prove, without the aid of the counting axiom, that if the set of Church numbers is not finite, then it is infinite, and Church successor is one-to-one. Consequently, Heyting's arithmetic is interpretable in INF plus the Church counting axiom.
△ Less
Submitted 21 November, 2021; v1 submitted 21 July, 2021;
originally announced August 2021.
-
Intuitionistic NF Set Theory
Authors:
Michael Beeson
Abstract:
We develop NF set theory using intuitionistic logic; we call this theory INF. We develop the theories of finite sets and their power sets, finite cardinals and their ordering, cardinal exponentiation, addition, and multiplication. We follow Rosser and Specker with appropriate constructive modifications, especially replacing "arbitrary subset" by "separable subset" in the definitions of exponentiat…
▽ More
We develop NF set theory using intuitionistic logic; we call this theory INF. We develop the theories of finite sets and their power sets, finite cardinals and their ordering, cardinal exponentiation, addition, and multiplication. We follow Rosser and Specker with appropriate constructive modifications, especially replacing "arbitrary subset" by "separable subset" in the definitions of exponentiation and order. It is not known whether \INF\ proves that the set of finite cardinals is infinite, so the whole development must allow for the possibility that there is a maximum integer; arithmetical computations might "overflow" as in a computer or odometer, and theorems about them must be carefully stated to allow for this possibility. The work presented here is intended as a substrate for further investigations of INF.
△ Less
Submitted 25 June, 2025; v1 submitted 31 March, 2021;
originally announced April 2021.
-
Euclid After Computer Proof-checking
Authors:
Michael Beeson
Abstract:
Euclid pioneered the concept of a mathematical theory developed from axioms by a series of justified proof steps. From the outset there were critics and improvers. In this century the use of computers to check proofs for correctness sets a new standard of rigor. How does Euclid stand up under such an examination? And what does the exercise have to teach us about geometry, mathematical foundations,…
▽ More
Euclid pioneered the concept of a mathematical theory developed from axioms by a series of justified proof steps. From the outset there were critics and improvers. In this century the use of computers to check proofs for correctness sets a new standard of rigor. How does Euclid stand up under such an examination? And what does the exercise have to teach us about geometry, mathematical foundations, and the relation of logic to truth?
△ Less
Submitted 16 March, 2021;
originally announced March 2021.
-
On the Notion of Equal Figures in Euclid
Authors:
Michael Beeson
Abstract:
Euclid uses an undefined notion of "equal figures", to which he applies the common notions about equals added to equals or subtracted from equals. When (in previous work) we formalized Euclid Book~I for computer proof-checking, we had to add fifteen axioms about undefined relations "equal triangles" and "equal quadrilaterals" to replace Euclid's use of the common notions. In this paper, we offer d…
▽ More
Euclid uses an undefined notion of "equal figures", to which he applies the common notions about equals added to equals or subtracted from equals. When (in previous work) we formalized Euclid Book~I for computer proof-checking, we had to add fifteen axioms about undefined relations "equal triangles" and "equal quadrilaterals" to replace Euclid's use of the common notions. In this paper, we offer definitions of "equal triangles" and "equal quadrilaterals", that Euclid could have given, and prove that they have the required properties. This removes the need for adding new axioms. The proof uses the theory of proportions. Hence we also discuss the "early theory of proportions", which has a long history.
△ Less
Submitted 2 April, 2022; v1 submitted 14 August, 2020;
originally announced August 2020.
-
Tiling an Equilateral Triangle
Authors:
Michael Beeson
Abstract:
Let $ABC$ be an equilateral triangle. For certain triangles $T$ (the "tile") and certain $N$, it is possible to cut $ABC$ into $N$ copies of $T$. It is known that only certain shapes of $T$ are possible, but until now very little was known about the possible values of $N$. Here we prove that for $N>3$, $N$ cannot be prime, and study more closely the possible tilings when the tile has a $π/3$ angle…
▽ More
Let $ABC$ be an equilateral triangle. For certain triangles $T$ (the "tile") and certain $N$, it is possible to cut $ABC$ into $N$ copies of $T$. It is known that only certain shapes of $T$ are possible, but until now very little was known about the possible values of $N$. Here we prove that for $N>3$, $N$ cannot be prime, and study more closely the possible tilings when the tile has a $π/3$ angle.
△ Less
Submitted 28 May, 2024; v1 submitted 17 December, 2018;
originally announced December 2018.
-
No triangle can be cut into seven congruent triangles
Authors:
Michael Beeson
Abstract:
We prove the theorem in the title, and prove the theorem for 11 as well as 7. By previous work of others, the problem reduces to a number of cases. The cases not solved already are solved here.
We prove the theorem in the title, and prove the theorem for 11 as well as 7. By previous work of others, the problem reduces to a number of cases. The cases not solved already are solved here.
△ Less
Submitted 16 June, 2019; v1 submitted 23 November, 2018;
originally announced November 2018.
-
Brouwer and Euclid
Authors:
Michael Beeson
Abstract:
We explore the relationship between Brouwer's intuitionistic mathematics and Euclidean geometry. Brouwer wrote a paper in 1949 called "The contradictority of elementary geometry". In that paper, he showed that a certain classical consequence of the parallel postulate implies Markov's principle, which he found intuitionistically unacceptable. But Euclid's geometry, having served as a beacon of clea…
▽ More
We explore the relationship between Brouwer's intuitionistic mathematics and Euclidean geometry. Brouwer wrote a paper in 1949 called "The contradictority of elementary geometry". In that paper, he showed that a certain classical consequence of the parallel postulate implies Markov's principle, which he found intuitionistically unacceptable. But Euclid's geometry, having served as a beacon of clear and correct reasoning for two millenia, is not so easily discarded.
Brouwer started from a "theorem" that is not in Euclid, and requires Markov's principle for its proof. That means that Brouwer's paper did not address the question whether Euclid's "Elements" really requires Markov's principle. In this paper we show that there is a coherent theory of "non-Markovian Euclidean geometry."
We show in some detail that our theory is an adequate formal rendering of (at least) Euclid's Book~I, and suffices to define geometric arithmetic, thus refining the author's previous investigations (which include Markov's principle as an axiom).
Philosophically, Brouwer's proof that his version of the parallel postulate implies Markov's principle could be read just as well as geometric evidence for the truth of Markov's principle, if one thinks the geometrical "intersection theorem" with which Brouwer started is geometrically evident.
△ Less
Submitted 24 May, 2017;
originally announced May 2017.
-
Finding Proofs in Tarskian Geometry
Authors:
Michael Beeson,
Larry Wos
Abstract:
We report on a project to use a theorem prover to find proofs of the theorems in Tarskian geometry. These theorems start with fundamental properties of betweenness, proceed through the derivations of several famous theorems due to Gupta and end with the derivation from Tarski's axioms of Hilbert's 1899 axioms for geometry. They include the four challenge problems left unsolved by Quaife, who two d…
▽ More
We report on a project to use a theorem prover to find proofs of the theorems in Tarskian geometry. These theorems start with fundamental properties of betweenness, proceed through the derivations of several famous theorems due to Gupta and end with the derivation from Tarski's axioms of Hilbert's 1899 axioms for geometry. They include the four challenge problems left unsolved by Quaife, who two decades ago found some \Otter proofs in Tarskian geometry (solving challenges issued in Wos's 1998 book). There are 212 theorems in this collection. We were able to find \Otter proofs of all these theorems. We developed a methodology for the automated preparation and checking of the input files for those theorems, to ensure that no human error has corrupted the formal development of an entire theory as embodied in two hundred input files and proofs. We distinguish between proofs that were found completely mechanically (without reference to the steps of a book proof) and proofs that were constructed by some technique that involved a human knowing the steps of a book proof. Proofs of length 40--100, roughly speaking, are difficult exercises for a human, and proofs of 100-250 steps belong in a Ph.D. thesis or publication. 29 of the proofs in our collection are longer than 40 steps, and ten are longer than 90 steps. We were able to derive completely mechanically all but 26 of the 183 theorems that have "short" proofs (40 or fewer deduction steps). We found proofs of the rest, as well as the 29 "hard" theorems, using a method that requires consulting the book proof at the outset. Our "subformula strategy" enabled us to prove four of the 29 hard theorems completely mechanically. These are Ph.D. level proofs, of length up to 108.
△ Less
Submitted 22 June, 2016;
originally announced June 2016.
-
The number of minimal surfaces bounded by Enneper's wire
Authors:
Michael Beeson
Abstract:
Enneper's wire, the image of the circle of radius $R$ under Enneper's surface, bounds exactly three minimal surfaces for $R$ between 1 and $\sqrt 3$, and these three surfaces depend continuously on $R$.
The other two surfaces (besides Enneper's surface) are absolute minima of area among disk-type surfaces bounded by Enneper's wire. These surfaces each have a unique horizontal tangent plane, whos…
▽ More
Enneper's wire, the image of the circle of radius $R$ under Enneper's surface, bounds exactly three minimal surfaces for $R$ between 1 and $\sqrt 3$, and these three surfaces depend continuously on $R$.
The other two surfaces (besides Enneper's surface) are absolute minima of area among disk-type surfaces bounded by Enneper's wire. These surfaces each have a unique horizontal tangent plane, whose height can be computed from $R$, and they are invariant under reflections in the planes $x_1=0$ and $x_2 = 0$. These two surfaces have positive second variation of area, and depend continuously on $R$. This result solves three open problems from the list in Nitche's 1989 book.
Enneper's wire is the only Jordan curve $Γ$ bounding more than one minimal surface for which a specific bound on the number of minimal surfaces bounded by $Γ$ is known.
△ Less
Submitted 26 February, 2016; v1 submitted 22 May, 2015;
originally announced June 2015.
-
Herbrand's theorem and non-Euclidean geometry
Authors:
Michael Beeson,
Pierre Boutry,
Julien Narboux
Abstract:
We use Herbrand's theorem to give a new proof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing pro…
▽ More
We use Herbrand's theorem to give a new proof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.
△ Less
Submitted 23 February, 2015; v1 submitted 7 October, 2014;
originally announced October 2014.
-
A Constructive Version of Tarski's Geometry
Authors:
Michael Beeson
Abstract:
Euclid's reasoning is essentially constructive. Tarski's elegant and concise first-order theory of Euclidean geometry, on the other hand, is essentially non-constructive, even if we restrict attention (as we do here) to the theory with line-circle and circle-circle continuity in place of first-order Dedekind completeness. Here we exhibit three constructive versions of Tarski's theory. One, like Ta…
▽ More
Euclid's reasoning is essentially constructive. Tarski's elegant and concise first-order theory of Euclidean geometry, on the other hand, is essentially non-constructive, even if we restrict attention (as we do here) to the theory with line-circle and circle-circle continuity in place of first-order Dedekind completeness. Here we exhibit three constructive versions of Tarski's theory. One, like Tarski's theory, has existential axioms and no function symbols. We then consider a version in which function symbols are used instead of existential quantifiers. The third version has a function symbol for the intersection point of two non-parallel, non-coincident lines, instead of only for intersection points produced by Pasch's axiom and the parallel axiom; this choice of function symbols connects directly to ruler-and-compass constructions. All three versions have this in common: the axioms have been modified so that the points they assert to exist are unique and depend continuously on parameters. This modification of Tarski's axioms, with classical logic, has the same theorems as Tarski's theory, but we obtain results connecting it with ruler-and-compass constructions as well. In particular, points constructively proved to exist can be constructed with ruler and compass, uniformly in parameters; the same is true with non-constructive proofs if several constructions are allowed for different cases.
△ Less
Submitted 5 July, 2015; v1 submitted 13 July, 2014;
originally announced July 2014.
-
Constructive Geometry and the Parallel Postulate
Authors:
Michael Beeson
Abstract:
Euclidean geometry consists of straightedge-and-compass constructions and reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. We consider three versions of Euclid's parallel postulate: Euclid's own formulation in his Postulate 5; Playfair's 1795 version, and a new version we call the strong parallel postulate. These…
▽ More
Euclidean geometry consists of straightedge-and-compass constructions and reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. We consider three versions of Euclid's parallel postulate: Euclid's own formulation in his Postulate 5; Playfair's 1795 version, and a new version we call the strong parallel postulate. These differ in that Euclid's version and the new version both assert the existence of a point where two lines meet, while Playfair's version makes no existence assertion. Classically, the models of Euclidean (straightedge-and-compass) geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to the different versions of the parallel axiom. In this paper, we completely settle the questions about implications between the three versions of the parallel postulate: the strong parallel postulate easily implies Euclid 5, and in fact Euclid 5 also implies the strong parallel postulate, although the proof is lengthy, depending on the verification that Euclid 5 suffices to define multiplication geometrically. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions.
△ Less
Submitted 31 October, 2015; v1 submitted 13 July, 2014;
originally announced July 2014.
-
Triangle Tiling I: The tile is similar to ABC or has a right angle
Authors:
Michael Beeson
Abstract:
An N -tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile'".
The tile may or may not be similar to ABC . This paper is the first of several papers, which together seek a complete characterization of the triples (ABC,N,T) such that ABC can be N -tiled by T . In this paper, we consi…
▽ More
An N -tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile'".
The tile may or may not be similar to ABC . This paper is the first of several papers, which together seek a complete characterization of the triples (ABC,N,T) such that ABC can be N -tiled by T . In this paper, we consider the case in which the tile is similar to ABC, the case in which the tile is a right triangle, and the case when ABC is equilateral.
We use (only) techniques from linear algebra and elementary field theory, as well as elementary geometry and trigonometry.
Our results (in this paper) are as follows: When the tile is similar to ABC, we always have "quadratic tilings'" when N is a square. If the tile is similar to ABC and is not a right triangle, then N is a square. If N is a sum of two squares, N = e^2 + f^2, then a right triangle with legs e and f can be N -tiled by a tile similar to ABC ; these tilings are called "biquadratic". If the tile and ABC are 30-60-90 triangles, then N can also be three times a square. If T is similar to ABC, these are all the possible triples (ABC, T, N) .
If the tile is a right triangle, of course it can tile a certain isosceles triangle when N is twice a square, and in some cases when N is six times a square.
Equilateral triangles can be 3-tiled and 6-tiled and hence they can also be 3n^2 and 6n^2 tiled for any n . We also discovered a family of tilings when N is 3 times a square, which we call the "hexagonal tilings." These tilings exhaust all the possible triples (ABC, T, N) in case T is a right triangle or is similar to ABC . Other cases are treated in subsequent papers.
△ Less
Submitted 4 June, 2012;
originally announced June 2012.
-
Triangle Tiling II: Nonexistence theorems
Authors:
Michael Beeson
Abstract:
An N -tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile".
The tile may or may not be similar to ABC . We wish to understand possible tilings by completely characterizing the triples (ABC, T, N) such that ABC can be N -tiled by T. In particular, this understanding should enable u…
▽ More
An N -tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile".
The tile may or may not be similar to ABC . We wish to understand possible tilings by completely characterizing the triples (ABC, T, N) such that ABC can be N -tiled by T. In particular, this understanding should enable us to specify for which N there exists a tile T and a triangle ABC that is N-tiled by T; or given N, determine which tiles and triangles can be used for N-tilings; or given ABC, to determine which tiles and N can be used to N-tile ABC. This is the second of four papers on this subject. In the first paper, we dealt with the case when ABC is similar to T, and the case when T is a right triangle. In this paper, we assume that ABC is not similar to T, and T is not a right triangle, and furthermore that if T has a 120 degree angle, then T is isosceles.
Under those hypotheses, there are only two families of tilings. There are tilings of an equilateral triangle ABC by an isosceles tile with base angles 30 degrees, and there are newly-discovered "triquadratic tilings", which are treated in the third paper in this series. These arise in the special case that 3α+ 2β= πor 3β+ 2α= πwith αnot a rational multiple of π, where αand βare the two smallest angles of the tile, and the sides of the tile have rational ratios.
The case when the tile has a 120 degree angle and is not isosceles is taken up in a subsequent paper.
We use techniques from linear algebra and elementary field theory, and in one case we use some algebraic number theory. We use some counting arguments and some elementary geometry and trigonometry.
△ Less
Submitted 4 June, 2012;
originally announced June 2012.
-
Triangle Tiling: The case $3α+ 2β= π$
Authors:
Michael Beeson
Abstract:
An $N$-tiling of triangle $ABC$ by triangle $T$ (the `tile') is a way of writing $ABC$ as a union of $N$ copies of $T$ overlapping only at their boundaries. Let the tile $T$ have angles $(α,β,γ)$, and sides $(a,b,c)$. This paper takes up the case when $3α+ 2β= π$. Then there are (as was already known) exactly five possible shapes of $ABC$: either $ABC$ is isosceles with base angles $α$, $β$, or…
▽ More
An $N$-tiling of triangle $ABC$ by triangle $T$ (the `tile') is a way of writing $ABC$ as a union of $N$ copies of $T$ overlapping only at their boundaries. Let the tile $T$ have angles $(α,β,γ)$, and sides $(a,b,c)$. This paper takes up the case when $3α+ 2β= π$. Then there are (as was already known) exactly five possible shapes of $ABC$: either $ABC$ is isosceles with base angles $α$, $β$, or $α+β$, or the angles of $ABC$ are $(2α,β,α+β)$, or the angles of $ABC$ are $(2α, α, 2β)$. In each of these cases, we have discovered, and here exhibit, a family of previously unknown tilings. These are tilings that, as far as we know, have never been seen before. We also discovered, in each of the cases, a Diophantine equation involving $N$ and the (necessarily rational) number $s = a/c$ that has solutions if there is a tiling using tile $T$ of some $ABC$ not similar to $T$. By means of these Diophantine equations, some conclusions about the possible values of $N$ are drawn; in particular there are no tilings possible for values of $N$ of certain forms. We prove, for example, that there is no $N$-tiling with $N$ prime when $3α+ 2β= π$. These equations also imply that for each $N$, there is a finite set of possibilities for the tile $(a,b,c)$ and the triangle $ABC$. (Usually, but not always, there is just one possible tile.) These equations provide necessary, and in three of the five cases sufficient, conditions for the existence of $N$-tilings.
△ Less
Submitted 13 February, 2019; v1 submitted 4 June, 2012;
originally announced June 2012.
-
Triangle Tiling V: Tilings by a tile with integer sides
Authors:
Michael Beeson
Abstract:
An N-tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile". The tile may or may not be similar to ABC. We wish to understand possible tilings by completely characterizing the triples (ABC, T, N) such that ABC can be N-tiled by T. In particular, this understanding should enable us to…
▽ More
An N-tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile". The tile may or may not be similar to ABC. We wish to understand possible tilings by completely characterizing the triples (ABC, T, N) such that ABC can be N-tiled by T. In particular, this understanding should enable us to specify for which N there exists a tile T and a triangle ABC that is N-tiled by T; or given N, to determine which tiles and triangles can be used for N-tilings; or given ABC, to determine which tiles and N can be used to N-tile ABC. This is the fifth paper in a series of papers on this subject. The previous papers have reduced the problem the case when T has a 120 degree angle and integer side lengths. That is the problem we take up in this paper. We are still not able to completely solve the problem, but we prove that if there are any N-tilings by such tiles, then N is at least 96. Combining this results with our earlier work, we can remove the exception for a tile with a 120 degree angle, obtaining definitive non-existence results. For example, there is no 7-tiling, no 11-tiling, no 14-tiling, no 19-tiling, no 31-tiling, no 41-tiling, etc.
Regarding the number N=96: There are several possible shapes of ABC, and for each shape, we exhibit the smallest N for which it is presently unknown whether there is an N-tiling. For example, for equilateral ABC, the simplest unsolved case as of May, 2012 is N=135. For each of these minimal-N examples, the tile would have to have sides (3,5,7).
△ Less
Submitted 27 May, 2024; v1 submitted 4 June, 2012;
originally announced June 2012.
-
Tilings of an Isosceles Triangle
Authors:
Michael Beeson
Abstract:
An N-tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile". The tile may or may not be similar to ABC. In this paper we study the case of isosceles (but not equilateral) ABC. We study three possible forms of the tile: right-angled, or with one angle double another, or with a 120 degr…
▽ More
An N-tiling of triangle ABC by triangle T is a way of writing ABC as a union of N triangles congruent to T, overlapping only at their boundaries. The triangle T is the "tile". The tile may or may not be similar to ABC. In this paper we study the case of isosceles (but not equilateral) ABC. We study three possible forms of the tile: right-angled, or with one angle double another, or with a 120 degree angle. In the case of a right-angled tile, we give a complete characterization of the tilings, and prove that N must be even. In the latter two cases we prove the ratios of the sides of the tile are rational, and give a necessary condition for the existence of an N-tiling. For the case when the tile has one angle double another, we prove N cannot be prime or even squarefree.
△ Less
Submitted 28 May, 2024; v1 submitted 9 June, 2012;
originally announced June 2012.
-
A real-analytic Jordan curve cannot bound infinitely many relative minima of area
Authors:
Michael Beeson
Abstract:
Let C be a real-analytic Jordan curve in $R^3$. Then C cannot bound infinitely many disk-type minimal surfaces which provide relative minima of area.
Let C be a real-analytic Jordan curve in $R^3$. Then C cannot bound infinitely many disk-type minimal surfaces which provide relative minima of area.
△ Less
Submitted 22 May, 2015; v1 submitted 30 November, 2006;
originally announced December 2006.
