Searcharxiv⌕ Search

arXiv subjects

Michael Beeson

Publications and source records attributed to Michael Beeson.

24 records · Page 2Linked to original sources
arXiv2015

A Constructive Version of Tarski's Geometry

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.

math.LO↗
arXiv2015

Herbrand's theorem and non-Euclidean geometry

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.

math.LO↗
arXiv2012

Triangle Tiling II: Nonexistence theorems

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.

math.MG↗
arXiv2012

Triangle Tiling I: The tile is similar to ABC or has a right angle

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.

math.MG↗
arXiv2003

Double-Negation Elimination in Some Propositional Logics

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.

cs.LO↗