28 June 2019, Colloquium on Mathematical Logic, Makoto Fujiwara

Abstract:

Brouwer’s intuitionistic mathematics is an origin of modern constructive mathematics which allows only constructive reasoning in the proofs.In 1930’s, Brouwer’s student A. Heyting introduced so-called Heyting arithmetic (HA) with an informal semantics, called the Brouwer-Heyting-Kolmogorov(BHK) interpretation, which works as a criterion for the constructive reasoning thereafter.Note that HA is based on intuitionstic logic and one can obtain classical arithmetic (PA) just by adding the law of excluded middle (A or not A) into the axioms of HA.Though the sentences provable in HA are valid in the (informal) sense of the BHK interpretation, it seems not that all the sentences valid in the BHK interpretation are provable in HA.Thus some weak fragment of the law of excluded middle can be contained in the arithmetic which exactly obey the BHK interpretation.Based on this situation, I have studied the structure (derivability relation) of weak logical principles over Heyting arithmetic and its extension in all finite types.The weak logical principles are closely related to various kinds of realizability, which can be seen as formal treatments of the BHK interpretation.In fact, to show that one logical principle A does not imply another principle B, one typically uses appropriate forms of realizability to show that A has a certain semi-constructive interpretation which B does not.In this talk, I would present the structure of the weal logical principles and discuss about the relation with the variations of realizability.If time permits, I would also talk briefly about a recent attempt to establish a general method to use Kripke models which separate intermediate logics for the separation of the logical principles over Heyting arithmetic.

For more information, see https://www.staff.science.uu.nl/~ooste110/seminar.html or contact Benno van den Berg at B.vandenBerg3 at uva.nl.