POPL Tutorial/Sequent vs Natural Deduction

In this exercise, we will present rules for natural deduction and for a sequent calculus presentation of intuitionistic logic, and give an two incomplete proofs. The first establishes that derivability in natural deduction implies derivability in the sequent calculus, the second establishes the converse.

There are two tasks:

• Complete the three cases of the natural deduction -> sequent calculus proof relating to conjunction.
• Complete the three cases of the sequent calculus -> natural deduction proof relating to implication and cut.

The solution is here.

Syntax for Propositions

%sort prop %.
%name prop %.
%term top prop %.
%term and %pi prop %-> prop %-> prop %.
%term imp %pi prop %-> prop %-> prop %.

Natural Deduction Inference Rules

Natural deduction deals with a single judgment, $\texttt{true}~A$.

%sort true {_ prop} %.

Six rules describe a natural deduction system for the language considered here.

%term topI true top %.
%term andI %pi (true (and A B)) %<- (true B) %<- (true A) %.
%term andE1 %pi (true A) %<- (true (and A B)) %.
%term andE2 %pi (true B) %<- (true (and A B)) %.
%term impI %pi (true (imp A B)) %<- (%pi (true A) %-> (true B)) %.
%term impE %pi (true B) %<- (true (imp A B)) %<- (true A) %.

Sequent Calculus

With the same grammar of propositions, we can define a sequent calculus with different judgments for the left and the right of the sequent ($\texttt{hyp}~A$ for the left and $\texttt{conc}~A$ for the right).

%sort hyp {_ prop} %.
%sort conc {_ prop} %.

This particular sequent calculus includes the cut rule. We can show separately that it is possible to eliminate all uses of cut by proving the admissibility of cut.

%term init %pi (conc A) %<- (hyp A) %.
%term topR conc top %.
%term andL %pi (%pi (hyp (and A B)) %-> (conc C)) %<- (%pi (hyp A) %-> (hyp B) %-> (conc C)) %.
%term andR %pi (conc (and A B)) %<- (conc B) %<- (conc A) %.
%term impL %pi (%pi (hyp (imp A B)) %-> (conc C)) %<- (conc A) %<- (%pi (hyp B) %-> (conc C)) %.
%term impR %pi (conc (imp A B)) %<- (%pi (hyp A) %-> (conc B)) %.
%term cut %pi (conc B) %<- (conc A) %<- (%pi (hyp A) %-> (conc B)) %.

The natural deduction system exists in a world with arbitrary assumptions $\texttt{hyp}~A$.

%block bhyp [A prop] {H hyp A}%.

Translation: Natural Deduction to Sequent Calculus

The following (incomplete) proof establishes that whenever a proposition is true in the natural deduction system, it is derivable as a conclusion in the sequent calculus.

The cases for top and implication are filled in for you; all that remains is the cases for conjunction.

The -impI case provides and example of using a theorem case. You will need something similar in the translation for the other direction.

TASK 1: Fill in the three missing cases for conjunction

%sort nd-to-seq {_ true A} {_ conc A} %.
%mode nd-to-seq %in %out %.
%scope nd-to-seq %term top nd-to-seq topI topR %.
%term andI nd-to-seq ((%abs andI) (%the (true A) DtrueA) (%the (true B) DtrueB)) XXX %.
% fill in here.
% fill in here.
%scope nd-to-seq %term andE1 nd-to-seq ((%abs andE1) (%the (true (and A B)) DtrueAB)) XXX %.
%term andE2 nd-to-seq ((%abs andE2) (%the (true (and A B)) DtrueAB)) XXX %.
% fill in here.
%scope nd-to-seq %term impI
  %pi (nd-to-seq ((%abs impI) ([dA true A] %the (true B) (Dimp dA))) (impR ([hA hyp A] DconcB hA)))
  %<- ({dA true A} {hA hyp A} {dtrans nd-to-seq dA (init hA)} nd-to-seq (Dimp dA) (%the (conc B) (DconcB hA))) %.
%term impE
  %pi (nd-to-seq ((%abs impE) (%the (true A) DtrueA) (%the (true (imp A B)) DtrueAB)) (cut (impL ([hB hyp B] init hB) DconcA) DconcAB))
  %<- (nd-to-seq DtrueA (%the (conc A) DconcA))
  %<- (nd-to-seq DtrueAB (%the (conc (imp A B)) DconcAB)) %.
%block truetohyp [A prop] {DA true A} {HA hyp A} {Dtrans nd-to-seq DA (init HA)}%.
%worlds (truetohyp) (nd-to-seq _ _) %.
%total D (nd-to-seq D _) %.

Translation: Sequent Calculus to Natural Deduction

The following (incomplete) proof establishes that whenever a proposition is derivable as a conclusion in the sequent calculus, it is true in the natural deduction system.

TASK 2: Complete the theorem with cases for implication and cut

%sort hyp-to-true {_ hyp A} {_ true A} %.
%mode hyp-to-true %in %out %.
%block hyptotrue [A prop] {HA hyp A} {DA true A} {Dtrans hyp-to-true HA DA}%.
%worlds (hyptotrue) (hyp-to-true _ _) %.
%total {} (hyp-to-true _ _) %.
%sort seq-to-nd {_ conc A} {_ true A} %.
%mode seq-to-nd %in %out %.
%scope seq-to-nd %term init
  %pi (seq-to-nd ((%abs init) (%the (hyp A) DhypA)) DtrueA)
  %<- (hyp-to-true DhypA (%the (true A) DtrueA)) %.
%term top seq-to-nd (%the (conc (%abs top)) topR) topI %.
%scope seq-to-nd %term andR
  %pi (seq-to-nd (%the (conc (and A B)) ((%abs andR) (%the (conc A) DconcA) (%the (conc B) DconcB))) (andI DtrueA DtrueB))
  %<- (seq-to-nd DconcA (%the (true A) DtrueA))
  %<- (seq-to-nd DconcB (%the (true B) DtrueB)) %.
%term andL
  %pi (seq-to-nd (%the (conc C) ((%abs andL) ([hA hyp A] [hB hyp B] %the (conc C) (DconcC hA hB)) (%the (hyp (and A B)) Hab))) (DtrueC (andE1 DtrueAB) (andE2 DtrueAB)))
  %<- ({hA} {dA true A} {dtransA hyp-to-true hA dA} {hB} {dB true B} {dtransB hyp-to-true hB dB} seq-to-nd (DconcC hA hB) (%the (true C) (DtrueC dA dB)))
  %<- (hyp-to-true Hab (%the (true (and A B)) DtrueAB)) %.
%% fill in here
%scope seq-to-nd %term impR seq-to-nd (%the (conc (imp A B)) ((%abs impR) ([hA] %the (conc B) (DconcB hA)))) XXX %.
%term impL seq-to-nd ((%abs impL) ([hB hyp B] %the (conc C) (DconcC hB)) (%the (conc A) DconcA) (%the (hyp (imp A B)) Hab)) XXX %.
%% fill in here
%% fill in here
%scope seq-to-nd %term cut seq-to-nd ((%abs cut) ([hA hyp A] %the (conc B) (DconcB hA)) (%the (conc A) DconcA)) XXX %.
%worlds (hyptotrue) (seq-to-nd _ _) %.
%total D (seq-to-nd D _) %.

Solution