Commit 21a02708 authored by Raphael Cauderlier's avatar Raphael Cauderlier

[fol] definition of n-ary quantifiers

parent 80698ccb
......@@ -105,6 +105,38 @@ def not (p : prop) := imp p false.
def true := not false.
def eqv (p : prop) (q : prop) := and (imp p q) (imp q p).
(; n-ary quantification ;)
(; nall_aux [A₁; …; Aₙ] : (term A₁ -> … -> term Aₙ -> prop) -> prop ;)
def nall_aux_type : types -> Type.
[] nall_aux_type nil_type --> prop.
[A,As] nall_aux_type (cons_type A As) --> term A -> nall_aux_type As.
def nall_aux : As : types -> nall_aux_type As -> prop.
[P] nall_aux nil_type --> P => P.
[A,As,P] nall_aux (cons_type A As) --> P => all A (a => nall_aux As (P a)).
def nex_aux : As : types -> nall_aux_type As -> prop.
[P] nex_aux nil_type --> P => P.
[A,As,P] nex_aux (cons_type A As) --> P => ex A (a => nex_aux As (P a)).
(; nall_aux2 [B₁; …; Bₘ] n A₁ … Aₙ = nall_aux [B₁; …; Bₘ; A₁; …; Aₙ] ;)
(; nall_aux2_type Bs n A₁ … Aₙ = nall_aux_type (Bs^As) -> prop ;)
def nall_aux2_type : types -> nat -> Type.
[Bs] nall_aux2_type Bs nat.O --> nall_aux_type Bs -> prop
[Bs,n] nall_aux2_type Bs (nat.S n) --> A : type -> nall_aux2_type (snoc_type Bs A) n.
def nall_aux2 : Bs : types -> n : nat -> nall_aux2_type Bs n.
[Bs] nall_aux2 Bs nat.O --> nall_aux Bs
[Bs,n] nall_aux2 Bs (nat.S n) --> A => nall_aux2 (snoc_type Bs A) n.
def nex_aux2 : Bs : types -> n : nat -> nall_aux2_type Bs n.
[Bs] nex_aux2 Bs nat.O --> nex_aux Bs
[Bs,n] nex_aux2 Bs (nat.S n) --> A => nex_aux2 (snoc_type Bs A) n.
def nall (n : nat) : nall_aux2_type nil_type n := nall_aux2 nil_type n.
def nex (n : nat) : nall_aux2_type nil_type n := nex_aux2 nil_type n.
(; Predicate application is also nary ;)
predicate : Type.
def pred_arity : predicate -> types.
......
......@@ -171,6 +171,10 @@ are represented by Dedukti variables.
The universal and existential quantifiers are respectively =fol.all=
and =fol.ex=. They have the same Dedukti type: =A : fol.type -> (fol.term A -> fol.prop) -> fol.prop=.
For convenience, n-ary versions =fol.nall= and =fol.nex= of these
quantifiers are also defined. They have the same type =n : nat.Nat -> A₁ : type -> … -> Aₙ : type -> (term A₁ -> … -> term Aₙ -> prop) -> prop= and are defined by nesting =fol.all= and =fol.ex=.
*** Proofs
We use an intuitionistic natural deduction proof system. If =A= is a
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment