I've been playing with axiomising systems of first-order logic in Coq. I've started to develop the beginning of a framework. As an example I give a minimal phrasing of Peano arithmetic in Coq in the style I am developing.
I define entailment as a reflexive, transitive relation in a category theory like style which happens to work well with Coq's support for setoids. I define terms and propositions inductively and I use parametric higher order abstract syntax to implement quantifiers. I'm still not sure this is a good approach. I do feel this sort of approach is flexible enough I could work with modal logic, linear logic or possibly co-intuitionistic logic.
Equality, quantifiers and substitution and binders in general are a headache. I'm just not sure what sort of approach I want to take.
Description operators and comprehensions are also a pain. Either you mix the grammar of terms and propositions (which conflicts with PHOAS), duplicate the grammar of propositions or you must rephrase things awkwardly in terms of images and spans. Basically instead of a comprehension $\{ x \in e \mid P(x) \}$ you have a separate limited grammar for formulas $\phi$ inside the comprehension $\{ x \in e \mid \phi(x) \}$ different from propositions $P$ or you rephrase things in terms of equalizers $\{ x \in e_1 \mid e_2(x) = e_3(x) \}$ or images $\{ e_1(x) \mid x \in e_2 \}$.
Naming is one of the hardest problems and its never clear to me how I should name the various combinators. Coq's support for notations has been very helpful but also very annoying to figure out. There are still associativity issues I haven't figured out.
I've started to develop the beginning of an approach that could work for systems in first-order logic but I'm not sure I want to commit to further work in this style. I'm still not confident this sort of approach would really scale up to working with something like NBG set theory.
Require Import Coq.Unicode.Utf8.
Require Coq.Program.Basics.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Lists.List.
Import IfNotations.
Import List.ListNotations.
Reserved Infix "⊢" (at level 90).
Reserved Notation "'∃' x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "∀ x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "'!' x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "'∃!' x .. y , P" (at level 200, x binder, y binder, right associativity).
Definition Var := Set.
Existing Class Var.
Inductive term `{V: Var}: Set :=
| var (x: V)
| O: term
| S: term → term
| add: term → term → term
.
Fixpoint const `{Var} n :=
if n is Datatypes.S n'
then S (const n')
else O.
Infix "+" := add.
Inductive prop `{V:Var}: Set :=
| true
| false
| and (P Q: prop)
| or (P Q: prop)
| impl (P Q: prop)
| colim (P: term → prop)
| lim (P: term → prop)
| eq (e e': term)
.
Notation "⊤" := true.
Notation "⊥" := false.
Infix "∧" := and.
Infix "∨" := or.
Infix "→" := impl.
Notation "¬ P" := (impl P false).
Notation "P ↔ Q" := (and (impl P Q) (impl Q P)).
Notation "'∃' x .. y , P" := (colim (λ x, .. (colim (λ y, P)) .. )).
Notation "'∀' x .. y , P" := (lim (λ x, .. (lim (λ y, P)) .. )).
Infix "=" := eq.
Notation "P ≠ Q" := (eq P Q → ⊥).
Definition unique `{Var} P := ∀ x y, P x → P y → x = y.
Definition colim_unique `{Var} P := colim P ∧ unique P.
Notation "'!' x .. y , P" := (unique (λ x, .. (unique (λ y, P)) .. )).
Notation "'∃!' x .. y , P" := (colim_unique (λ x, .. (colim_unique (λ y, P)) .. )).
Inductive entail `{V: Var}: prop → prop → Prop :=
| id: Reflexive entail
| compose {A B C}: B ⊢ C → A ⊢ B → A ⊢ C
| bang P: P ⊢ ⊤
| absurd P: ⊥ ⊢ P
| fanout {P Q R}: P ⊢ Q → P ⊢ R → P ⊢ (Q ∧ R)
| π1 {P Q}: (P ∧ Q) ⊢ P
| π2 {P Q}: (P ∧ Q) ⊢ Q
| fanin {P Q R}: P ⊢ R → Q ⊢ R → P ∨ Q ⊢ R
| i1 {P Q}: P ⊢ P ∨ Q
| i2 {P Q}: Q ⊢ P ∨ Q
| curry {P Q R}:
Q ∧ P ⊢ R →
P ⊢ (Q → R)
| uncurry {P Q R}:
P ⊢ (Q → R) →
Q ∧ P ⊢ R
| colim_intro {P} e: P e ⊢ ∃ x, P x
| colim_elim {P} {B}:
(∀ x, P x ⊢ B) →
(∃ x, P x) ⊢ B
| lim_elim {P} e: (∀ x, P x) ⊢ P e
| lim_intro {P} {Q}:
(∀ x, Q ⊢ P x) →
Q ⊢ ∀ x, P x
| refl: ⊤ ⊢ ∀ x, x = x
| sym: ⊤ ⊢ ∀ x y, x = y → y = x
| trans: ⊤ ⊢ ∀ x y z, x = y → y = z → x = z
| S_subst: ⊤ ⊢ ∀ x y, x = y → S x = S y
| S_injective:
⊤ ⊢ ∀ x y, S x = S y → x = y
| S_distinct:
⊤ ⊢ ∀ x, S x ≠ O
| add_O_r: ⊤ ⊢ ∀ m, m + O = m
| add_S_r: ⊤ ⊢ ∀ m n, m + S n = S (m + n)
| induction P:
P O ∧ (∀ n, P n → P (S n)) ⊢ ∀ n, P n
where "P ⊢ Q" := (entail P Q).
Infix "∘" := compose (at level 30).
Infix "⊢" := entail.
Existing Instance id.
Instance entail_Transitive `{Var}: Transitive entail.
Proof.
intros ? ? ? f g.
exact (g ∘ f).
Qed.
Notation "⟨ x , y , .. , z ⟩" := (fanout .. (fanout x y) .. z).
Instance and_Proper `{Var}: Proper (entail ==> entail ==> entail) and.
Proof.
intros ? ? f ? ? g.
exact ⟨ f ∘ π1 , g ∘ π2 ⟩.
Defined.
Instance or_Proper `{Var}: Proper (entail ==> entail ==> entail) or.
Proof.
intros ? ? f ? ? g.
exact (fanin (i1 ∘ f) (i2 ∘ g)).
Defined.
Instance impl_Proper `{Var}: Proper (Basics.flip entail ==> entail ==> entail) impl.
Proof.
unfold Basics.flip.
intros ? ? f ? ? g.
apply curry.
rewrite f.
rewrite <- g.
apply uncurry.
reflexivity.
Defined.
Instance colim_Proper `{Var}: Proper (pointwise_relation _ entail ==> entail) (@colim _).
Proof.
intros ? ? f.
apply colim_elim.
intro e.
rewrite f.
apply colim_intro.
Defined.
Instance lim_Proper `{Var}: Proper (pointwise_relation _ entail ==> entail) (@lim _).
Proof.
intros ? ? f.
apply lim_intro.
intro e.
erewrite lim_elim.
apply f.
Defined.
Ltac xtaut := refine (_ ∘ bang _).
Ltac xabsurd := refine (absurd _ ∘ _).
Ltac xsplit := refine ⟨ _, _ ⟩.
Ltac xcase := refine (fanin _ _).
Ltac xleft := refine (i1 ∘ _).
Ltac xright := refine (i2 ∘ _).
Ltac xfirst := refine (_ ∘ π1).
Ltac xsecond := refine (_ ∘ π2).
Ltac xcurry := refine (curry _).
Ltac xuncurry := refine (uncurry _).
Ltac xlim_elim := refine (_ ∘ lim_elim _).
Ltac xlim_intro x := refine (lim_intro (λ x, _)).
Ltac xcolim_intro := refine (colim_intro _ ∘ _).
Ltac xcolim_elim x := refine (colim_elim (λ x, _)).
Definition eval `{Var} {P Q}: P ∧ (P → Q) ⊢ Q := uncurry (id _).
Fixpoint arguments `{V:Var} (xs: list (option term)) (P: prop) :=
match xs with
| cons x nil =>
match x, P with
| Some x, lim _ => ⊤
| None, P → _ => P
| _, _ => ⊥
end
| cons x xs' =>
match x, P with
| Some x, lim P => arguments xs' (P x)
| None, P → Q => P ∧ arguments xs' Q
| _, _ => ⊥
end
| nil => ⊤
end.
Fixpoint instance `{V:Var} (xs: list (option term)) (P: prop) :=
if xs is cons x xs'
then
match x, P with
| Some x, lim P => instance xs' (P x)
| None, _ → Q => instance xs' Q
| _, _ => ⊤
end
else
P.
Lemma spec `{V:Var} xs:
∀ {P},
P ∧ arguments xs P ⊢ instance xs P.
Proof.
induction xs.
all: cbn.
all: intros.
1: xfirst.
1: reflexivity.
destruct a, P.
all: try (exact (bang _)).
all: try rewrite <- IHxs.
all: try xsplit.
- xfirst.
rewrite (lim_elim t).
reflexivity.
- xsecond.
destruct xs.
all: reflexivity.
- destruct xs.
1: rewrite ⟨π2, π1⟩.
1: rewrite eval.
1: reflexivity.
rewrite ⟨π1 ∘ π2, π1⟩.
exact eval.
- destruct xs.
all: cbn.
1: apply bang.
1: xsecond.
1: xsecond.
reflexivity.
Qed.
Lemma app `{Var}:
∀ {P},
⊤ ⊢ P →
∀ xs,
arguments xs P ⊢ instance xs P.
Proof.
intros ? f xs.
rewrite <- (spec xs).
xsplit.
2: reflexivity.
exact (f ∘ bang _).
Qed.
Example add_O_l `{Var}: ⊤ ⊢ ∀ m, O + m = m.
Proof.
rewrite <- (induction _).
xsplit.
- eassert (p := app add_O_r [Some _]).
cbn in p.
apply p.
- xlim_intro x.
xcurry.
xfirst.
eassert (p := app add_S_r [Some O; Some x]).
cbn in p.
eassert (q := app trans [Some (O + S x); Some _; Some (S x); None; None]).
cbn in q.
rewrite <- q.
clear q.
xsplit.
+ rewrite <- p.
apply bang.
+ eassert (q := app S_subst [Some _; Some _; None]).
cbn in q.
rewrite <- q.
clear q.
reflexivity.
Qed.
