If you want something like first-order predicate calculus but need several ‘types’ each using its own sort of variable here is how to re-do your propositions so as to appear as ordinary PC (predicate calc) and also convert your proofs.
To transform multi-type to unitype
It takes only a little work to transform the proofs from multi type logic to unitype logic.
- Invent a new predicate T for each type which will be deemed true for that type and false for all others.
- Recursively replace each instance of (∧x Φ) by
(∧x (Tx → Φ)) where the selected predicate T matches the type of the variable x.
We assume that existential quantifiers are defined in terms of universal quantifiers and they will be transformed thereby as well.