Trying to understand "Deriving natural deduction rules from truth tables" and having trouble with false hypothetical judgments

Question

For rows of the truth table where the connective is false the connective is placed as a judgement. This doesn't make sense to me. Having the false proposition be in the hypothetical position makes more sense, as implication can be cast that way.

Answer 1

Herman Geuvers, one of the authors, answered over email:

There is a more philosophical explanation in

• P. Milne, Inversion Principles and Introduction Rules. In Dag Prawitz on Proofs and Meaning, volume 7 of Outstanding Contributions to Logic, pages 189–224. Springer, 2015, who devised the rules (from TT to ND and back) independently from us, for classical logic. It is based on Gentzen-Prawitz' "inversion principles" and there is much more literature on that referred to in Milne's paper and in our paper:
• Herman Geuvers and Tonny Hurkens, Proof Terms for Generalized Natural Deduction, In 23rd International Conference on Types for Proofs and Programs (TYPES 2017), editors A. Abel, F. Nordvall Forsberg and A. Kaposi, LIPIcs Vol 104, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018, pages 3:1--3:39. https://drops.dagstuhl.de/opus/volltexte/2018/10051/

a truth table row ...|0 for a formula Phi = c(A_1,..,A_n) corresponds to something like

(1) A_i, ..., ~A_j, ... |- ~Phi

whereas the corresponding elimination rule corresponds to something like

(2) for all Psi, (Phi, A_i, ..., (A_j -> Psi), ... |- Psi) 

which is equivalent to

(3) for all Psi, (A_i, ..., (A_j -> Psi), ... |- Phi -> Psi)

From a classical point of view, any Psi is either true or false, so equivalent to Top or Bot, and (3) holds trivially for Psi = Top, so classically (3) is equivalent to the special case Psi = Bot:

(4) A_i, ..., (A_j -> Bot), ... |- Phi -> Bot

which is equivalent to (1). But constructively, (1) only expresses the special case of applying the elimination rule to Psi = Bot. For example, the well-known elimination rule for disjunction Phi = A_1 \/ A_2, corresponding to the row 0,0|0 (in which the formula Phi is indeed false), corresponds to the theorem:

(5) for all Psi, (A_1 -> Psi) -> (A_2 -> Psi) -> Phi -> Psi

and not to just

(6) ~A_1 -> ~A2 -> ~Phi.

For example, by applying (5) to Psi = A_2 \/ A_1 we can derive Phi |- A_2 \/ A_1 which cannot be done constructively using just theorems like (6) that correspond to the rows of the truth table of connective \/.

Also note that there are many constructively definable connectives with the same truth table as a_1 \/ A_2 (like ~A_1 -> A_2 or ~(~A_1 /\ ~A_2)) for which our derivations rules derived from the truth table are NOT correct!