Natural deduction

From Wikipedia, the free encyclopedia

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

Motivation

Natural deduction grew out of a context of dissatisfaction with the axiomatizations of deductive reasoning common to the systems of Hilbert, Frege, and Russell (see, e.g., Hilbert system). Such axiomatizations were most famously used by Russell and Whitehead in their mathematical treatise Principia Mathematica. Spurred on by a series of seminars in Poland in 1926 by Łukasiewicz that advocated a more natural treatment of logic, Jaśkowski made the earliest attempts at defining a more natural deduction, first in 1929 using a diagrammatic notation, and later updating his proposal in a sequence of papers in 1934 and 1935. His proposals led to different notations such as Fitch-style calculus (or Fitch's diagrams) or Suppes' method of which e.g. Lemmon gave a variant called system L.

Natural deduction in its modern form was independently proposed by the German mathematician Gerhard Gentzen in 1934, in a dissertation delivered to the faculty of mathematical sciences of the University of Göttingen. The term natural deduction (or rather, its German equivalent natürliches Schließen) was coined in that paper:

Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens".

(First I wished to construct a formalism that comes as close as possible to actual reasoning. Thus arose a "calculus of natural deduction".)

Gentzen was motivated by a desire to establish the consistency of number theory. He was unable to prove the main result required for the consistency result, the cut elimination theorem—the Hauptsatz—directly for natural deduction. For this reason he introduced his alternative system, the sequent calculus, for which he proved the Hauptsatz both for classical and intuitionistic logic. In a series of seminars in 1961 and 1962 Prawitz gave a comprehensive summary of natural deduction calculi, and transported much of Gentzen's work with sequent calculi into the natural deduction framework. His 1965 monograph Natural deduction: a proof-theoretical study was to become a reference work on natural deduction, and included applications for modal and second-order logic.

In natural deduction, a proposition is deduced from a collection of premises by applying inference rules repeatedly. The system presented in this article is a minor variation of Gentzen's or Prawitz's formulation, but with a closer adherence to Martin-Löf's description of logical judgments and connectives.

Judgments and propositions

A judgment is something that is knowable, that is, an object of knowledge. It is evident if one in fact knows it. Thus "it is raining" is a judgment, which is evident for the one who knows that it is actually raining; in this case one may readily find evidence for the judgment by looking outside the window or stepping out of the house. In mathematical logic however, evidence is often not as directly observable, but rather deduced from more basic evident judgments. The process of deduction is what constitutes a proof; in other words, a judgment is evident if one has a proof for it.

The most important judgments in logic are of the form "A is true". The letter A stands for any expression representing a proposition; the truth judgments thus require a more primitive judgment: "A is a proposition". Many other judgments have been studied; for example, "A is false", "A is true at time t", "A is necessarily true" or "A is possibly true", "the program M has type τ", "A is achievable from the available resources", and many others. To start with, we shall concern ourselves with the simplest two judgments "A is a proposition" and "A is true", abbreviated as "A prop" and "A true" respectively.

The judgment "A prop" defines the structure of valid proofs of A, which in turn defines the structure of propositions. For this reason, the inference rules for this judgment are sometimes known as formation rules. To illustrate, if we have two propositions A and B (that is, the judgments "A prop" and "B prop" are evident), then we form the compound proposition A and B, written symbolically as "${\displaystyle A\wedge B}$". We can write this in the form of an inference rule:

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}\ \wedge _{F}}$

where the parentheses are omitted to make the inference rule more succinct:

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\wedge B{\hbox{ prop}}}}\ \wedge _{F}}$

This inference rule is schematic: A and B can be instantiated with any expression. The general form of an inference rule is:

${\displaystyle {\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}}$

where each ${\displaystyle J_{i}}$ is a judgment and the inference rule is named "name". The judgments above the line are known as premises, and those below the line are conclusions. Other common logical propositions are disjunction (${\displaystyle A\vee B}$), negation (${\displaystyle \neg A}$), implication (${\displaystyle A\supset B}$), and the logical constants truth (${\displaystyle \top }$) and falsehood (${\displaystyle \bot }$). Their formation rules are below.

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\vee B{\hbox{ prop}}}}\ \vee _{F}\qquad {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\supset B{\hbox{ prop}}}}\ \supset _{F}\qquad {\frac {\hbox{ }}{\top {\hbox{ prop}}}}\ \top _{F}\qquad {\frac {\hbox{ }}{\bot {\hbox{ prop}}}}\ \bot _{F}\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}}$

Introduction and elimination

Now we discuss the "A true" judgment. Inference rules that introduce a logical connective in the conclusion are known as introduction rules. To introduce conjunctions, i.e., to conclude "A and B true" for propositions A and B, one requires evidence for "A true" and "B true". As an inference rule:

${\displaystyle {\frac {A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}}$

It must be understood that in such rules the objects are propositions. That is, the above rule is really an abbreviation for:

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}}$

This can also be written:

${\displaystyle {\frac {A\wedge B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}}$

In this form, the first premise can be satisfied by the ${\displaystyle \wedge _{F}}$ formation rule, giving the first two premises of the previous form. In this article we shall elide the "prop" judgments where they are understood. In the nullary case, one can derive truth from no premises.

${\displaystyle {\frac {\ }{\top {\hbox{ true}}}}\ \top _{I}}$

If the truth of a proposition can be established in more than one way, the corresponding connective has multiple introduction rules.

${\displaystyle {\frac {A{\hbox{ true}}}{A\vee B{\hbox{ true}}}}\ \vee _{I1}\qquad {\frac {B{\hbox{ true}}}{A\vee B{\hbox{ true}}}}\ \vee _{I2}}$

Note that in the nullary case, i.e., for falsehood, there are no introduction rules. Thus one can never infer falsehood from simpler judgments.

Dual to introduction rules are elimination rules to describe how to deconstruct information about a compound proposition into information about its constituents. Thus, from "A ∧ B true", we can conclude "A true" and "B true":

${\displaystyle {\frac {A\wedge B{\hbox{ true}}}{A{\hbox{ true}}}}\ \wedge _{E1}\qquad {\frac {A\wedge B{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E2}}$

As an example of the use of inference rules, consider commutativity of conjunction. If A ∧ B is true, then B ∧ A is true; This derivation can be drawn by composing inference rules in such a fashion that premises of a lower inference match the conclusion of the next higher inference.

${\displaystyle {\cfrac {{\cfrac {A\wedge B{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E2}\qquad {\cfrac {A\wedge B{\hbox{ true}}}{A{\hbox{ true}}}}\ \wedge _{E1}}{B\wedge A{\hbox{ true}}}}\ \wedge _{I}}$

The inference figures we have seen so far are not sufficient to state the rules of implication introduction or disjunction elimination; for these, we need a more general notion of hypothetical derivation.

Hypothetical derivations

A pervasive operation in mathematical logic is reasoning from assumptions. For example, consider the following derivation:

${\displaystyle {\cfrac {A\wedge \left(B\wedge C\right){\hbox{ true}}}{{\cfrac {B\wedge C{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E1}}}\ \wedge _{E2}}$

This derivation does not establish the truth of B as such; rather, it establishes the following fact:

If A ∧ (B ∧ C) is true then B is true.

In logic, one says "assuming A ∧ (B ∧ C) is true, we show that B is true"; in other words, the judgment "B true" depends on the assumed judgment "A ∧ (B ∧ C) true". This is a hypothetical derivation, which we write as follows:

${\displaystyle {\begin{matrix}A\wedge \left(B\wedge C\right){\hbox{ true}}\\\vdots \\B{\hbox{ true}}\end{matrix}}}$

The interpretation is: "B true is derivable from A ∧ (B ∧ C) true". Of course, in this specific example we actually know the derivation of "B true" from "A ∧ (B ∧ C) true", but in general we may not a priori know the derivation. The general form of a hypothetical derivation is:

${\displaystyle {\begin{matrix}D_{1}\quad D_{2}\ \cdots \ D_{n}\\\vdots \\J\end{matrix}}}$

Each hypothetical derivation has a collection of antecedent derivations (the D_i) written on the top line, and a succedent judgment (J) written on the bottom line. Each of the premises may itself be a hypothetical derivation. (For simplicity, we treat a judgment as a premise-less derivation.)

The notion of hypothetical judgment is internalised as the connective of implication. The introduction and elimination rules are as follows.

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\B{\hbox{ true}}\end{matrix}}{A\supset B{\hbox{ true}}}}\ \supset _{I^{u}}\qquad {\cfrac {A\supset B{\hbox{ true}}\quad A{\hbox{ true}}}{B{\hbox{ true}}}}\ \supset _{E}}$

In the introduction rule, the antecedent named u is discharged in the conclusion. This is a mechanism for delimiting the scope of the hypothesis: its sole reason for existence is to establish "B true"; it cannot be used for any other purpose, and in particular, it cannot be used below the introduction. As an example, consider the derivation of "A ⊃ (B ⊃ (A ∧ B)) true":

${\displaystyle {\cfrac {{\cfrac {{\cfrac {}{A{\hbox{ true}}}}\ u\quad {\cfrac {}{B{\hbox{ true}}}}\ w}{A\wedge B{\hbox{ true}}}}\ \wedge _{I}}{{\cfrac {B\supset \left(A\wedge B\right){\hbox{ true}}}{A\supset \left(B\supset \left(A\wedge B\right)\right){\hbox{ true}}}}\ \supset _{I^{u}}}}\ \supset _{I^{w}}}$

This full derivation has no unsatisfied premises; however, sub-derivations are hypothetical. For instance, the derivation of "B ⊃ (A ∧ B) true" is hypothetical with antecedent "A true" (named u).
With hypothetical derivations, we can now write the elimination rule for disjunction:

${\displaystyle {\cfrac {A\vee B{\hbox{ true}}\quad {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\C{\hbox{ true}}\end{matrix}}\quad {\begin{matrix}{\cfrac {}{B{\hbox{ true}}}}\ w\\\vdots \\C{\hbox{ true}}\end{matrix}}}{C{\hbox{ true}}}}\ \vee _{E^{u,w}}}$

In words, if A ∨ B is true, and we can derive "C true" both from "A true" and from "B true", then C is indeed true. Note that this rule does not commit to either "A true" or "B true". In the zero-ary case, i.e. for falsehood, we obtain the following elimination rule:

${\displaystyle {\frac {\perp {\hbox{ true}}}{C{\hbox{ true}}}}\ \perp _{E}}$

This is read as: if falsehood is true, then any proposition C is true.

Negation is similar to implication.

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\p{\hbox{ true}}\end{matrix}}{\lnot A{\hbox{ true}}}}\ \lnot _{I^{u,p}}\qquad {\cfrac {\lnot A{\hbox{ true}}\quad A{\hbox{ true}}}{C{\hbox{ true}}}}\ \lnot _{E}}$

The introduction rule discharges both the name of the hypothesis u, and the succedent p, i.e., the proposition p must not occur in the conclusion A. Since these rules are schematic, the interpretation of the introduction rule is: if from "A true" we can derive for every proposition p that "p true", then A must be false, i.e., "not A true". For the elimination, if both A and not A are shown to be true, then there is a contradiction, in which case every proposition C is true. Because the rules for implication and negation are so similar, it should be fairly easy to see that not A and A ⊃ ⊥ are equivalent, i.e., each is derivable from the other.

Consistency, completeness, and normal forms

A theory is said to be consistent if falsehood is not provable (from no assumptions) and is complete if every theorem or its negation is provable using the inference rules of the logic. These are statements about the entire logic, and are usually tied to some notion of a model. However, there are local notions of consistency and completeness that are purely syntactic checks on the inference rules, and require no appeals to models. The first of these is local consistency, also known as local reducibility, which says that any derivation containing an introduction of a connective followed immediately by its elimination can be turned into an equivalent derivation without this detour. It is a check on the strength of elimination rules: they must not be so strong that they include knowledge not already contained in their premises. As an example, consider conjunctions.

────── u ────── w A true B true ────────────────── ∧I A ∧ B true ────────── ∧E1 A true

⇒

────── u A true

Dually, local completeness says that the elimination rules are strong enough to decompose a connective into the forms suitable for its introduction rule. Again for conjunctions:

────────── u A ∧ B true

⇒

────────── u ────────── u A ∧ B true A ∧ B true ────────── ∧E1 ────────── ∧E2 A true B true ─────────────────────── ∧I A ∧ B true

These notions correspond exactly to β-reduction (beta reduction) and η-conversion (eta conversion) in the lambda calculus, using the Curry–Howard isomorphism. By local completeness, we see that every derivation can be converted to an equivalent derivation where the principal connective is introduced. In fact, if the entire derivation obeys this ordering of eliminations followed by introductions, then it is said to be normal. In a normal derivation all eliminations happen above introductions. In most logics, every derivation has an equivalent normal derivation, called a normal form. The existence of normal forms is generally hard to prove using natural deduction alone, though such accounts do exist in the literature, most notably by Dag Prawitz in 1961. It is much easier to show this indirectly by means of a cut-free sequent calculus presentation.

First and higher-order extensions

Summary of first-order system

The logic of the earlier section is an example of a single-sorted logic, i.e., a logic with a single kind of object: propositions. Many extensions of this simple framework have been proposed; in this section we will extend it with a second sort of individuals or terms. More precisely, we will add a new kind of judgment, "t is a term" (or "t term") where t is schematic. We shall fix a countable set V of variables, another countable set F of function symbols, and construct terms as follows:

v ∈ V ────── var-F v term

f ∈ F t1 term t2 term ... tn term ────────────────────────────────────────── app-F f (t1, t2, ..., tn) term

For propositions, we consider a third countable set P of predicates, and define atomic predicates over terms with the following formation rule:

φ ∈ P t1 term t2 term ... tn term ────────────────────────────────────────── pred-F φ (t1, t2, ..., tn) prop

In addition, we add a pair of quantified propositions: universal (∀) and existential (∃):

x ∈ V A prop ───────────────── ∀Fu ∀x. A prop

x ∈ V A prop ───────────────── ∃Fu ∃x. A prop

These quantified propositions have the following introduction and elimination rules.

────── u a term ⋮ [a/x] A true ──────────── ∀Iu, a ∀x. A true		∀x. A true t term ──────────────────── ∀E [t/x] A true
[t/x] A true ──────────── ∃I ∃x. A true		────── u ──────────── v a term [a/x] A true ⋮ ∃x. A true C true ────────────────────────── ∃Ea, u,v C true

In these rules, the notation [t/x] A stands for the substitution of t for every (visible) instance of x in A, avoiding capture; see the article on lambda calculus for more detail about this standard operation. As before the superscripts on the name stand for the components that are discharged: the term a cannot occur in the conclusion of ∀I (such terms are known as eigenvariables or parameters), and the hypotheses named u and v in ∃E are localised to the second premise in a hypothetical derivation. Although the propositional logic of earlier sections was decidable, adding the quantifiers makes the logic undecidable.

So far the quantified extensions are first-order: they distinguish propositions from the kinds of objects quantified over. Higher-order logic takes a different approach and has only a single sort of propositions. The quantifiers have as the domain of quantification the very same sort of propositions, as reflected in the formation rules:

────── u p prop ⋮ A prop ────────── ∀Fu ∀p. A prop

────── u p prop ⋮ A prop ────────── ∃Fu ∃p. A prop

A discussion of the introduction and elimination forms for higher-order logic is beyond the scope of this article. It is possible to be in-between first-order and higher-order logics. For example, second-order logic has two kinds of propositions, one kind quantifying over terms, and the second kind quantifying over propositions of the first kind.

Different presentations of natural deduction

Tree-like presentations

Gentzen's discharging annotations used to internalise hypothetical judgments can be avoided by representing proofs as a tree of sequents Γ ⊢A instead of a tree of A true judgments.

Sequential presentations

Jaśkowski's representations of natural deduction led to different notations such as Fitch-style calculus (or Fitch's diagrams) or Suppes' method, of which Lemmon gave a variant called system L. Such presentation systems, which are more accurately described as tabular, include the following.

• 1940: In a textbook, Quine indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
• 1950: In a textbook, Quine (1982, pp. 241–255) demonstrated a method of using one or more asterisks to the left of each line of proof to indicate dependencies. This is equivalent to Kleene's vertical bars. (It is not totally clear if Quine's asterisk notation appeared in the original 1950 edition or was added in a later edition.)
• 1957: An introduction to practical logic theorem proving in a textbook by Suppes (1999, pp. 25–150). This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line.
• 1963: Stoll (1979, pp. 183–190, 215–219) uses sets of line numbers to indicate antecedent dependencies of the lines of sequential logical arguments based on natural deduction inference rules.
• 1965: The entire textbook by Lemmon (1965) is an introduction to logic proofs using a method based on that of Suppes.
• 1967: In a textbook, Kleene (2002, pp. 50–58, 128–130) briefly demonstrated two kinds of practical logic proofs, one system using explicit quotations of antecedent propositions on the left of each line, the other system using vertical bar-lines on the left to indicate dependencies.

Proofs and type theory

The presentation of natural deduction so far has concentrated on the nature of propositions without giving a formal definition of a proof. To formalise the notion of proof, we alter the presentation of hypothetical derivations slightly. We label the antecedents with proof variables (from some countable set V of variables), and decorate the succedent with the actual proof. The antecedents or hypotheses are separated from the succedent by means of a turnstile (⊢). This modification sometimes goes under the name of localised hypotheses. The following diagram summarises the change.

──── u1 ──── u2 ... ──── un J1 J2 Jn ⋮ J

⇒

u1:J1, u2:J2, ..., un:Jn ⊢ J

The collection of hypotheses will be written as Γ when their exact composition is not relevant. To make proofs explicit, we move from the proof-less judgment "A true" to a judgment: "π is a proof of (A true)", which is written symbolically as "π : A true". Following the standard approach, proofs are specified with their own formation rules for the judgment "π proof". The simplest possible proof is the use of a labelled hypothesis; in this case the evidence is the label itself.

u ∈ V ─────── proof-F u proof

───────────────────── hyp u:A true ⊢ u : A true

For brevity, we shall leave off the judgmental label true in the rest of this article, i.e., write "Γ ⊢ π : A". Let us re-examine some of the connectives with explicit proofs. For conjunction, we look at the introduction rule ∧I to discover the form of proofs of conjunction: they must be a pair of proofs of the two conjuncts. Thus:

π1 proof π2 proof ──────────────────── pair-F (π1, π2) proof

Γ ⊢ π1 : A Γ ⊢ π2 : B ------------------------ ∧I Γ ⊢ (π1, π2) : A ∧ B

The elimination rules ∧E₁ and ∧E₂ select either the left or the right conjunct; thus the proofs are a pair of projections—first (fst) and second (snd).

π proof ─────────── fst-F fst π proof		Γ ⊢ π : A ∧ B ───────────── ∧E1 Γ ⊢ fst π : A
π proof ─────────── snd-F snd π proof		Γ ⊢ π : A ∧ B ───────────── ∧E2 Γ ⊢ snd π : B

For implication, the introduction form localises or binds the hypothesis, written using a λ; this corresponds to the discharged label. In the rule, "Γ, u:A" stands for the collection of hypotheses Γ, together with the additional hypothesis u.

π proof ──────────── λ-F λu. π proof		Γ, u:A ⊢ π : B ───────────────── ⊃I Γ ⊢ λu. π : A ⊃ B
π1 proof π2 proof ─────────────────── app-F π1 π2 proof		Γ ⊢ π1 : A ⊃ B Γ ⊢ π2 : A ──────────────────────────── ⊃E Γ ⊢ π1 π2 : B

With proofs available explicitly, one can manipulate and reason about proofs. The key operation on proofs is the substitution of one proof for an assumption used in another proof. This is commonly known as a substitution theorem, and can be proved by induction on the depth (or structure) of the second judgment.

Substitution theorem

 

If  Γ ⊢ π₁ : A and Γ, u:A ⊢ π₂ : B, then Γ ⊢ [π₁/u] π₂ : B.

So far the judgment "Γ ⊢ π : A" has had a purely logical interpretation. In type theory, the logical view is exchanged for a more computational view of objects. Propositions in the logical interpretation are now viewed as types, and proofs as programs in the lambda calculus. Thus the interpretation of "π : A" is "the program π has type A". The logical connectives are also given a different reading: conjunction is viewed as product (×), implication as the function arrow (→), etc. The differences are only cosmetic, however. Type theory has a natural deduction presentation in terms of formation, introduction and elimination rules; in fact, the reader can easily reconstruct what is known as simple type theory from the previous sections.

The difference between logic and type theory is primarily a shift of focus from the types (propositions) to the programs (proofs). Type theory is chiefly interested in the convertibility or reducibility of programs. For every type, there are canonical programs of that type which are irreducible; these are known as canonical forms or values. If every program can be reduced to a canonical form, then the type theory is said to be normalising (or weakly normalising). If the canonical form is unique, then the theory is said to be strongly normalising. Normalisability is a rare feature of most non-trivial type theories, which is a big departure from the logical world. (Recall that almost every logical derivation has an equivalent normal derivation.) To sketch the reason: in type theories that admit recursive definitions, it is possible to write programs that never reduce to a value; such looping programs can generally be given any type. In particular, the looping program has type ⊥, although there is no logical proof of "⊥ true". For this reason, the propositions as types; proofs as programs paradigm only works in one direction, if at all: interpreting a type theory as a logic generally gives an inconsistent logic.

Example: Dependent Type Theory

Like logic, type theory has many extensions and variants, including first-order and higher-order versions. One branch, known as dependent type theory, is used in a number of computer-assisted proof systems. Dependent type theory allows quantifiers to range over programs themselves. These quantified types are written as Π and Σ instead of ∀ and ∃, and have the following formation rules:

Γ ⊢ A type Γ, x:A ⊢ B type ───────────────────────────── Π-F Γ ⊢ Πx:A. B type

Γ ⊢ A type Γ, x:A ⊢ B type ──────────────────────────── Σ-F Γ ⊢ Σx:A. B type

These types are generalisations of the arrow and product types, respectively, as witnessed by their introduction and elimination rules.

Γ, x:A ⊢ π : B ──────────────────── ΠI Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π1 : Πx:A. B Γ ⊢ π2 : A ───────────────────────────── ΠE Γ ⊢ π1 π2 : [π2/x] B

Γ ⊢ π1 : A Γ, x:A ⊢ π2 : B ───────────────────────────── ΣI Γ ⊢ (π1, π2) : Σx:A. B

Γ ⊢ π : Σx:A. B ──────────────── ΣE1 Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B ──────────────────────── ΣE2 Γ ⊢ snd π : [fst π/x] B

Dependent type theory in full generality is very powerful: it is able to express almost any conceivable property of programs directly in the types of the program. This generality comes at a steep price — either typechecking is undecidable (extensional type theory), or extensional reasoning is more difficult (intensional type theory). For this reason, some dependent type theories do not allow quantification over arbitrary programs, but rather restrict to programs of a given decidable index domain, for example integers, strings, or linear programs.

Since dependent type theories allow types to depend on programs, a natural question to ask is whether it is possible for programs to depend on types, or any other combination. There are many kinds of answers to such questions. A popular approach in type theory is to allow programs to be quantified over types, also known as parametric polymorphism; of this there are two main kinds: if types and programs are kept separate, then one obtains a somewhat more well-behaved system called predicative polymorphism; if the distinction between program and type is blurred, one obtains the type-theoretic analogue of higher-order logic, also known as impredicative polymorphism. Various combinations of dependency and polymorphism have been considered in the literature, the most famous being the lambda cube of Henk Barendregt.

The intersection of logic and type theory is a vast and active research area. New logics are usually formalised in a general type theoretic setting, known as a logical framework. Popular modern logical frameworks such as the calculus of constructions and LF are based on higher-order dependent type theory, with various trade-offs in terms of decidability and expressive power. These logical frameworks are themselves always specified as natural deduction systems, which is a testament to the versatility of the natural deduction approach.

Classical and modal logics

For simplicity, the logics presented so far have been intuitionistic. Classical logic extends intuitionistic logic with an additional axiom or principle of excluded middle:

For any proposition p, the proposition p ∨ ¬p is true.

This statement is not obviously either an introduction or an elimination; indeed, it involves two distinct connectives. Gentzen's original treatment of excluded middle prescribed one of the following three (equivalent) formulations, which were already present in analogous forms in the systems of Hilbert and Heyting:

────────────── XM1 A ∨ ¬A true

¬¬A true ────────── XM2 A true

──────── u ¬A true ⋮ p true ────── XM3u, p A true

(XM₃ is merely XM₂ expressed in terms of E.) This treatment of excluded middle, in addition to being objectionable from a purist's standpoint, introduces additional complications in the definition of normal forms.

A comparatively more satisfactory treatment of classical natural deduction in terms of introduction and elimination rules alone was first proposed by Parigot in 1992 in the form of a classical lambda calculus called λμ. The key insight of his approach was to replace a truth-centric judgment A true with a more classical notion, reminiscent of the sequent calculus: in localised form, instead of Γ ⊢ A, he used Γ ⊢ Δ, with Δ a collection of propositions similar to Γ. Γ was treated as a conjunction, and Δ as a disjunction. This structure is essentially lifted directly from classical sequent calculi, but the innovation in λμ was to give a computational meaning to classical natural deduction proofs in terms of a callcc or a throw/catch mechanism seen in LISP and its descendants. (See also: first class control.)

Another important extension was for modal and other logics that need more than just the basic judgment of truth. These were first described, for the alethic modal logics S4 and S5, in a natural deduction style by Prawitz in 1965,^[4] and have since accumulated a large body of related work. To give a simple example, the modal logic S4 requires one new judgment, "A valid", that is categorical with respect to truth:

If "A true" under no assumptions of the form "B true", then "A valid".

This categorical judgment is internalised as a unary connective ◻A (read "necessarily A") with the following introduction and elimination rules:

A valid ──────── ◻I ◻ A true

◻ A true ──────── ◻E A true

Note that the premise "A valid" has no defining rules; instead, the categorical definition of validity is used in its place. This mode becomes clearer in the localised form when the hypotheses are explicit. We write "Ω;Γ ⊢ A true" where Γ contains the true hypotheses as before, and Ω contains valid hypotheses. On the right there is just a single judgment "A true"; validity is not needed here since "Ω ⊢ A valid" is by definition the same as "Ω;⋅ ⊢ A true". The introduction and elimination forms are then:

Ω;⋅ ⊢ π : A true ──────────────────── ◻I Ω;⋅ ⊢ box π : ◻ A true

Ω;Γ ⊢ π : ◻ A true ────────────────────── ◻E Ω;Γ ⊢ unbox π : A true

The modal hypotheses have their own version of the hypothesis rule and substitution theorem.

─────────────────────────────── valid-hyp Ω, u: (A valid) ; Γ ⊢ u : A true

Modal substitution theorem 

 

If Ω;⋅ ⊢ π₁ : A true and Ω, u: (A valid) ; Γ ⊢ π₂ : C true, then Ω;Γ ⊢ [π₁/u] π₂ : C true.

This framework of separating judgments into distinct collections of hypotheses, also known as multi-zoned or polyadic contexts, is very powerful and extensible; it has been applied for many different modal logics, and also for linear and other substructural logics, to give a few examples. However, relatively few systems of modal logic can be formalised directly in natural deduction. To give proof-theoretic characterisations of these systems, extensions such as labelling or systems of deep inference.

The addition of labels to formulae permits much finer control of the conditions under which rules apply, allowing the more flexible techniques of analytic tableaux to be applied, as has been done in the case of labelled deduction. Labels also allow the naming of worlds in Kripke semantics; Simpson (1993) presents an influential technique for converting frame conditions of modal logics in Kripke semantics into inference rules in a natural deduction formalisation of hybrid logic. Stouppa (2004) surveys the application of many proof theories, such as Avron and Pottinger's hypersequents and Belnap's display logic to such modal logics as S5 and B.

Comparison with other foundational approaches

Sequent calculus

The sequent calculus is the chief alternative to natural deduction as a foundation of mathematical logic. In natural deduction the flow of information is bi-directional: elimination rules flow information downwards by deconstruction, and introduction rules flow information upwards by assembly. Thus, a natural deduction proof does not have a purely bottom-up or top-down reading, making it unsuitable for automation in proof search. To address this fact, Gentzen in 1935 proposed his sequent calculus, though he initially intended it as a technical device for clarifying the consistency of predicate logic. Kleene, in his seminal 1952 book Introduction to Metamathematics, gave the first formulation of the sequent calculus in the modern style.

In the sequent calculus all inference rules have a purely bottom-up reading. Inference rules can apply to elements on both sides of the turnstile. (To differentiate from natural deduction, this article uses a double arrow ⇒ instead of the right tack ⊢ for sequents.) The introduction rules of natural deduction are viewed as right rules in the sequent calculus, and are structurally very similar. The elimination rules on the other hand turn into left rules in the sequent calculus. To give an example, consider disjunction; the right rules are familiar:

Γ ⇒ A ───────── ∨R1 Γ ⇒ A ∨ B

Γ ⇒ B ───────── ∨R2 Γ ⇒ A ∨ B

On the left:

Γ, u:A ⇒ C Γ, v:B ⇒ C ─────────────────────────── ∨L Γ, w: (A ∨ B) ⇒ C

Recall the ∨E rule of natural deduction in localised form:

Γ ⊢ A ∨ B Γ, u:A ⊢ C Γ, v:B ⊢ C ─────────────────────────────────────── ∨E Γ ⊢ C

The proposition A ∨ B, which is the succedent of a premise in ∨E, turns into a hypothesis of the conclusion in the left rule ∨L. Thus, left rules can be seen as a sort of inverted elimination rule. This observation can be illustrated as follows:

natural deduction		sequent calculus
────── hyp | | elim. rules | ↓ ────────────────────── ↑↓ meet ↑ | | intro. rules | conclusion	⇒	─────────────────────────── init ↑ ↑ | | | left rules | right rules | | conclusion

In the sequent calculus, the left and right rules are performed in lock-step until one reaches the initial sequent, which corresponds to the meeting point of elimination and introduction rules in natural deduction. These initial rules are superficially similar to the hypothesis rule of natural deduction, but in the sequent calculus they describe a transposition or a handshake of a left and a right proposition:

────────── init Γ, u:A ⇒ A

The correspondence between the sequent calculus and natural deduction is a pair of soundness and completeness theorems, which are both provable by means of an inductive argument.

Soundness of ⇒ wrt. ⊢ 

 

If Γ ⇒ A, then Γ ⊢ A.

 

Completeness of ⇒ wrt. ⊢ 

 

If Γ ⊢ A, then Γ ⇒ A.

It is clear by these theorems that the sequent calculus does not change the notion of truth, because the same collection of propositions remain true. Thus, one can use the same proof objects as before in sequent calculus derivations. As an example, consider the conjunctions. The right rule is virtually identical to the introduction rule

sequent calculus		natural deduction
Γ ⇒ π1 : A Γ ⇒ π2 : B ─────────────────────────── ∧R Γ ⇒ (π1, π2) : A ∧ B		Γ ⊢ π1 : A Γ ⊢ π2 : B ───────────────────────── ∧I Γ ⊢ (π1, π2) : A ∧ B

The left rule, however, performs some additional substitutions that are not performed in the corresponding elimination rules.

sequent calculus		natural deduction
Γ, v: (A ∧ B), u:A ⇒ π : C ──────────────────────────────── ∧L1 Γ, v: (A ∧ B) ⇒ [fst v/u] π : C		Γ ⊢ π : A ∧ B ───────────── ∧E1 Γ ⊢ fst π : A
Γ, v: (A ∧ B), u:B ⇒ π : C ──────────────────────────────── ∧L2 Γ, v: (A ∧ B) ⇒ [snd v/u] π : C		Γ ⊢ π : A ∧ B ───────────── ∧E2 Γ ⊢ snd π : B

The kinds of proofs generated in the sequent calculus are therefore rather different from those of natural deduction. The sequent calculus produces proofs in what is known as the β-normal η-long form, which corresponds to a canonical representation of the normal form of the natural deduction proof. If one attempts to describe these proofs using natural deduction itself, one obtains what is called the intercalation calculus (first described by John Byrnes), which can be used to formally define the notion of a normal form for natural deduction.

The substitution theorem of natural deduction takes the form of a structural rule or structural theorem known as cut in the sequent calculus.

Cut (substitution) 

 

If Γ ⇒ π₁ : A and Γ, u:A ⇒ π₂ : C, then Γ ⇒ [π₁/u] π₂ : C.

In most well behaved logics, cut is unnecessary as an inference rule, though it remains provable as a meta-theorem; the superfluousness of the cut rule is usually presented as a computational process, known as cut elimination. This has an interesting application for natural deduction; usually it is extremely tedious to prove certain properties directly in natural deduction because of an unbounded number of cases. For example, consider showing that a given proposition is not provable in natural deduction. A simple inductive argument fails because of rules like ∨E or E which can introduce arbitrary propositions. However, we know that the sequent calculus is complete with respect to natural deduction, so it is enough to show this unprovability in the sequent calculus. Now, if cut is not available as an inference rule, then all sequent rules either introduce a connective on the right or the left, so the depth of a sequent derivation is fully bounded by the connectives in the final conclusion. Thus, showing unprovability is much easier, because there are only a finite number of cases to consider, and each case is composed entirely of sub-propositions of the conclusion. A simple instance of this is the global consistency theorem: "⋅ ⊢ ⊥ true" is not provable. In the sequent calculus version, this is manifestly true because there is no rule that can have "⋅ ⇒ ⊥" as a conclusion! Proof theorists often prefer to work on cut-free sequent calculus formulations because of such properties.

Foundations of geometry

From Wikipedia, the free encyclopedia

Foundations of geometry is the study of geometries as axiomatic systems. There are several sets of axioms which give rise to Euclidean geometry or to non-Euclidean geometries. These are fundamental to the study and of historical importance, but there are a great many modern geometries that are not Euclidean which can be studied from this viewpoint. The term axiomatic geometry can be applied to any geometry that is developed from an axiom system, but is often used to mean Euclidean geometry studied from this point of view. The completeness and independence of general axiomatic systems are important mathematical considerations, but there are also issues to do with the teaching of geometry which come into play.

Axiomatic systems

Based on ancient Greek methods, an axiomatic system is a formal description of a way to establish the mathematical truth that flows from a fixed set of assumptions. Although applicable to any area of mathematics, geometry is the branch of elementary mathematics in which this method has most extensively been successfully applied.

There are several components of an axiomatic system.

1. Primitives (undefined terms) are the most basic ideas. Typically they include objects and relationships. In geometry, the objects are things like points, lines and planes while a fundamental relationship is that of incidence – of one object meeting or joining with another. The terms themselves are undefined. Hilbert once remarked that instead of points, lines and planes one might just as well talk of tables, chairs and beer mugs. His point being that the primitive terms are just empty shells, place holders if you will, and have no intrinsic properties.
2. Axioms (or postulates) are statements about these primitives; for example, any two points are together incident with just one line (i.e. that for any two points, there is just one line which passes through both of them). Axioms are assumed true, and not proven. They are the building blocks of geometric concepts, since they specify the properties that the primitives have.
3. The laws of logic.
4. The theorems are the logical consequences of the axioms, that is, the statements that can be obtained from the axioms by using the laws of deductive logic.

An interpretation of an axiomatic system is some particular way of giving concrete meaning to the primitives of that system. If this association of meanings makes the axioms of the system true statements, then the interpretation is called a model of the system. In a model, all the theorems of the system are automatically true statements.

Properties of axiomatic systems

In discussing axiomatic systems several properties are often focused on:

• The axioms of an axiomatic system are said to be consistent if no logical contradiction can be derived from them. Except in the simplest systems, consistency is a difficult property to establish in an axiomatic system. On the other hand, if a model exists for the axiomatic system, then any contradiction derivable in the system is also derivable in the model, and the axiomatic system is as consistent as any system in which the model belongs. This property (having a model) is referred to as relative consistency or model consistency.
• An axiom is called independent if it can not be proved or disproved from the other axioms of the axiomatic system. An axiomatic system is said to be independent if each of its axioms is independent. If a true statement is a logical consequence of an axiomatic system, then it will be a true statement in every model of that system. To prove that an axiom is independent of the remaining axioms of the system, it is sufficient to find two models of the remaining axioms, for which the axiom is a true statement in one and a false statement in the other. Independence is not always a desirable property from a pedagogical viewpoint.
• An axiomatic system is called complete if every statement expressible in the terms of the system is either provable or has a provable negation. Another way to state this is that no independent statement can be added to a complete axiomatic system which is consistent with axioms of that system.
• An axiomatic system is categorical if any two models of the system are isomorphic (essentially, there is only one model for the system). A categorical system is necessarily complete, but completeness does not imply categoricity. In some situations categoricity is not a desirable property, since categorical axiomatic systems can not be generalized. For instance, the value of the axiomatic system for group theory is that it is not categorical, so proving a result in group theory means that the result is valid in all the different models for group theory and one doesn't have to reprove the result in each of the non-isomorphic models.

Euclidean geometry

Euclidean geometry is a mathematical system attributed to the Alexandrian Greek mathematician Euclid, which he described (although non-rigorously by modern standards) in his textbook on geometry: the Elements. Euclid's method consists in assuming a small set of intuitively appealing axioms, and deducing many other propositions (theorems) from these. Although many of Euclid's results had been stated by earlier mathematicians, Euclid was the first to show how these propositions could fit into a comprehensive deductive and logical system. The Elements begins with plane geometry, still taught in secondary school as the first axiomatic system and the first examples of formal proof. It goes on to the solid geometry of three dimensions. Much of the Elements states results of what are now called algebra and number theory, explained in geometrical language.

For over two thousand years, the adjective "Euclidean" was unnecessary because no other sort of geometry had been conceived. Euclid's axioms seemed so intuitively obvious (with the possible exception of the parallel postulate) that any theorem proved from them was deemed true in an absolute, often metaphysical, sense. Today, however, many other geometries which are not Euclidean are known, the first ones having been discovered in the early 19th century.

Euclid's Elements

Euclid's Elements is a mathematical and geometric treatise consisting of 13 books written by the ancient Greek mathematician Euclid in Alexandria c. 300 BC. It is a collection of definitions, postulates (axioms), propositions (theorems and constructions), and mathematical proofs of the propositions. The thirteen books cover Euclidean geometry and the ancient Greek version of elementary number theory. With the exception of Autolycus' On the Moving Sphere, the Elements is one of the oldest extant Greek mathematical treatises, and it is the oldest extant axiomatic deductive treatment of mathematics. It has proven instrumental in the development of logic and modern science.

Euclid's Elements has been referred to as the most successful and influential textbook ever written. Being first set in type in Venice in 1482, it is one of the very earliest mathematical works to be printed after the invention of the printing press and was estimated by Carl Benjamin Boyer to be second only to the Bible in the number of editions published, with the number reaching well over one thousand. For centuries, when the quadrivium was included in the curriculum of all university students, knowledge of at least part of Euclid's Elements was required of all students. Not until the 20th century, by which time its content was universally taught through other school textbooks, did it cease to be considered something all educated people had read.

The Elements are mainly a systematization of earlier knowledge of geometry. It is assumed that its superiority over earlier treatments was recognized, with the consequence that there was little interest in preserving the earlier ones, and they are now nearly all lost.

Books I–IV and VI discuss plane geometry. Many results about plane figures are proved, e.g., If a triangle has two equal angles, then the sides subtended by the angles are equal. The Pythagorean theorem is proved.

Books V and VII–X deal with number theory, with numbers treated geometrically via their representation as line segments with various lengths. Notions such as prime numbers and rational and irrational numbers are introduced. The infinitude of prime numbers is proved.

Books XI–XIII concern solid geometry. A typical result is the 1:3 ratio between the volume of a cone and a cylinder with the same height and base.

The parallel postulate: If two lines intersect a third in such a way that the sum of the inner angles on one side is less than two right angles, then the two lines inevitably must intersect each other on that side if extended far enough.

Near the beginning of the first book of the Elements, Euclid gives five postulates (axioms) for plane geometry, stated in terms of constructions (as translated by Thomas Heath):

"Let the following be postulated":

1. "To draw a straight line from any point to any point."
2. "To produce [extend] a finite straight line continuously in a straight line."
3. "To describe a circle with any centre and distance [radius]."
4. "That all right angles are equal to one another."
5. The parallel postulate: "That, if a straight line falling on two straight lines make the interior angles on the same side less than two right angles, the two straight lines, if produced indefinitely, meet on that side on which are the angles less than the two right angles."

Although Euclid's statement of the postulates only explicitly asserts the existence of the constructions, they are also assumed to produce unique objects.

The success of the Elements is due primarily to its logical presentation of most of the mathematical knowledge available to Euclid. Much of the material is not original to him, although many of the proofs are supposedly his. Euclid's systematic development of his subject, from a small set of axioms to deep results, and the consistency of his approach throughout the Elements, encouraged its use as a textbook for about 2,000 years. The Elements still influences modern geometry books. Further, its logical axiomatic approach and rigorous proofs remain the cornerstone of mathematics.

A critique of Euclid

The standards of mathematical rigor have changed since Euclid wrote the Elements. Modern attitudes towards, and viewpoints of, an axiomatic system can make it appear that Euclid was in some way sloppy or careless in his approach to the subject, but this is an ahistorical illusion. It is only after the foundations were being carefully examined in response to the introduction of non-Euclidean geometry that what we now consider flaws began to emerge. Mathematician and historian W. W. Rouse Ball put these criticisms in perspective, remarking that "the fact that for two thousand years [the Elements] was the usual text-book on the subject raises a strong presumption that it is not unsuitable for that purpose."

Some of the main issues with Euclid's presentation are:

• Lack of recognition of the concept of primitive terms, objects and notions that must be left undefined in the development of an axiomatic system.
• The use of superposition in some proofs without there being an axiomatic justification of this method.
• Lack of a concept of continuity which is needed to prove the existence of some points and lines that Euclid constructs.
• Lack of clarity on whether a straight line is infinite or boundary-less in the second postulate.
• Lack of the concept of betweeness used, among other things, for distinguishing between the inside and outside of various figures.

Euclid's list of axioms in the Elements was not exhaustive, but represented the principles that seemed the most important. His proofs often invoke axiomatic notions which were not originally presented in his list of axioms. He does not go astray and prove erroneous things because of this since he is actually making use of implicit assumptions whose validity appears to be justified by the diagrams which accompany his proofs. Later mathematicians have incorporated Euclid's implicit axiomatic assumptions in the list of formal axioms, thereby greatly extending that list.

For example, in the first construction of Book 1, Euclid used a premise that was neither postulated nor proved: that two circles with centers at the distance of their radius will intersect in two points. Later, in the fourth construction, he used superposition (moving the triangles on top of each other) to prove that if two sides and their angles are equal then they are congruent; during these considerations he uses some properties of superposition, but these properties are not described explicitly in the treatise. If superposition is to be considered a valid method of geometric proof, all of geometry would be full of such proofs. For example, propositions I.1 – I.3 can be proved trivially by using superposition.

To address these issues in Euclid's work, later authors have either attempted to fill in the holes in Euclid's presentation–the most notable of these attempts is due to D. Hilbert–or to organize the axiom system around different concepts, as G.D. Birkhoff has done.

Pasch and Peano

The German mathematician Moritz Pasch (1843–1930) was the first to accomplish the task of putting Euclidean geometry on a firm axiomatic footing. In his book, Vorlesungen über neuere Geometrie published in 1882, Pasch laid the foundations of the modern axiomatic method. He originated the concept of primitive notion (which he called Kernbegriffe) and together with the axioms (Kernsätzen) he constructs a formal system which is free from any intuitive influences. According to Pasch, the only place where intuition should play a role is in deciding what the primitive notions and axioms should be. Thus, for Pasch, point is a primitive notion but line (straight line) is not, since we have good intuition about points but no one has ever seen or had experience with an infinite line. The primitive notion that Pasch uses in its place is line segment.

Pasch observed that the ordering of points on a line (or equivalently containment properties of line segments) is not properly resolved by Euclid's axioms; thus, Pasch's theorem, stating that if two line segment containment relations hold then a third one also holds, cannot be proven from Euclid's axioms. The related Pasch's axiom concerns the intersection properties of lines and triangles.

Pasch's work on the foundations set the standard for rigor, not only in geometry but also in the wider context of mathematics. His breakthrough ideas are now so commonplace that it is difficult to remember that they had a single originator. Pasch's work directly influenced many other mathematicians, in particular D. Hilbert and the Italian mathematician Giuseppe Peano (1858–1932). Peano's work, largely a translation of Pasch's treatise into the notation of symbolic logic (which Peano invented), uses the primitive notions of point and betweeness. Peano breaks the empirical tie in the choice of primitive notions and axioms that Pasch required. For Peano, the entire system is purely formal, divorced from any empirical input.

Pieri and the Italian school of geometers

The Italian mathematician Mario Pieri (1860–1913) took a different approach and considered a system in which there were only two primitive notions, that of point and of motion. Pasch had used four primitives and Peano had reduced this to three, but both of these approaches relied on some concept of betweeness which Pieri replaced by his formulation of motion. In 1905 Pieri gave the first axiomatic treatment of complex projective geometry which did not start by building real projective geometry.

Pieri was a member of a group of Italian geometers and logicians that Peano had gathered around himself in Turin. This group of assistants, junior colleagues and others were dedicated to carrying out Peano's logico–geometrical program of putting the foundations of geometry on firm axiomatic footing based on Peano's logical symbolism. Besides Pieri, Burali-Forti, Padoa and Fano were in this group. In 1900 there were two international conferences held back-to-back in Paris, the International Congress of Philosophy and the Second International Congress of Mathematicians. This group of Italian mathematicians was very much in evidence at these congresses, pushing their axiomatic agenda. Padoa gave a well regarded talk and Peano, in the question period after David Hilbert's famous address on unsolved problems, remarked that his colleagues had already solved Hilbert's second problem.

Hilbert's axioms

David Hilbert

At the University of Göttingen, during the 1898–1899 winter term, the eminent German mathematician David Hilbert (1862–1943) presented a course of lectures on the foundations of geometry. At the request of Felix Klein, Professor Hilbert was asked to write up the lecture notes for this course in time for the summer 1899 dedication ceremony of a monument to C.F. Gauss and Wilhelm Weber to be held at the university. The rearranged lectures were published in June 1899 under the title Grundlagen der Geometrie (Foundations of Geometry). The influence of the book was immediate. According to Eves (1963, pp. 384–5):

By developing a postulate set for Euclidean geometry that does not depart too greatly in spirit from Euclid's own, and by employing a minimum of symbolism, Hilbert succeeded in convincing mathematicians to a far greater extent than had Pasch and Peano, of the purely hypothetico-deductive nature of geometry. But the influence of Hilbert's work went far beyond this, for, backed by the author's great mathematical authority, it firmly implanted the postulational method, not only in the field of geometry, but also in essentially every other branch of mathematics. The stimulus to the development of the foundations of mathematics provided by Hilbert's little book is difficult to overestimate. Lacking the strange symbolism of the works of Pasch and Peano, Hilbert's work can be read, in great part, by any intelligent student of high school geometry.

It is difficult to specify the axioms used by Hilbert without referring to the publication history of the Grundlagen since Hilbert changed and modified them several times. The original monograph was quickly followed by a French translation, in which Hilbert added V.2, the Completeness Axiom. An English translation, authorized by Hilbert, was made by E.J. Townsend and copyrighted in 1902. This translation incorporated the changes made in the French translation and so is considered to be a translation of the 2nd edition. Hilbert continued to make changes in the text and several editions appeared in German. The 7th edition was the last to appear in Hilbert's lifetime. New editions followed the 7th, but the main text was essentially not revised. The modifications in these editions occur in the appendices and in supplements. The changes in the text were large when compared to the original and a new English translation was commissioned by Open Court Publishers, who had published the Townsend translation. So, the 2nd English Edition was translated by Leo Unger from the 10th German edition in 1971. This translation incorporates several revisions and enlargements of the later German editions by Paul Bernays. The differences between the two English translations are due not only to Hilbert, but also to differing choices made by the two translators. What follows will be based on the Unger translation.

Hilbert's axiom system is constructed with six primitive notions: point, line, plane, betweenness, lies on (containment), and congruence.

All points, lines, and planes in the following axioms are distinct unless otherwise stated.

I. Incidence

1. For every two points A and B there exists a line a that contains them both. We write AB = a or BA = a. Instead of “contains,” we may also employ other forms of expression; for example, we may say “A lies upon a”, “A is a point of a”, “a goes through A and through B”, “a joins A to B”, etc. If A lies upon a and at the same time upon another line b, we make use also of the expression: “The lines a and b have the point A in common,” etc.
2. For every two points there exists no more than one line that contains them both; consequently, if AB = a and AC = a, where B ≠ C, then also BC = a.
3. There exist at least two points on a line. There exist at least three points that do not lie on a line.
4. For every three points A, B, C not situated on the same line there exists a plane α that contains all of them. For every plane there exists a point which lies on it. We write ABC = α. We employ also the expressions: “A, B, C, lie in α”; “A, B, C are points of α”, etc.
5. For every three points A, B, C which do not lie in the same line, there exists no more than one plane that contains them all.
6. If two points A, B of a line a lie in a plane α, then every point of a lies in α. In this case we say: “The line a lies in the plane α,” etc.
7. If two planes α, β have a point A in common, then they have at least a second point B in common.
8. There exist at least four points not lying in a plane.

II. Order

1. If a point B lies between points A and C, B is also between C and A, and there exists a line containing the distinct points A,B,C.
2. If A and C are two points of a line, then there exists at least one point B lying between A and C.
3. Of any three points situated on a line, there is no more than one which lies between the other two.
4. Pasch's Axiom: Let A, B, C be three points not lying in the same line and let a be a line lying in the plane ABC and not passing through any of the points A, B, C. Then, if the line a passes through a point of the segment AB, it will also pass through either a point of the segment BC or a point of the segment AC.

III. Congruence

1. If A, B are two points on a line a, and if A′ is a point upon the same or another line a′ , then, upon a given side of A′ on the straight line a′ , we can always find a point B′ so that the segment AB is congruent to the segment A′B′ . We indicate this relation by writing AB ≅ A′ B′. Every segment is congruent to itself; that is, we always have AB ≅ AB.
   We can state the above axiom briefly by saying that every segment can be laid off upon a given side of a given point of a given straight line in at least one way.
2. If a segment AB is congruent to the segment A′B′ and also to the segment A″B″, then the segment A′B′ is congruent to the segment A″B″; that is, if AB ≅ A′B′ and AB ≅ A″B″, then A′B′ ≅ A″B″.
3. Let AB and BC be two segments of a line a which have no points in common aside from the point B, and, furthermore, let A′B′ and B′C′ be two segments of the same or of another line a′ having, likewise, no point other than B′ in common. Then, if AB ≅ A′B′ and BC ≅ B′C′, we have AC ≅ A′C′.
4. Let an angle ∠ (h,k) be given in the plane α and let a line a′ be given in a plane α′. Suppose also that, in the plane α′, a definite side of the straight line a′ be assigned. Denote by h′ a ray of the straight line a′ emanating from a point O′ of this line. Then in the plane α′ there is one and only one ray k′ such that the angle ∠ (h, k), or ∠ (k, h), is congruent to the angle ∠ (h′, k′) and at the same time all interior points of the angle ∠ (h′, k′) lie upon the given side of a′. We express this relation by means of the notation ∠ (h, k) ≅ ∠ (h′, k′).
5. If the angle ∠ (h, k) is congruent to the angle ∠ (h′, k′) and to the angle ∠ (h″, k″), then the angle ∠ (h′, k′) is congruent to the angle ∠ (h″, k″); that is to say, if ∠ (h, k) ≅ ∠ (h′, k′) and ∠ (h, k) ≅ ∠ (h″, k″), then ∠ (h′, k′) ≅ ∠ (h″, k″).

IV. Parallels

1. (Euclid's Axiom): Let a be any line and A a point not on it. Then there is at most one line in the plane, determined by a and A, that passes through A and does not intersect a.

V. Continuity

1. Axiom of Archimedes. If AB and CD are any segments then there exists a number n such that n segments CD constructed contiguously from A, along the ray from A through B, will pass beyond the point B.
2. Axiom of line completeness. An extension of a set of points on a line with its order and congruence relations that would preserve the relations existing among the original elements as well as the fundamental properties of line order and congruence that follows from Axioms I–III and from V-1 is impossible.

Changes in Hilbert's axioms

When the monograph of 1899 was translated into French, Hilbert added:

V.2 Axiom of completeness. To a system of points, straight lines, and planes, it is impossible to add other elements in such a manner that the system thus generalized shall form a new geometry obeying all of the five groups of axioms. In other words, the elements of geometry form a system which is not susceptible of extension, if we regard the five groups of axioms as valid.

This axiom is not needed for the development of Euclidean geometry, but is needed to establish a bijection between the real numbers and the points on a line. This was an essential ingredient in Hilbert's proof of the consistency of his axiom system.

By the 7th edition of the Grundlagen, this axiom had been replaced by the axiom of line completeness given above and the old axiom V.2 became Theorem 32.

Also to be found in the 1899 monograph (and appearing in the Townsend translation) is:

II.4. Any four points A, B, C, D of a line can always be labeled so that B shall lie between A and C and also between A and D, and, furthermore, that C shall lie between A and D and also between B and D.

However, E.H. Moore and R.L. Moore independently proved that this axiom is redundant, and the former published this result in an article appearing in the Transactions of the American Mathematical Society in 1902. Hilbert moved the axiom to Theorem 5 and renumbered the axioms accordingly (old axiom II-5 (Pasch's axiom) now became II-4).

While not as dramatic as these changes, most of the remaining axioms were also modified in form and/or function over the course of the first seven editions.

Consistency and Independence

Going beyond the establishment of a satisfactory set of axioms, Hilbert also proved the consistency of his system relative to the theory of real numbers by constructing a model of his axiom system from the real numbers. He proved the independence of some of his axioms by constructing models of geometries which satisfy all except the one axiom under consideration. Thus, there are examples of geometries satisfying all except the Archimedean axiom V.1 (non-Archimedean geometries), all except the parallel axiom IV.1 (non-Euclidean geometries) and so on. Using the same technique he also showed how some important theorems depended on certain axioms and were independent of others. Some of his models were very complex and other mathematicians tried to simplify them. For instance, Hilbert's model for showing the independence of Desargues theorem from certain axioms ultimately led Ray Moulton to discover the non-Desarguesian Moulton plane. These investigations by Hilbert virtually inaugurated the modern study of abstract geometry in the twentieth century.

Birkhoff's axioms

George David Birkhoff

In 1932, G. D. Birkhoff created a set of four postulates of Euclidean geometry sometimes referred to as Birkhoff's axioms. These postulates are all based on basic geometry that can be experimentally verified with a scale and protractor. In a radical departure from the synthetic approach of Hilbert, Birkhoff was the first to build the foundations of geometry on the real number system. It is this powerful assumption that permits the small number of axioms in this system.

Postulates

Birkhoff uses four undefined terms: point, line, distance and angle. His postulates are:

Postulate I: Postulate of Line Measure. The points A, B, ... of any line can be put into 1:1 correspondence with the real numbers x so that |x_B −x _A| = d(A, B) for all points A and B.

Postulate II: Point-Line Postulate. There is one and only one straight line, ℓ, that contains any two given distinct points P and Q.

Postulate III: Postulate of Angle Measure. The rays {ℓ, m, n, ...} through any point O can be put into 1:1 correspondence with the real numbers a (mod 2π) so that if A and B are points (not equal to O) of ℓ and m, respectively, the difference a_m − a_ℓ (mod 2π) of the numbers associated with the lines ℓ and m is ${\displaystyle \angle }$AOB. Furthermore, if the point B on m varies continuously in a line r not containing the vertex O, the number a_m varies continuously also.

Postulate IV: Postulate of Similarity. If in two triangles ABC and A'B'C'  and for some constant k > 0, d(A', B' ) = kd(A, B), d(A', C' ) = kd(A, C) and ${\displaystyle \angle }$B'A'C'  = ±${\displaystyle \angle }$BAC, then d(B', C' ) = kd(B, C), ${\displaystyle \angle }$ C'B'A'  = ±${\displaystyle \angle }$CBA, and ${\displaystyle \angle }$A'C'B'  = ±${\displaystyle \angle }$ACB.

School geometry

George Bruce Halsted

Whether or not it is wise to teach Euclidean geometry from an axiomatic viewpoint at the high school level has been a matter of debate. There have been many attempts to do so and not all of them have been successful. In 1904, George Bruce Halsted published a high school geometry text based on Hilbert's axiom set. Logical criticisms of this text led to a highly revised second edition. In reaction to the launching of the Russian satellite Sputnik there was a call to revise the school mathematics curriculum. From this effort there arose the New Math program of the 1960s. With this as a background, many individuals and groups set about to provide textual material for geometry classes based on an axiomatic approach.

Mac Lane's axioms

Saunders Mac Lane

Saunders Mac Lane (1909–2005), a mathematician, wrote a paper in 1959 in which he proposed a set of axioms for Euclidean geometry in the spirit of Birkhoff's treatment using a distance function to associate real numbers with line segments. This was not the first attempt to base a school level treatment on Birkhoff's system, in fact, Birkhoff and Ralph Beatley had written a high school text in 1940 which developed Euclidean geometry from five axioms and the ability to measure line segments and angles. However, in order to gear the treatment to a high school audience, some mathematical and logical arguments were either ignored or slurred over.

In Mac Lane's system there are four primitive notions (undefined terms): point, distance, line and angle measure. There are also 14 axioms, four giving the properties of the distance function, four describing properties of lines, four discussing angles (which are directed angles in this treatment), a similarity axiom (essentially the same as Birkhoff's) and a continuity axiom which can be used to derive the Crossbar theorem and its converse. The increased number of axioms has the pedagogical advantage of making early proofs in the development easier to follow and the use of a familiar metric permits a rapid advancement through basic material so that the more "interesting" aspects of the subject can be gotten to sooner.

SMSG (School Mathematics Study Group) axioms

In the 1960s a new set of axioms for Euclidean geometry, suitable for high school geometry courses, was introduced by the School Mathematics Study Group (SMSG), as a part of the New math curricula. This set of axioms follows the Birkhoff model of using the real numbers to gain quick entry into the geometric fundamentals. However, whereas Birkhoff tried to minimize the number of axioms used, and most authors were concerned with the independence of the axioms in their treatments, the SMSG axiom list was intentionally made large and redundant for pedagogical reasons. The SMSG only produced a mimeographed text using these axioms, but Edwin E. Moise, a member of the SMSG, wrote a high school text based on this system, and a college level text, Moise (1974), with some of the redundancy removed and modifications made to the axioms for a more sophisticated audience.

There are eight undefined terms: point, line, plane, lie on, distance, angle measure, area and volume. The 22 axioms of this system are given individual names for ease of reference. Amongst these are to be found: the Ruler Postulate, the Ruler Placement Postulate, the Plane Separation Postulate, the Angle Addition Postulate, the Side angle side (SAS) Postulate, the Parallel Postulate (in Playfair's form), and Cavalieri's principle.

UCSMP (University of Chicago School Mathematics Project) axioms

Although much of the New math curriculum has been drastically modified or abandoned, the geometry portion has remained relatively stable. Modern high school textbooks use axiom systems that are very similar to those of the SMSG. For example, the texts produced by the University of Chicago School Mathematics Project (UCSMP) use a system which, besides some updating of language, differs mainly from the SMSG system in that it includes some transformation concepts under its "Reflection Postulate".

There are only three undefined terms: point, line and plane. There are eight "postulates", but most of these have several parts (which are generally called assumptions in this system). Counting these parts, there are 32 axioms in this system. Amongst the postulates can be found the point-line-plane postulate, the Triangle inequality postulate, postulates for distance, angle measurement, corresponding angles, area and volume, and the Reflection postulate. The reflection postulate is used as a replacement for the SAS postulate of SMSG system.

Other systems

Oswald Veblen (1880 – 1960) provided a new axiom system in 1904 when he replaced the concept of "betweeness", as used by Hilbert and Pasch, with a new primitive, order. This permitted several primitive terms used by Hilbert to become defined entities, reducing the number of primitive notions to two, point and order.

Many other axiomatic systems for Euclidean geometry have been proposed over the years. A comparison of many of these can be found in a 1927 monograph by Henry George Forder. Forder also gives, by combining axioms from different systems, his own treatment based on the two primitive notions of point and order. He also provides a more abstract treatment of one of Pieri's systems (from 1909) based on the primitives point and congruence.

Starting with Peano, there has been a parallel thread of interest amongst logicians concerning the axiomatic foundations of Euclidean geometry. This can be seen, in part, in the notation used to describe the axioms. Pieri claimed that even though he wrote in the traditional language of geometry, he was always thinking in terms of the logical notation introduced by Peano, and used that formalism to see how to prove things. A typical example of this type of notation can be found in the work of E. V. Huntington (1874 – 1952) who, in 1913, produced an axiomatic treatment of three-dimensional Euclidean geometry based upon the primitive notions of sphere and inclusion (one sphere lying within another). Beyond notation there is also interest in the logical structure of the theory of geometry. Alfred Tarski proved that a portion of geometry, which he called elementary geometry, is a first order logical theory.

Modern text treatments of the axiomatic foundations of Euclidean geometry follow the pattern of H.G. Forder and Gilbert de B. Robinson^[54] who mix and match axioms from different systems to produce different emphasizes. Venema (2006) is a modern example of this approach.

Non-Euclidean geometry

In view of the role which mathematics plays in science and implications of scientific knowledge for all of our beliefs, revolutionary changes in man's understanding of the nature of mathematics could not but mean revolutionary changes in his understanding of science, doctrines of philosophy, religious and ethical beliefs, and, in fact, all intellectual disciplines.

In the first half of the nineteenth century a revolution took place in the field of geometry that was as scientifically important as the Copernican revolution in astronomy and as philosophically profound as the Darwinian theory of evolution in its impact on the way we think. This was the consequence of the discovery of non-Euclidean geometry. For over two thousand years, starting in the time of Euclid, the postulates which grounded geometry were considered self-evident truths about physical space. Geometers thought that they were deducing other, more obscure truths from them, without the possibility of error. This view became untenable with the development of hyperbolic geometry. There were now two incompatible systems of geometry (and more came later) that were self-consistent and compatible with the observable physical world. "From this point on, the whole discussion of the relation between geometry and physical space was carried on in quite different terms."(Moise 1974, p. 388)

To obtain a non-Euclidean geometry, the parallel postulate (or its equivalent) must be replaced by its negation. Negating the Playfair's axiom form, since it is a compound statement (... there exists one and only one ...), can be done in two ways. Either there will exist more than one line through the point parallel to the given line or there will exist no lines through the point parallel to the given line. In the first case, replacing the parallel postulate (or its equivalent) with the statement "In a plane, given a point P and a line ℓ not passing through P, there exist two lines through P which do not meet ℓ" and keeping all the other axioms, yields hyperbolic geometry. The second case is not dealt with as easily. Simply replacing the parallel postulate with the statement, "In a plane, given a point P and a line ℓ not passing through P, all the lines through P meet ℓ", does not give a consistent set of axioms. This follows since parallel lines exist in absolute geometry, but this statement would say that there are no parallel lines. This problem was known (in a different guise) to Khayyam, Saccheri and Lambert and was the basis for their rejecting what was known as the "obtuse angle case". In order to obtain a consistent set of axioms which includes this axiom about having no parallel lines, some of the other axioms must be tweaked. The adjustments to be made depend upon the axiom system being used. Amongst others these tweaks will have the effect of modifying Euclid's second postulate from the statement that line segments can be extended indefinitely to the statement that lines are unbounded. Riemann's elliptic geometry emerges as the most natural geometry satisfying this axiom.

It was Gauss who coined the term "non-Euclidean geometry". He was referring to his own, unpublished work, which today we call hyperbolic geometry. Several authors still consider "non-Euclidean geometry" and "hyperbolic geometry" to be synonyms. In 1871, Felix Klein, by adapting a metric discussed by Arthur Cayley in 1852, was able to bring metric properties into a projective setting and was thus able to unify the treatments of hyperbolic, euclidean and elliptic geometry under the umbrella of projective geometry.^[60] Klein is responsible for the terms "hyperbolic" and "elliptic" (in his system he called Euclidean geometry "parabolic", a term which has not survived the test of time and is used today only in a few disciplines.) His influence has led to the common usage of the term "non-Euclidean geometry" to mean either "hyperbolic" or "elliptic" geometry.

There are some mathematicians who would extend the list of geometries that should be called "non-Euclidean" in various ways. In other disciplines, most notably mathematical physics, where Klein's influence was not as strong, the term "non-Euclidean" is often taken to mean not Euclidean.

Euclid's parallel postulate

For two thousand years, many attempts were made to prove the parallel postulate using Euclid's first four postulates. A possible reason that such a proof was so highly sought after was that, unlike the first four postulates, the parallel postulate isn't self-evident. If the order the postulates were listed in the Elements is significant, it indicates that Euclid included this postulate only when he realised he could not prove it or proceed without it. Many attempts were made to prove the fifth postulate from the other four, many of them being accepted as proofs for long periods of time until the mistake was found. Invariably the mistake was assuming some 'obvious' property which turned out to be equivalent to the fifth postulate. Eventually it was realized that this postulate may not be provable from the other four. According to Trudeau (1987, p. 154) this opinion about the parallel postulate (Postulate 5) does appear in print:

Apparently the first to do so was G. S. Klügel (1739–1812), a doctoral student at the University of Gottingen, with the support of his teacher A. G. Kästner, in the former's 1763 dissertation Conatuum praecipuorum theoriam parallelarum demonstrandi recensio (Review of the Most Celebrated Attempts at Demonstrating the Theory of Parallels). In this work Klügel examined 28 attempts to prove Postulate 5 (including Saccheri's), found them all deficient, and offered the opinion that Postulate 5 is unprovable and is supported solely by the judgment of our senses.

The beginning of the 19th century would finally witness decisive steps in the creation of non-Euclidean geometry. Circa 1813, Carl Friedrich Gauss and independently around 1818, the German professor of law Ferdinand Karl Schweikart had the germinal ideas of non-Euclidean geometry worked out, but neither published any results. Then, around 1830, the Hungarian mathematician János Bolyai and the Russian mathematician Nikolai Ivanovich Lobachevsky separately published treatises on what we today call hyperbolic geometry. Consequently, hyperbolic geometry has been called Bolyai-Lobachevskian geometry, as both mathematicians, independent of each other, are the basic authors of non-Euclidean geometry. Gauss mentioned to Bolyai's father, when shown the younger Bolyai's work, that he had developed such a geometry several years before, though he did not publish. While Lobachevsky created a non-Euclidean geometry by negating the parallel postulate, Bolyai worked out a geometry where both the Euclidean and the hyperbolic geometry are possible depending on a parameter k. Bolyai ends his work by mentioning that it is not possible to decide through mathematical reasoning alone if the geometry of the physical universe is Euclidean or non-Euclidean; this is a task for the physical sciences. The independence of the parallel postulate from Euclid's other axioms was finally demonstrated by Eugenio Beltrami in 1868.

The various attempted proofs of the parallel postulate produced a long list of theorems that are equivalent to the parallel postulate. Equivalence here means that in the presence of the other axioms of the geometry each of these theorems can be assumed to be true and the parallel postulate can be proved from this altered set of axioms. This is not the same as logical equivalence. In different sets of axioms for Euclidean geometry, any of these can replace the Euclidean parallel postulate. The following partial list indicates some of these theorems that are of historical interest.

1. Parallel straight lines are equidistant. (Poseidonios, 1st century B.C.)
2. All the points equidistant from a given straight line, on a given side of it, constitute a straight line. (Christoph Clavius, 1574)
3. Playfair's axiom. In a plane, there is at most one line that can be drawn parallel to another given one through an external point. (Proclus, 5th century, but popularized by John Playfair, late 18th century)
4. The sum of the angles in every triangle is 180° (Gerolamo Saccheri, 1733; Adrien-Marie Legendre, early 19th century)
5. There exists a triangle whose angles add up to 180°. (Gerolamo Saccheri, 1733; Adrien-Marie Legendre, early 19th century)
6. There exists a pair of similar, but not congruent, triangles. (Gerolamo Saccheri, 1733)
7. Every triangle can be circumscribed. (Adrien-Marie Legendre, Farkas Bolyai, early 19th century)
8. If three angles of a quadrilateral are right angles, then the fourth angle is also a right angle. (Alexis-Claude Clairaut, 1741; Johann Heinrich Lambert, 1766)
9. There exists a quadrilateral in which all angles are right angles. (Geralamo Saccheri, 1733)
10. Wallis' postulate. On a given finite straight line it is always possible to construct a triangle similar to a given triangle. (John Wallis, 1663; Lazare-Nicholas-Marguerite Carnot, 1803; Adrien-Marie Legendre, 1824)
11. There is no upper limit to the area of a triangle. (Carl Friedrich Gauss, 1799)
12. The summit angles of the Saccheri quadrilateral are 90°. (Geralamo Saccheri, 1733)
13. Proclus' axiom. If a line intersects one of two parallel lines, both of which are coplanar with the original line, then it also intersects the other. (Proclus, 5th century)

Neutral (or Absolute) geometry

Absolute geometry is a geometry based on an axiom system consisting of all the axioms giving Euclidean geometry except for the parallel postulate or any of its alternatives. The term was introduced by János Bolyai in 1832.^[69] It is sometimes referred to as neutral geometry, as it is neutral with respect to the parallel postulate.

Relation to other geometries

In Euclid's Elements, the first 28 propositions and Proposition I.31 avoid using the parallel postulate, and therefore are valid theorems in absolute geometry.^[71] Proposition I.31 proves the existence of parallel lines (by construction). Also, the Saccheri–Legendre theorem, which states that the sum of the angles in a triangle is at most 180°, can be proved.

The theorems of absolute geometry hold in hyperbolic geometry as well as in Euclidean geometry.

Absolute geometry is inconsistent with elliptic geometry: in elliptic geometry there are no parallel lines at all, but in absolute geometry parallel lines do exist. Also, in elliptic geometry, the sum of the angles in any triangle is greater than 180°.

Incompleteness

Logically, the axioms do not form a complete theory since one can add extra independent axioms without making the axiom system inconsistent. One can extend absolute geometry by adding different axioms about parallelism and get incompatible but consistent axiom systems, giving rise to Euclidean or hyperbolic geometry. Thus every theorem of absolute geometry is a theorem of hyperbolic geometry and Euclidean geometry. However the converse is not true. Also, absolute geometry is not a categorical theory, since it has models that are not isomorphic.

Hyperbolic geometry

In the axiomatic approach to hyperbolic geometry (also referred to as Lobachevskian geometry or Bolyai–Lobachevskian geometry), one additional axiom is added to the axioms giving absolute geometry. The new axiom is Lobachevsky's parallel postulate (also known as the characteristic postulate of hyperbolic geometry):

Through a point not on a given line there exists (in the plane determined by this point and line) at least two lines which do not meet the given line.

With this addition, the axiom system is now complete.

Although the new axiom asserts only the existence of two lines, it is readily established that there are an infinite number of lines through the given point which do not meet the given line. Given this plenitude, one must be careful with terminology in this setting, as the term parallel line no longer has the unique meaning that it has in Euclidean geometry. Specifically, let P be a point not on a given line ${\displaystyle \ell }$. Let PA be the perpendicular drawn from P to ${\displaystyle \ell }$ (meeting at point A). The lines through P fall into two classes, those that meet ${\displaystyle \ell }$ and those that don't. The characteristic postulate of hyperbolic geometry says that there are at least two lines of the latter type. Of the lines which don't meet ${\displaystyle \ell }$, there will be (on each side of PA) a line making the smallest angle with PA. Sometimes these lines are referred to as the first lines through P which don't meet ${\displaystyle \ell }$ and are variously called limiting, asymptotic or parallel lines (when this last term is used, these are the only parallel lines). All other lines through P which do not meet ${\displaystyle \ell }$ are called non-intersecting or ultraparallel lines.

Since hyperbolic geometry and Euclidean geometry are both built on the axioms of absolute geometry, they share many properties and propositions. However, the consequences of replacing the parallel postulate of Euclidean geometry with the characteristic postulate of hyperbolic geometry can be dramatic. To mention a few of these:

Lambert quadrilateral in hyperbolic geometry

• A Lambert quadrilateral is a quadrilateral which has three right angles. The fourth angle of a Lambert quadrilateral is acute if the geometry is hyperbolic, and a right angle if the geometry is Euclidean. Furthermore, rectangles can exist (a statement equivalent to the parallel postulate) only in Euclidean geometry.
• A Saccheri quadrilateral is a quadrilateral which has two sides of equal length, both perpendicular to a side called the base. The other two angles of a Saccheri quadrilateral are called the summit angles and they have equal measure. The summit angles of a Saccheri quadrilateral are acute if the geometry is hyperbolic, and right angles if the geometry is Euclidean.
• The sum of the measures of the angles of any triangle is less than 180° if the geometry is hyperbolic, and equal to 180° if the geometry is Euclidean. The defect of a triangle is the numerical value (180° – sum of the measures of the angles of the triangle). This result may also be stated as: the defect of triangles in hyperbolic geometry is positive, and the defect of triangles in Euclidean geometry is zero.
• The area of a triangle in hyperbolic geometry is bounded while triangles exist with arbitrarily large areas in Euclidean geometry.
• The set of points on the same side and equally far from a given straight line themselves form a line in Euclidean geometry, but don't in hyperbolic geometry (they form a hypercycle.)

Advocates of the position that Euclidean geometry is the one and only "true" geometry received a setback when, in a memoir published in 1868, "Fundamental theory of spaces of constant curvature", Eugenio Beltrami gave an abstract proof of equiconsistency of hyperbolic and Euclidean geometry for any dimension. He accomplished this by introducing several models of non-Euclidean geometry that are now known as the Beltrami–Klein model, the Poincaré disk model, and the Poincaré half-plane model, together with transformations that relate them. For the half-plane model, Beltrami cited a note by Liouville in the treatise of Monge on differential geometry. Beltrami also showed that n-dimensional Euclidean geometry is realized on a horosphere of the (n + 1)-dimensional hyperbolic space, so the logical relation between consistency of the Euclidean and the non-Euclidean geometries is symmetric.

Elliptic geometry

Another way to modify the Euclidean parallel postulate is to assume that there are no parallel lines in a plane. Unlike the situation with hyperbolic geometry, where we just add one new axiom, we can not obtain a consistent system by adding this statement as a new axiom to the axioms of absolute geometry. This follows since parallel lines provably exist in absolute geometry. Other axioms must be changed.

Starting with Hilbert's axioms the necessary changes involve removing Hilbert's four axioms of order and replacing them with these seven axioms of separation concerned with a new undefined relation.

There is an undefined (primitive) relation between four points, A, B, C and D denoted by (A,C|B,D) and read as "A and C separate B and D", satisfying these axioms:

1. If (A,B|C,D), then the points A, B, C and D are collinear and distinct.
2. If (A,B|C,D), then (C,D|A,B) and (B,A|D,C).
3. If (A,B|C,D), then not (A,C|B,D).
4. If points A, B, C and D are collinear and distinct then (A,B|C,D) or (A,C|B,D) or (A,D|B,C).
5. If points A, B, and C are collinear and distinct, then there exists a point D such that (A,B|C,D).
6. For any five distinct collinear points A, B, C, D and E, if (A,B|D,E), then either (A,B|C,D) or (A,B|C,E).
7. Perspectivities preserve separation.

Since the Hilbert notion of "betweeness" has been removed, terms which were defined using that concept need to be redefined. Thus, a line segment AB defined as the points A and B and all the points between A and B in absolute geometry, needs to be reformulated. A line segment in this new geometry is determined by three collinear points A, B and C and consists of those three points and all the points not separated from B by A and C. There are further consequences. Since two points do not determine a line segment uniquely, three noncollinear points do not determine a unique triangle, and the definition of triangle has to be reformulated.

Once these notions have been redefined, the other axioms of absolute geometry (incidence, congruence and continuity) all make sense and are left alone. Together with the new axiom on the nonexistence of parallel lines we have a consistent system of axioms giving a new geometry. The geometry that results is called (plane) Elliptic geometry.

Saccheri quadrilaterals in Euclidean, Elliptic and Hyperbolic geometry

Even though elliptic geometry is not an extension of absolute geometry (as Euclidean and hyperbolic geometry are), there is a certain "symmetry" in the propositions of the three geometries that reflects a deeper connection which was observed by Felix Klein. Some of the propositions which exhibit this property are:

• The fourth angle of a Lambert quadrilateral is an obtuse angle in elliptic geometry.
• The summit angles of a Saccheri quadrilateral are obtuse in elliptic geometry.
• The sum of the measures of the angles of any triangle is greater than 180° if the geometry is elliptic. That is, the defect of a triangle is negative.
• All the lines perpendicular to a given line meet at a common point in elliptic geometry, called the pole of the line. In hyperbolic geometry these lines are mutually non-intersecting, while in Euclidean geometry they are mutually parallel.

Other results, such as the exterior angle theorem, clearly emphasize the difference between elliptic and the geometries that are extensions of absolute geometry.

Other geometries

Ordered geometry

Absolute geometry is an extension of ordered geometry, and thus, all theorems in ordered geometry hold in absolute geometry. The converse is not true. Absolute geometry assumes the first four of Euclid's Axioms (or their equivalents), to be contrasted with affine geometry, which does not assume Euclid's third and fourth axioms. Ordered geometry is a common foundation of both absolute and affine geometry.