Search

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., Comment: 92 pages, 2 figures. This version added Section 20; the previous Section 20 became Section 21

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., Comment: 89 pages. This version added one more lemma. arXiv admin note: text overlap with arXiv:2108.09270

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?, Comment: 25 pages, 16 figures. To appear in American Mathematical Monthly in 2022

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., Comment: 38 pages, 28 figures

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 $\pi/3$ angle., Comment: 24 pages, 11 figures. This version added pictures of new tilings found by Herdt, and a table of unsolved values of N

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., Comment: 39 pages, 26 figures. The treatment of isosceles triangles has been replaced by a citation of the paper Tilings of an Isosceles Triangle, which seems a better organization of the material and reduces the length of this paper. arXiv admin note: text overlap with arXiv:1206.1974

We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid's gaps and correcting errors. Euclid Book I has 48 propositions, we proved 235 theorems. The extras were partly "Book Zero", preliminaries of a very fundamental nature, partly propositions that Euclid omitted but were used implicitly, partly advanced theorems that we found necessary to fill Euclid's gaps, and partly just variants of Euclid's propositions. We wrote these proofs in a simple fragment of first-order logic corresponding to Euclid's logic, debugged them using a custom software tool, and then checked them in the well-known and trusted proof checkers HOL Light and Coq., Comment: 53 pages

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., Comment: 61 pages, 18 figures

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., Comment: 32 pages, 4 figures, 4 tables. Supplementary computer code published separately

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 $\Gamma$ bounding more than one minimal surface for which a specific bound on the number of minimal surfaces bounded by $\Gamma$ is known., Comment: This paper has been withdrawn by the author. The claim that the surfaces all contain two crossed horizontal lines is actually false. The problems posed by Nitsche remain open

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., Comment: 12 pages, 5 figures

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., Comment: 114 pages, 39 figures

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., Comment: 92 pages, 30 figures. Final pre-publication version

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., Comment: 59 pages, 25 figures. This version contains new tilings found by Herdt

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)., Comment: Theorem 1 is wrong; tilings described in later papers contradict it. Line 4, page 8, is the error in the alleged proof. This paper is not used in any of my other papers on triangle tiling

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\alpha + 2\beta = \pi or 3\beta+ 2\alpha = \pi with \alpha not a rational multiple of \pi, where \alpha and \beta 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.

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.

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 $(\alpha,\beta,\gamma)$, and sides $(a,b,c)$. This paper takes up the case when $3\alpha + 2\beta = \pi$. Then there are (as was already known) exactly five possible shapes of $ABC$: either $ABC$ is isosceles with base angles $\alpha$, $\beta$, or $\alpha+\beta$, or the angles of $ABC$ are $(2\alpha,\beta,\alpha+\beta)$, or the angles of $ABC$ are $(2\alpha, \alpha, 2\beta)$. 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\alpha + 2\beta = \pi$. 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., Comment: 94 pages, 27 figures. This version adds the theorem that N cannot be prime for tilings of the form treated in the paper, and also corrects and improves some proofs; and improves one of the tiling-equation theorems to "necessary and sufficient" instead of just "necessary"

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., Comment: This revision removes some unnecessary lemmas, adds an outline of the proof, and corrects some typos

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the form n(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program OTTER played an indispensable role in this study., Comment: 32 pages, no figures