Project

Namespaces

Public Vars

latte-prelude.quant

Basic definitions and theorems about the universal and existential quantifiers.

Note that for the universal quantifier, it is a primitive of the calculus of constructions, hence Latte.

The elimination rule for ∀ (for all) is application, and introduction is through lambda-abstraction.

decompose-ex-type

(decompose-ex-type def-env ctx t)

decompose-forall-type

(decompose-forall-type def-env ctx t)

decompose-single-type

(decompose-single-type def-env ctx t)

ex

(ex [P (==> T :type)])
(forall [α :type] (==> (forall [x T] (==> (P x) α)) α))

Definition: The encoding for the existential quantifier.

(ex P) encodes the existential quantification

there exists an element of (implicit) type T such that the predicate P holds for this element.

Remark: this is a second-order, intuitionistic definition that is more general than the definition in classical logic.

ex-elim

An elimination rule written (ex-elim ex-proof x-proof) with: - ex-proof of type (ex P) for some property P if type (==> T :type), - x-proof a proof of (forall [x T] (==> (P x) A)) for some goal statement A. Thanks to ex-elim-rule the goal A is concluded.

ex-elim-rule

(ex-elim-rule [P (==> T :type)] [A :type])
(==> (ex P) (forall [x T] (==> (P x) A)) A)

Theorem: The (intuitionistic) elimination rule for the existential quantifier.

ex-impl

(ex-impl [P (==> T :type)] [Q (==> T :type)])
(==> (ex P) (forall [x T] (==> (P x) (Q x))) (ex Q))

Theorem: Use of implication in existentials.

ex-intro

(ex-intro [P (==> T :type)] [x T])
(==> (P x) (ex P))

Theorem: The introduction rule for the existential quantifier.

exists

The existential quantification (exists [x T] P) is a shortcut for (ex (lambda [x T] P)), corresponding to the usual notation for existential quantification: ∃x:T.(P x)

there exists an x of type T such that (P x) is true.

not-ex-elim

(not-ex-elim [P (==> T :type)])
(==> (not (ex P)) (forall [x T] (not (P x))))

Theorem: The classical elimination rule for negation of existence.

not-ex-intro

(not-ex-intro [P (==> T :type)])
(==> (forall [x T] (not (P x))) (not (ex P)))

Theorem: The introduction rule for negation of existence.

not-not-elim

(not-not-elim [P (==> T :type)])
(==> (not (exists [x T] (not (P x)))) (forall [x T] (P x)))

Theorem: A classical (i.e. non-intuitionistic) elimination rule for double existential negation.

single

(single [P (==> T :type)])
(forall [x y T] (==> (P x) (P y) (equal x y)))

Definition: The constraint that “there exists at most”…

single-elim

Elimination rule for single. (single-elim s-proof x y) such that the type of s-proof is (single P) for some property P, then we have (==> (P x) (P y) (equal x y)) thanks to [[single-elim-rule]].

single-elim-rule

(single-elim-rule [P (==> T :type)] [x T] [y T])
(==> (single P) (P x) (P y) (equal x y))

Theorem: Elimination rule for single.

single-intro

(single-intro [P (==> T :type)])
(==> (forall [x y T] (==> (P x) (P y) (equal x y))) (single P))

Theorem: Introduction rule for single.

the

The unique element descriptor.

(the u) defines the unique object satisfying a predicate P as demonstrated by the proof u of type (unique P). This is the implicit version of the axiom the-ax.

the-ax

(the-ax [T :type] [P (==> T :type)] [u (unique P)])
T

Axiom: The unique element descriptor.

(the T P u) defines the unique inhabitant of type T satisfying the predicate P. This is provided thanks to the uniqueness proof u (of type (unique T P).

the-lemma

(the-lemma u) proves that (forall [y T] (==> (P y) (equal y (the u)))) from the proof u that (unique P) for some property P.

the-lemma-prop

(the-lemma-prop [P (==> T :type)] [u (unique P)])
(forall [y T] (==> (P y) (equal y (the u))))

Theorem: The unique element is … unique.

the-prop

(the-prop u) proves (P (the u)) from the proof u of (unique P), for some property P. This is the main property of the unique descriptor the, cf. the-prop-ax.

the-prop-ax

(the-prop-ax [T :type] [P (==> T :type)] [u (unique P)])
(P (the u))

Axiom: The property of the unique element descriptor.

unique

(unique [P (==> T :type)])
(and (ex P) (single P))

Definition: The constraint that “there exists a unique” …