Hilbert System axiom dependency in Coq

terrible-axiom.pdf

terrible-axiom.png

terrible-axiom.v

(* Here we use the Coq proof assistant to show that in the basic
   Hilbert System for propositional logic, the axiom schema P1 is
   derivable from the other three axioms (actually even just from the
   second and third axioms) and the inference rule, modus ponens. *)

(* Formulas can be constructed using "~>" (implication), "-,"
   (negation), and atoms drawn from some set of atoms (these latter
   are irrelevant for our purposes). *)

Parameter atom : Set.

Inductive formula : Type :=
| f_not  : formula -> formula
| f_imp  : formula -> formula -> formula
| f_atom : atom -> formula.

Notation "-, F" := (f_not F) (at level 75, right associativity).
Notation "F ~> G" := (f_imp F G) (at level 95, right associativity).

(* We have a single inference rule, namely Modus Ponens. *)

Inductive proof : formula -> Prop :=
| ponens : forall F G,
               proof (F ~> G) -> proof F
               -> proof G.

(* Here is the statement of Axiom P1 of the Hilbert System, though we
   do not posit it as an axiom as we wish to prove it from P2 and
   P3. *)

Definition P1_statement :=
  forall F,
    proof (F ~> F).

(* Here are P2 through P4. *)

Axiom P2 :
  forall F G,
    proof (F ~> (G ~> F)).

Axiom P3 :
  forall F G H,
    proof ((F ~> (G ~> H)) ~> ((F ~> G) ~> (F ~> H))).

Axiom P4 :
  forall F G,
    proof ((-, F ~> -, G) ~> (G ~> F)).

(* And here is theorem P1, solved easily by the magic of eapply!
   Comments are included to demonstrate that this was done quite
   mindlessly indeed. *)

Theorem P1 : P1_statement.
Proof.
  intro F.  (* Assume we have a formula F. *)
  eapply ponens.  (* P2 and P3 fail to match so we choose ponens. *)
  eapply ponens.  (* P2 also matches but results in an obligation to
                     prove F, which is impossible, so we choose
                     ponens. *)
  eapply P3.  (* P2 also matches but results in an obligation to prove
                     F ~> F, which has gotten us nowhere.  ponens
                     always matches but discharging the obligation
                     with an axiom is preferable to extending the
                     proof search further with another application of
                     ponens. *)
  eapply P2.  (* P3 fails to match, P2 preferable to ponens. *)
  eapply P2.  (* P3 fails to match, P2 preferable to ponens. *)
  (* At this point we're done, except that we still have an unfilled
     gap ("existential variable") which is not bound by any
     constraints; it needs to be instantiated to some formula. We can
     choose for example F, though any formula would do. *)
  Existential 1 := F.
Qed.  (* Done! *)

(* Let's look at the actual proof object we got. *)

Print P1.

(* The output, re-indented for clarity:

P1 = 
fun F : formula =>
ponens (F ~> F ~> F) (F ~> F)
       (ponens (F ~> (F ~> F) ~> F) ((F ~> F ~> F) ~> F ~> F)
               (P3 F (F ~> F) F)
               (P2 F (F ~> F)))
       (P2 F F)
     : P1_statement

And here is the proof tree we get as a result (see accompanying PDF
and/or PNG for a typeset version):

\[
\infer[\textsc{(Ponens)}]{F \to F}{
  \infer[\textsc{(Ponens)}]{(F \to F \to F) \to F \to F}{
    \infer[\textsc{(P3)}]{(F \to (F \to F) \to F) \to (F \to F \to F) \to F \to F}{} &
    \infer[\textsc{(P2)}]{F \to (F \to F) \to F}{}
  } &
  \infer[\textsc{(P2)}]{F \to F \to F}{}
}
\]

*)