Quantifiers in the World of Types
J.F.A.K. van Benthem, J. van Eyck, J. van der Does · UvA-DARE (University of Amsterdam) · 1995
or itself. 2 In a common notation with Boolean inclusion, this would read as: 'f1 Ÿ ... Ÿ fn ≤ y ' . 3 Actually, from the type-theoretic point of view, having arbitrary base domains of 'truth values', with appropriate operations over these, would be quite admissible too. 4 This calculus has been chosen for its meta-logical convenience, not for its practical utility. For instance, proving the Boolean 'conjunction rule' from two conclusions to their conjunction already requires a trick: Suppose that D• at = 1, D• bt = 1 . By Boolean Algebra and Substitution of Identicals, at = 1, bt = 1 • at Ÿ 1 = 1 • (at Ÿ bt) = 1 . Hence, by Cut and Contraction, D• (at Ÿ bt) = 1 . 5 The principles preceding them are merely some useful derived facts, allowing one to represent the binary quantifier some as a unary one in the usual manner. 6 The reason is that, since only finitely many possibilities exists for interpreting a Boolean operator, the usual ultraproduct proof for Compactness will still go through: one unique interpretation will be enforced in the ultrafilter. 7 Here is an illustration. The formula ¬(pŸ¬Fq) is monotone in F . By the recipe given, it must be equivalent, after some Boolean simplification, to the disjunction of F(0)ŸF(1), F(1)Ÿ¬(pŸ¬q), F(0)Ÿ¬(pŸq), ¬p . And the latter may be reduced again to the obvious equivalent ¬p⁄Fq . 8 There are many further subtleties to the process of 'argument management' in natural language, where, e.g., identifications must be lexicalized to a large extent. See the various discussions on this topic in van Benthem 1991, as well as the treatment of Boolean coordination in Sanchez Valencia 1990. 9 By way of example, the procedure may be applied to the earlier form xxy . What we get then for the case of y , is the disjunction of '0Oy'Ÿxx0, '1Oy'Ÿxx1 , which is indeed equivalent to the earlier form (xx1Ÿy) ⁄ xx0 . For the case of x , the result obtained reduces to that obtained via the earlier procedure for predicate logic, namely to something like (x1Ÿx0) ⁄ (x1Ÿy) ⁄ (x0Ÿy) , which is again equivalent to the one found 'by hand'. 10 It will still work, of course, for purely Boolean objects even in a an {e, t}-type environment, witness the earlier case of truth-functional operators in predicate logic.