20.2.2019 16:00 @ Applied Mathematical Logic
The uniform interpolation property of the intuitionistic propositional calculus (IPC) was first proved by Pitts in 1992 by means of proof-theoretic methods. We prove an open mapping theorem for the topological spaces dual to finitely presented Heyting algebras. In turn, this yields a short, self-contained semantic proof of Pitts result. Our proof is based on the methods of Ghilardi & Zawadowski. However, it does not require sheaves nor games, only basic duality theory for Heyting algebras. This is joint work with Sam van Gool.
27.2.2019 16:00 @ Applied Mathematical Logic
Recall that in natural deduction each primitive constant is equipped with introduction and elimination rules. Such rules can be given not only for the logical connectives and the quantifiers, but also for the identity predicate: its introduction rule is the reexivity axiom, t = t, and its elimination rule is the indiscernibility of identicals. Although a normalization theorem can be proved for the resulting system, one might not be entirely satisfied with this treatment of identity, especially if one adheres to the idea|going back to Gentzen| that the meaning of a primitive constant is determined by its introduction rule(s). Firstly, it is not obvious that the introduction rule for the identity predicate is strong enough to justify its elimination rule. Secondly, it is not clear what to say about definitions taking the form of equations. Such definitions are usually regarded as axioms, hence they must be additional introduction rules for the identity predicate. Since definitions are particular to theories, it follows that the meaning of the identity predicate changes from one theory to the other. I will show that by enriching natural deduction with a theory of definitional identity we can answer both of these worries: we can justify the elimination rule on the basis of the introduction rule, and we can extend any theory with definitions while keeping the reexivity axiom as the only introduction rule for the identity predicate.
