In this talk we will focus on the problems and the solutions we encountered when building the Partial Predicate Calculus as an object-logic for Isabelle.
Items such as three-valued logic, syntax vs. semantics, hypsubstfun, quantifiers, classical reasoner and sequents will be discussed.