# References for intuitionistic meta-logic?

It seems to me that arguments about logical theories itself are often done using classical logic. For example, one says that a theorem is provable or not provable, which is not automatically valid without law of excluded middle.

Are there references for study of logic from the viewpoint of intuitionism? Or maybe there are immediate problems and such an approach wouldn't make any sense?

Intuitionistic logic is currently studied... and "it works".

Some books dedicated to intuitionism :

Arend Heyting, 1956, Intuitionism: An Introduction, Amsterdam: North-Holland Publishing (3rd revised ed, 1971)

Anne Sjerp Troelstra and Dirk van Dalen, 1988, Constructivism in Mathematics: An Introduction, Amsterdam: North-Holland Publishing

Michael Dummett, 1977, Elements of Intuitionism (Oxford Logic Guides, 39), Oxford: Clarendon Press (2nd edition, 2000)

Grigori Mints, 2000, A Short Introduction to Intuitionistic Logic, KLUWER ACADEMIC PUBLISHERS.

For a "standard" textbook in math log with a chapter about intuitionistic logic, see :

Dirk van Dalen, Logic and Structure (5th ed - 2013), Chapter 6: Intuitionistic Logic.

• Thanks for the references, but I was more specifically looking for intuitionistic proofs for statements in logic, like completeness theorems and the incompleteness theorem. This kind of statements are sometimes about intuitionistic logic, but their proofs seem to be in classical logic. Maybe I should edit the question for this to be more clear. – Jens Hemelaer Apr 4 '14 at 15:37
• @JensHemelaer - for this, you must start from Proof-Theoretic Semantics and the Bibliography there; at least : Per Martin-Löf and Dag Prawitz. – Mauro ALLEGRANZA Apr 4 '14 at 15:48
• @JensHemelaer - Godel's Incompleteness Th is proved constructively; thus it is acceptable also from an intuitionsitic point of view. G's Completeness Th is base on "set-theoretic" semantics (the notion of validity) and its proof is non-constructive (it needs at least Konig's lemma). Reagrding the Completenss results for intuitionistic logic based on Kripke semantics, I do not know them in details: it is necessary to see the details of the proof itself to check what kind of "resources" are used. – Mauro ALLEGRANZA Apr 4 '14 at 15:53
• @JensHemelaer - see also Melvin Fitting, Intuitionistic logic Model theory and Forcing (1969). – Mauro ALLEGRANZA Apr 6 '14 at 20:18
• @JensHemelaer - see in A.S. Troelstra and D.Dalen, Chapter 2: Logic : Section 5 [page 75-on] is dedicated to Kripke semantics; there are the completeness results, with discussion about the fact that "The completeness proofs given rely on classical metamathematics" (page 87) and a Remark taht "It is possible to remove the classical steps in the argument, for example via a formalization of the completeness theorem (see Smorynski 1982)." – Mauro ALLEGRANZA Apr 7 '14 at 8:39