 However, some critics have questioned the cogency of Church’s philosophical arguments for his requirement of effectiveness (Anderson 1998). Moreover, it should be noted that logical consequence is not in general an effective notion. By Church’s Theorem (1936a), there is no effective test for deciding the validity or provability of the wffs of first order logic or of logics of any higher order (as Church himself notes; 1956–71 [BE: 703]). Further, as Church was acutely aware, there is a price to be paid for communicating and verifying proofs in a formalized language that meets the requirement of effectiveness. If the formalized language is sufficiently expressive, it will be subject to Gödel’s incompleteness theorems (see  §5.4).