[FOM] invention of minimal logic

[Sara Negri]

Dear FOMers,

Sara Negri has again drawn my attention to a FOM discussion, this time  
on minimal logic. There is a wonderful correspondence between the  
inventor of minimal logic Ingebrigt Johansson and Arend Heyting that I  
have summarized in a book to appear next year as follows:


"The enormous step ahead in the study of intuitionistic logic brought  
by sequent calculus is seen clearly in the work of Ingebrigt  
Johansson. He had found Heyting's 1930 paper and wrote to him about  
his misgivings concerning the ex falso-axiom A & -A -> B, 'the magic  
works of a contradiction' as he called it. Johansson had made a very  
careful study of which results in Heyting's article depend on this  
axiom; just a few indeed, and in particular, the axiom is  
interderivable with (A V B) & -B -> A which latter he was not prepared  
to give up. In his answer, of 7 September 1935, Heyting recommends  
Johansson to study Gentzen's work. It took Johansson about two months  
to clear all things up and to write the well-known article about  
minimal logic that appeared in 1936. Here is his reasoning: By the  
disjunction property, if A V B is a theorem, either A or B is a  
theorem. If even -B is a theorem, the former must be the case, because  
predicate logic is consistent. Even if Johansson does not have a name  
for it, he had shown the modus tollendo ponens-rule (MTP) to be  
admissible, i.e., a rule the conclusion of which is derivable whenever  
its premisses are derivable, and this substitute of the full rule was  
enough for him. Johansson's further remarks contain: the ex  
falso-axiom holds in minimal logic for negative propositions, as in A  
& -A -> -B, and it is not needed if the law of excluded middle is  
admitted."

This is from the introduction to "Saved from the Cellar: Gerhard  
Gentzen's Shorthand Notes on Logic and Foundations of Mathematics."

Jan von Plato