module PredicateLogic where
{-
Howard introduced dependent types and could thus extend Curry's correspondence between propositions as types (sets) to the quantifiers.
Since a predicate corresponds to a set a predicate P over a set A, corresponds to a "propositional function" P : A → Set. The universally quantified proposition ∀ x : A. P x corresponds to the set (x : A) → P x. Intuitively a proof of ∀ x : A. P x is a function which maps an arbitrary element a : A to a proof of P a.
Agda allows the notation ∀ (x : A) → P x which emphasizes the correspondence between the dependent function space and universally quantified propositions.
Alternatively, you can think of universal quantification (over an infinite set) as infinite conjunction and existential quantification as infinite disjunction.
A proof of an existentially quantified proposition ∃ x : A. P x is a pair < a , p > consisting of an element a : A and a proof p : P a. We can define it as a data type with one constructor:
-}
data ∃ (A : Set) (P : A → Set) : Set where
<_,_> : (a : A) → P a → ∃ A P
{-
The first projection gives access to the "witness" a : A.
-}
witness : {A : Set} {P : A → Set} -> ∃ A P → A
witness < a , p > = a
{-
The second projection gives access to the proof that P holds for the witness a (that is, p : P a).
-}
proof : {A : Set} → {P : A → Set} → (c : ∃ A P) → P (witness c)
proof < a , p > = p
{-
The rule of existence elimination is as follows:
-}
∃-elim : {A : Set} → {P : A → Set} → {Q : Set}
→ ((a : A) → P a → Q) → ∃ A P → Q
∃-elim f < a , p > = f a p
{-
Exercise:
Define uncurrying!
uncurry : {A B C : Set} → (A → B → C) → A × B → C
and note the similarity with ∃-elim!
The universal quantifier can be defined as a datatype with a single constructor (cf definition of implication)
-}
data ∀‘ (A : Set) (P : A → Set) : Set where
∀'-intro : ((x : A) → P x) → ∀‘ A P
{-
Note that this gives variable free-notation ∀‘ A P = ∀‘ A (λ x → P x) for ∀ x : A. P x.
We can also define the rule of universal elimination:
-}
∀'-elim : {A : Set} {P : A → Set} → ∀‘ A P → (a : A) → P a
∀'-elim (∀'-intro f) a = f a