Equivalence of natural deduction, hilbert calculus, and sequent calculus

Executable Specification

[View equiv.sig] [View equiv.mod]
sig equiv.

kind     form                    type.

type     imp                     form -> form -> form.

type     nd, hil, conc, hyp      form -> o.

module equiv.

% Natural deduction
nd (imp A B) :- nd A => nd B.      % implies introduction
nd B :- nd (imp A B), nd A.        % implies elimination

% Hilbert calculus
hil (imp A (imp B A)).                                   % K combinator
hil (imp (imp A (imp B C)) (imp (imp A B) (imp A C))).   % S combinator
hil B :- hil (imp A B), hil A.                           % Modus ponens

%% Sequent calculus
conc A :- hyp A.                                     % init
conc B :- hyp A => conc B, conc A.                   % cut

conc (imp A B) :- hyp A => conc B.                   % impR
conc C :- hyp (imp A B), conc A, hyp B => conc C.    % impL


[View equiv.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "equiv".

%% Contexts

Define ctxs : olist -> olist -> olist -> prop by
  ctxs nil nil nil ;
  ctxs (nd G :: L) (hyp G :: J) (hil G :: K) := ctxs L J K.

Theorem ctxs_member1 : forall L J K E,
  ctxs L J K -> member E L ->
    exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K.

Theorem ctxs_member2 : forall L J K E,
  ctxs L J K -> member E J ->
    exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K.

Theorem ctxs_member3 : forall L J K E,
  ctxs L J K -> member E K ->
    exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J.

%% Natural deduction -> sequent calculus

Theorem nd_to_seq_ext : forall L J K G,
  ctxs L J K -> {L |- nd G} -> {J |- conc G}.

Theorem nd_to_seq : forall G,
  {nd G} -> {conc G}.

%% Sequent calculus -> hilbert calculus

Set witnesses on.
Theorem hil_deduction : forall L J K A B,
  ctxs L J K ->
  {K, hil A |- hil B} -> {K |- hil (imp A B)}.
Set witnesses off.

Theorem seq_to_hil_ext : forall L J K G,
  ctxs L J K -> {J |- conc G} -> {K |- hil G}.

Theorem seq_to_hil : forall G,
  {conc G} -> {hil G}.

%% Hilbert calculus -> natural deduction

Theorem hil_to_nd_ext : forall L J K G,
  ctxs L J K -> {K |- hil G} -> {L |- nd G}.

Theorem hil_to_nd : forall G,
  {hil G} -> {nd G}.

%% The general form of the Hilbert deduction theorem:
%%   if   {hil A1, hil A2, ..., hil An |- hil B}
%%   then {hil (imp A1 (imp A2 (imp ... (imp An B)...)))}

Define fold : olist -> form -> form -> prop by
  fold nil B B ;
  fold (hil A :: L) B B' := fold L (imp A B) B'.

Theorem hil_deduction_generalized : forall L J K B B',
  ctxs L J K ->
  fold K B B' -> {K |- hil B} -> {hil B'}.