Formal Language of GeometryConnection axiomslabelingangles and congruenceBirkhoff-MoiseAformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseA formalization of Hilbert’s AxiomsJohn T. BaldwinNovember 3, 2007Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseQuiz1 Suppose two mirrors are hinged at 90o. Are the followingtwo statements equivalent.1 No matter what angle you look at the mirror you will seeyour reflection.2 A line incident on one mirror is parallel to the line reflectedfrom the second.2 What is a proof?3 In teaching experiment 19 (Harel and Souder), what wasthe student’s misconception about a line?Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseGoalsFormal languages arose to remedy the lack of precision innatural language.1 Understand the use of axiom systems to ‘define’fundamental notions.2 See exact formalization of Hilbert as a basis forindependence proofs.Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseGeometric GoalsOver the course of the semester we want to understand threegeometric assertions and why we might or might not acceptthem.1 vertical angles are equal2 the congruence theorems3 the parallel postulateAformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseOutline1 Formal Language of Geometry2 Connection axioms3 labeling4 angles and congruence5 Birkhoff-MoiseAformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoisePlane GeometryWe are modifying Hilbert’s axioms in several ways. Numberingis as in Hilbert.We are only trying to axiomatize plane geometry so anythingrelating to higher dimensions is ignored.Note difference from Weinzweig.Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseThe objectsTwo SortsThere are two unary predicates: P and L.(∀x)P(x) ∨ L(x).(∀x)P(x) → ¬L(x).Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseRelationsbinary relation: I (x, y ) ”x on y”ternary relation: B(a, b, c) ”(c between a and b)”Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseConnection Axioms(∀x)(∀y)I (x, y ) → P(x) ∧ L(y).There is a unique line between any two points.exists(∀x)(∀y)[P(x) ∧ P(y ) → (∃z)L(z) ∧ I (x, z) ∧ I(y , z)].only one(∀x)(∀y)(∀z)(∀w )([x 6= y ∧ I(x, z) ∧ I (y, z) ∧ I (x, w) ∧ I (y, w)]→ w = z).Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseExamplesCan we construct finite models for these axioms?Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseOrder AxiomsII.1(∀x)(∀y)(∀z)B(x, y , z) → B(y, x, z).II.2 If two points are on a line there is a point on the linebetween them and a point so that one of these is between theother and the chosen point.(∀x1)(∀x2)[(∃w)[^i ≤2I (xi, w )∧(∃z)B(x1, x2, z) ∧ (∃w )B(x1, w , x2).Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseOrder Axioms IIII.3 If three points are on a line there is always one and onlywhich lies between the other two.(∀x1)(∀x2)(∀x3)[(∃w)[^i ≤3I (xi, w )→ B(x1, x2, x3) ∨ B(x2, x3, x1) ∨ B(x1, x3, x2).II.4 Four points on a straight line can be labeled so thatB(A, D, B), B(A, D, C), B(B, D, B), B(A, C , B).Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseLabelingIs this a correct statement of the Pythagorean Theorem?a2+ b2= c2Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseWhat about?c2+ a2= b2@@@@@acbAformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseDefinitionsSegmentIf A, B are on a line C is on the segment AB if B(A, B, C ).Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseCongruenceSegment CongruenceIntroduce a new 4-ary relation AB∼=CD.Intended meaning AB∼=CD iff AB is congruent to CD.Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseCongruenceAxioms on Segment CongruenceCongruence is an equivalence relation that is preserved whensegments are concatenated.Fix the segment: AB. On any ` through any C on `, there aretwo points D, D0on ` with CD∼=AB, CD0∼=AB.Hilbert (IV.1, IV.2, IV.3)Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseCongruenceAxioms on Segment CongruenceCongruence is an equivalence relation that is preserved whensegments are concatenated.Fix the segment: AB. On any ` through any C on `, there aretwo points D, D0on ` with CD∼=AB, CD0∼=AB.Hilbert (IV.1, IV.2, IV.3)Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseTaking StockToward angle congruenceNeed to define ”angle” carefully.Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoisePasch’s AxiomHilbert II.5A line which intersects one edge of a triangle and misses thethree vertices must intersect one of the other two edges.Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles andcongruenceBirkhoff-MoiseAnother DefinitionHalfplaneIf A, B are on a line, C and D are in the same halfplane AB ifthe segment CD does not intersect the line determined by AB.Aformalizationof Hilbert’sAxiomsJohn T.BaldwinFormalLanguage ofGeometryConnectionaxiomslabelingangles