--#include "BasicTypeTheory.agda" -- The simple propositions are defined as a recursive data type -- where there is an atomic formula atom(P) for -- each (constructive) proposition P SP :: Type = data absurd | atom (P::Set) | sand (a::SP) (b::SP) | simp (a::SP) (b::SP) | sor (a::SP) (b::SP) | forall (A::Set) (P::A -> SP) | exists (A::Set) (P::A -> SP) -- translation to ordinary proposition Tp (S::SP) :: Set = case S of { (absurd) -> Absurd; (atom P) -> P; (sand a b) -> Cart (Tp a) (Tp b); (simp a b) -> Tp a -> Tp b; (sor a b) -> Sum (Tp a) (Tp b); (forall A P) -> Pi A (\(h::A) -> Tp (P h)); (exists A P) -> Sigma A (\(h::A) -> Tp (P h));} -- make types for realising terms Cr (S::SP) :: Set = case S of { (absurd) -> Unit; (atom P) -> Unit; (sand a b) -> Cart (Cr a) (Cr b); (simp a b) -> Cr a -> Cr b; (sor a b) -> Sum (Cr a) (Cr b); (forall A P) -> Pi A (\(h::A) -> Cr (P h)); (exists A P) -> Sum Unit (Sigma A (\(h::A) -> Cr (P h)));} element (S::SP) :: Cr S = case S of { (absurd) -> elt@_; (atom P) -> elt@_; (sand a b) -> struct { _1 = element a; _2 = element b;}; (simp a b) -> \(h::Cr a) -> element b; (sor a b) -> inl@_ (element a); (forall A P) -> \(x::A) -> element (P x); (exists A P) -> inl@_ elt@_;} -- Modified realisability with truth (see implication case) MR (S::SP)(r::Cr S) :: Set = case S of { (absurd) -> Absurd; (atom P) -> P; (sand a b) -> and (MR a r._1) (MR b r._2); (simp a b) -> and ((x::Cr a) -> MR a x -> MR b (r x)) (Tp a -> Tp b); (sor a b) -> case r of { (inl x) -> MR a x; (inr y) -> MR b y;}; (forall A P) -> (t::A) -> MR (P t) (r t); (exists A P) -> case r of { (inl x) -> Absurd; (inr y) -> MR (P y._1) y._2;};} -- Correctness theorem Correct (S::SP)(r::Cr S)(p::MR S r) :: Tp S = case S of { (absurd) -> p; (atom P) -> p; (sand a b) -> struct { _1 = Correct a r._1 p._1; _2 = Correct b r._2 p._2;}; (simp a b) -> p._2; (sor a b) -> case r of { (inl x) -> inl@_ (Correct a x p); (inr y) -> inr@_ (Correct b y p);}; (forall A P) -> \(x::A) -> Correct (P x) (r x) (p x); (exists A P) -> case r of { (inl x) -> elempty (Tp (exists@_ A P)) p; (inr y) -> struct { _1 = y._1; _2 = Correct (P _1) y._2 p;};};} -- predicate for realised formulas Realized (A::SP) :: Set = sig{real :: Cr A; pf :: MR A real;} Correct_2 (A::SP)(pf::Realized A) :: Tp A = Correct A pf.real pf.pf -- extraction theorem for AE-formulas Extract (A::Set) (B::Set) (P::A -> B -> SP) (pfe::Realized (forall@_ A (\(x::A) -> exists@_ B (\(y::B) -> P x y)))) :: Pi A (\(x::A) -> Sigma B (\(y::B) -> Tp (P x y))) = \(x::A) -> Correct_2 (exists@_ B (\(y::B) -> P x y)) (struct { real = pfe.real x; pf = pfe.pf x;}) -- Validity of rules for first order logic -- system essentially the one often used in categorical logic -- Note: weak elimination rule true_impl_realised (A::Set)(B::Set)(p::A -> B) :: Realized (simp@_ (atom@_ A) (atom@_ B)) = struct { real = \(h::Cr (atom@_ A)) -> h; pf = struct { _1 = \(x::Cr (atom@_ A)) -> p; _2 = p;};} Entails (a::SP)(b::SP) :: SP = simp@_ a b truthaxiom (a::SP)(P::Set)(p::P) :: Realized (Entails a (atom@_ P)) = struct { real = \(h::Cr a) -> elt@_; pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> p; _2 = \(h::Tp a) -> p;};} absurdityaxiom (a::SP) :: Realized (Entails absurd@_ a) = struct { real = \(h::Cr absurd@_) -> element a; pf = struct { _1 = \(x::Cr absurd@_) -> \(h::MR absurd@_ x) -> elempty (MR a (real x)) h; _2 = \(h::Tp absurd@_) -> elempty (Tp a) h;};} idaxiom (a::SP) :: Realized (Entails a a) = struct { real = \(h::Cr a) -> h; pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> h; _2 = \(h::Tp a) -> h;};} cut (a::SP) (b::SP) (c::SP) (p1::Realized (Entails a b)) (p2::Realized (Entails b c)) :: Realized (Entails a c) = struct { real = \(h::Cr a) -> p2.real (p1.real h); pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> p2.pf._1 (p1.real x) (p1.pf._1 x h); _2 = \(h::Tp a) -> p2.pf._2 (p1.pf._2 h);};} And_i (a::SP) (b::SP) (c::SP) (p1::Realized (Entails a b)) (p2::Realized (Entails a c)) :: Realized (Entails a (sand@_ b c)) = struct { real = \(h::Cr a) -> struct { _1 = p1.real h; _2 = p2.real h;}; pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> struct { _1 = p1.pf._1 x h; _2 = p2.pf._1 x h;}; _2 = \(h::Tp a) -> struct { _1 = p1.pf._2 h; _2 = p2.pf._2 h;};};} And_e1 (a::SP)(b::SP) :: Realized (Entails (sand@_ a b) a) = struct { real = \(h::Cr (sand@_ a b)) -> h._1; pf = struct { _1 = \(x::Cr (sand@_ a b)) -> \(h::MR (sand@_ a b) x) -> h._1; _2 = \(h::Tp (sand@_ a b)) -> h._1;};} And_e2 (a::SP)(b::SP) :: Realized (Entails (sand@_ a b) b) = struct { real = \(h::Cr (sand@_ a b)) -> h._2; pf = struct { _1 = \(x::Cr (sand@_ a b)) -> \(h::MR (sand@_ a b) x) -> h._2; _2 = \(h::Tp (sand@_ a b)) -> h._2;};} Imp_i (a::SP) (b::SP) (c::SP) (p::Realized (Entails (sand@_ a b) c)) :: Realized (Entails a (simp@_ b c)) = struct { real = \(h::Cr a) -> \(h'::Cr b) -> p.real (struct { _1 = h; _2 = h';}); pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> struct { _1 = \(x'::Cr b) -> \(h'::MR b x') -> p.pf._1 (struct { _1 = x; _2 = x';}) (struct { _1 = h; _2 = h';}); _2 = \(h'::Tp b) -> p.pf._2 (struct { _1 = Correct a x h; _2 = h';});}; _2 = \(h::Tp a) -> \(h'::Tp b) -> p.pf._2 (struct { _1 = h; _2 = h';});};} Or_i1 (a::SP)(b::SP) :: Realized (Entails a (sor@_ a b)) = struct { real = \(h::Cr a) -> inl@_ h; pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> h; _2 = \(h::Tp a) -> inl@_ h;};} Or_i2 (a::SP)(b::SP) :: Realized (Entails b (sor@_ a b)) = struct { real = \(h::Cr b) -> inr@_ h; pf = struct { _1 = \(x::Cr b) -> \(h::MR b x) -> h; _2 = \(h::Tp b) -> inr@_ h;};} Or_e (a::SP) (b::SP) (c::SP) (p1::Realized (Entails a c)) (p2::Realized (Entails b c)) :: Realized (Entails (sor@_ a b) c) = struct { real = \(h::Cr (sor@_ a b)) -> case h of { (inl x) -> p1.real x; (inr y) -> p2.real y;}; pf = struct { _1 = \(x::Cr (sor@_ a b)) -> case x of { (inl x') -> \(h::MR (sor@_ a b) (inl@_ x')) -> p1.pf._1 x' h; (inr y) -> \(h::MR (sor@_ a b) (inr@_ y)) -> p2.pf._1 y h;}; _2 = \(h::Tp (sor@_ a b)) -> case h of { (inl x) -> p1.pf._2 x; (inr y) -> p2.pf._2 y;};};} Imp_e (a::SP) (b::SP) (c::SP) (p::Realized (Entails a (simp@_ b c))) :: Realized (Entails (sand@_ a b) c) = struct { real = \(h::Cr (sand@_ a b)) -> p.real h._1 h._2; pf = struct { _1 = \(x::Cr (sand@_ a b)) -> \(h::MR (sand@_ a b) x) -> let p1 :: MR (simp@_ b c) (p.real x._1) = p.pf._1 x._1 h._1 in p1._1 x._2 h._2; _2 = \(h::Tp (sand@_ a b)) -> let p2 :: (h'::Tp a) -> Tp (simp@_ b c) = p.pf._2 in p2 h._1 h._2;};} All_i (A::Set) (a::SP) (P::A -> SP) (p::(x::A) -> Realized (Entails a (P x))) :: Realized (Entails a (forall@_ A P)) = struct { real = \(h::Cr a) -> \(x::A) -> (p x).real h; pf = struct { _1 = \(x::Cr a) -> \(h::MR a x) -> \(t::A) -> (p t).pf._1 x h; _2 = \(h::Tp a) -> \(x::A) -> (p x).pf._2 h;};} All_e (A::Set) (a::SP) (P::A -> SP) (p::Realized (Entails a (forall@_ A P))) (x::A) :: Realized (Entails a (P x)) = struct { real = \(h::Cr a) -> p.real h x; pf = let p1 :: MR (Entails a (forall@_ A P)) p.real = p.pf in struct { _1 = \(x'::Cr a) -> \(h::MR a x') -> p1._1 x' h x; _2 = \(h::Tp a) -> p1._2 h x;};} Ex_i (A::Set) (a::SP) (P::A -> SP) (p::(x::A) -> Realized (Entails (P x) a)) :: Realized (Entails (exists@_ A P) a) = struct { real = \(h::Cr (exists@_ A P)) -> case h of { (inl x) -> element a; (inr y) -> (p y._1).real y._2;}; pf = struct { _1 = \(x::Cr (exists@_ A P)) -> \(h::MR (exists@_ A P) x) -> case x of { (inl x') -> elempty (MR a (real (inl@_ x'))) h; (inr y) -> (p y._1).pf._1 y._2 h;}; _2 = \(h::Tp (exists@_ A P)) -> (p h._1).pf._2 h._2;};} Ex_e (A::Set) (a::SP) (P::A -> SP) (p::Realized (Entails (exists@_ A P) a)) (x::A) :: Realized (Entails (P x) a) = struct { real = \(h::Cr (P x)) -> p.real (inr@_ (struct { _1 = x; _2 = h;})); pf = struct { _1 = \(x'::Cr (P x)) -> \(h::MR (P x) x') -> p.pf._1 (inr@_ (struct { _1 = x; _2 = x';})) h; _2 = \(h::Tp (P x)) -> p.pf._2 (struct { _1 = x; _2 = h;});};} {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding off var "gg" con "forall" con "cimp" infix as "=>" con "cand" infix as "&" con "absurd" as "^" with symbolfont var "BinProd" infix as "´" with symbolfont var "Sigma" as "S" with symbolfont var "iff" infix var "Entails" infix as "|--" con "sand" infix as "&" con "simp" infix as "=>" con "sor" infix as "Ú" with symbolfont #-}