This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic (...) with implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

This book is a thesis submitted to the Faculty of Arts of the University of Utrecht. It was prepared under the supervision of Prof. Dr. H. Schultink. I would like to express my gratitude to him for his criticisms of earlier versions which led to many improvements, in particular with respect to the exposition of the argument. To my co-referent Dirk van Dalen, reader in the Department of Philo sophy (,Centrale Interfaculteit') of the University of Utrecht, I am greatly (...) indebted for his valuable and fruitful suggestions about problems relevant to both linguistics and logic. Several ideas developed in this study owe their present concrete form to our many discussions. This thesis originates in syntactic research into the Aspects carried out in 1967 under the supervision of Albert Kraak, professor at the University of Nijmegen, who ever since gave much attention to my work in progress. I am very grateful to him for his careful and stimulating criticism as well as for the continuous support he gave me during these years. The present study closely relates to the work of my colleague Wim Klooster with regard to both its theoretical framework and its subject matter. Our joint work on the measurement of duration in Dutch is an integral part of the argument. I have greatly profited from the numerous discussions we have had. (shrink)