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.
Tested with:
- Agda version 2.5.4
- Agda Standard Library version 0.16
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₂ : ∀ {Γ} {φ ψ} → Γ ⊢ ψ → Γ ⊢ φ ⇔ ψ
→ Γ ⊢ φ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.
$ 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 -- ∀ {Γ} {φ} → Γ ⊢ φ ∨ ¬ φ
...
- Cai, L., Kaposi, A., & Altenkirch, T. (2015) Formalising the Completeness Theorem of Classical Propositional Logic in Agda. Retrieved from https://akaposi.github.io/proplogic.pdf