How to do deep embedding of propositional calculus?

Using Coq
1

Can you suggest any literature (algorithms etc.) that could help with making a library - for constructing proofs in propositional calculus and other possible useful stuff.
The following is the start, where I define axioms as formulae and inference rules in similar way.

Require Import List.
Import ListNotations.

Inductive prop :=
| Var: nat -> prop
| Neg: prop -> prop
| And: prop -> prop -> prop
| Or: prop -> prop -> prop
| Impl: prop -> prop -> prop.

Coercion Var: nat >-> prop.

Notation "¬ A" := (Neg A) (at level 20): prop.
Notation "A ∧ B" := (And A B) (at level 21, right associativity): prop.
Notation "A ∨ B" := (Or A B) (at level 22, right associativity): prop.
Notation "A → B" := (Impl A B) (at level 23, right associativity): prop.

Open Scope prop.

Definition B := 0.
Definition C := 1.
Definition D := 2.

Definition L1 := B → (C → B).
(* ... omitted axioms ... *) 

Definition inference_rule := prod (list prop) prop.
Definition MP: inference_rule := ([B → C ; Var B], Var C).
2

If you’re only looking for a way to express rules for a simple propositional system, you might find this encoding of a sound Fitch-style proof system via the Ott tool helpful. Specifically, Ott generates the Coq code for the tedious inductive predicate expressing 15+ inference rules. There is also an executable proof checker.

However, the crux for a full system equivalent to natural deduction for first-order logic is that one needs to handle capture-avoiding substitution, and there are many widely different ways to do that (autosubst is one that comes to mind).

1 Like