Skip to content

jonaprieto/agda-prop

Repository files navigation

Agda-Prop Build Status DOI

This is a library to work with Classical Propositional Logic based on a deep embedding. It also contains a compilation of useful theorems with their natural deduction proofs, and some properties ready to work with and some algorithms like NNF, CNF, among others.

Quick Start

Prerequisites

Tested with:

Types

We define two data types, the formula data type Prop and the theorem data type _⊢_, that depended of a list of hypothesis and the conclusion, a formula. The constructors are the following.

data PropFormula : Type where
  Var  : Fin n  PropFormula           -- Variables.
  : PropFormula                   -- Top (truth).
  : PropFormula                   -- Bottom (falsum).
  _∧_  : (φ ψ : PropFormula)  Prop    -- Conjunction.
  _∨_  : (φ ψ : PropFormula)  Prop    -- Disjunction.
  _⊃_  : (φ ψ : PropFormula)  Prop    -- Implication.
  _⇔_  : (φ ψ : PropFormula)  Prop    -- Biimplication.
  ¬_   :: PropFormula)    Prop    -- Negation.

The theorems use the following inference rules:

data _⊢_ :: Ctxt)(φ : PropFormula)  Set where

-- Hyp.

  assume   :  {Γ} : PropFormula)       Γ , φ ⊢ φ

  axiom    :  {Γ} : PropFormula)       φ ∈ Γ
                                             Γ ⊢ φ

  weaken   :  {Γ} {φ} : PropFormula)   Γ ⊢ φ
                                             Γ , ψ ⊢ φ

  weaken₂   :  {Γ} {φ} : PropFormula)  Γ ⊢ φ
                                             ψ ∷ Γ ⊢ φ
-- Top and Bottom.

  ⊤-intro  :  {Γ}                           Γ ⊢ ⊤

  ⊥-elim   :  {Γ} : PropFormula)       Γ ⊢ ⊥
                                             Γ ⊢ φ
-- Negation.

  ¬-intro  :  {Γ} {φ}                       Γ , φ ⊢ ⊥
                                             Γ ⊢ ¬ φ

  ¬-elim   :  {Γ} {φ}                       Γ ⊢ ¬ φ  Γ ⊢ φ
                                             Γ ⊢ ⊥
-- Conjunction.

  ∧-intro  :  {Γ} {φ ψ}                     Γ ⊢ φ  Γ ⊢ ψ
                                             Γ ⊢ φ ∧ ψ

  ∧-proj₁  :  {Γ} {φ ψ}                     Γ ⊢ φ ∧ ψ
                                             Γ ⊢ φ

  ∧-proj₂  :  {Γ} {φ ψ}                     Γ ⊢ φ ∧ ψ
                                             Γ ⊢ ψ
-- Disjunction.

  ∨-intro₁ :  {Γ} {φ} : PropFormula)   Γ ⊢ φ
                                             Γ ⊢ φ ∨ ψ

  ∨-intro₂ :  {Γ} {ψ} : PropFormula)   Γ ⊢ ψ
                                             Γ ⊢ φ ∨ ψ

  ∨-elim  :  {Γ} {φ ψ χ}                    Γ , φ ⊢ χ
                                             Γ , ψ ⊢ χ
                                             Γ , φ ∨ ψ ⊢ χ
-- Implication.

  ⊃-intro  :  {Γ} {φ ψ}                     Γ , φ ⊢ ψ
                                             Γ ⊢ φ ⊃ ψ

  ⊃-elim   :  {Γ} {φ ψ}                     Γ ⊢ φ ⊃ ψ  Γ ⊢ φ
                                             Γ ⊢ ψ
-- Biconditional.

  ⇔-intro  :  {Γ} {φ ψ}                     Γ , φ ⊢ ψ
                                             Γ , ψ ⊢ φ
                                             Γ ⊢ φ ⇔ ψ

  ⇔-elim₁ :  {Γ} {φ ψ}                      Γ ⊢ φ  Γ ⊢ φ ⇔ ψ
                                             Γ ⊢ ψ

  ⇔-elim₂ :  {Γ} {φ ψ}                      Γ ⊢ ψ  Γ ⊢ φ ⇔ ψ
                                             Γ ⊢ φ

Library

We have a list of theorems for each connective and a mix of them. Their names are based on their main connective, their purpose or their source. We added sub-indices for those theorems that differ a little with other one. If you need an specific theorem that you think we should include, open an issue.

Additional Theorems

Example

$ cat test/ex-andreas-abel.agda
open import Data.PropFormula 2 public
...

EM⊃Pierce
  :  {Γ} {φ ψ}
   Γ ⊢ ((φ ⊃ ψ) ⊃ φ) ⊃ φ

EM⊃Pierce {Γ}{φ}{ψ} =
  ⊃-elim
    (⊃-intro
      (∨-elim {Γ = Γ}
        (⊃-intro
          (weaken ((φ ⊃ ψ) ⊃ φ)
            (assume {Γ = Γ} φ)))
        (⊃-intro
          (⊃-elim
            (assume {Γ = Γ , ¬ φ} ((φ ⊃ ψ) ⊃ φ))
              (⊃-intro
                (⊥-elim
                  ψ
                  (¬-elim
                  (weaken φ
                    (weaken ((φ ⊃ ψ) ⊃ φ)
                      (assume {Γ = Γ} (¬ φ))))
                      (assume {Γ = Γ , ¬ φ , (φ ⊃ ψ) ⊃ φ} φ))))
            ))))
      PEM -- ∀ {Γ} {φ}  → Γ ⊢ φ ∨ ¬ φ

...

References