|
Axioms for various systems of geometry usually use a typed language, with the different types corresponding to different geometric objects such as points, lines, circles, planes, and so on. The signature will often consist of binary incidence relations between objects of different types; for example, the relation that a point lies on a line. The signature may have more complicated relations; for example ordered geometry might have a ternary "betweenness" relation for 3 points, which says whether one lies between two others, or a "congruence" relation between 2 pairs of points. Some examples of axiomatized systems of geometry include ordered geometry, absolute geometry, affine geometry, Euclidean geometry, projective geometry, and hyperbolic geometry. For each of these geometries there are many different and inequivalent systems of axioms for various dimensions. Some of these axiom systems include "completeness" axioms that are not first order. As a typical example, the axioms for projective geometry use 2 types, points and lines, and a binary incidence relation between points and lines. If point and line variables are indicated by small and capital letter, and a incident to A is written as aA, then one set of axioms is \forall a\forall b\;\lnot a=b\rightarrow \exists C\; aC\and bC (There is a line through any 2 distinct points a,b ...) \forall a\forall b\forall C\forall D\; \lnot a=b\and aC\and bC \and aD\and bD\rightarrow C=D (... which is unique) \forall a\forall b\forall c\forall d\forall e\forall G\forall H \;aH\and bH\and eH\and cG\and dG\and eG\rightarrow\exists f\exists I\exists J\; aI\and cI\and fI\and bJ\and dJ\and fJ (Veblen's axiom: if ab and cd lie on intersecting lines, then so do ac and bd.) \forall A\exists b\exists c\exists d\; bA\and cA\and dA\and \lnot b=c\and \lnot b=d\and \lnot c=d (Every line has at least 3 points) Euclid did not state all the axioms for Euclidean geometry explicitly, and the first complete list was given by Hilbert in Hilbert's axioms. This is not a first order axiomatization as one of Hilbert's axioms is a second order completeness axiom. Tarski's axioms are a first order axiomatization of Euclidean geometry. Tarski showed this axiom system is complete and decidable by relating it to the complete and decidable theory of real closed fields. |
About us|Jobs|Help|Disclaimer|Advertising services|Contact us|Sign in|Website map|Search|
GMT+8, 2015-9-11 22:04 , Processed in 0.371342 second(s), 16 queries .
