First-order Logic 2.5 2001/11/13 2002/07/04 Ian Barland ian@cs.rice.edu Ian Barland ian@cs.rice.edu Peggy Fidelman peggy@rice.edu first-order for all proof quantifier there exists waterworld We replace long lists of particular statements with a few general statements, involving the quantifiers "for all" and "there exists". We see how this changes our proofs, and rules of inference. The information in this module is outdated. Please see my course for a table of contents.

quantifiers - statements we'd like to express: "every neighbor of x is unsafe", or "if num(x) = 3, then every neighbor of x is unsafe". "There is a safe square ... that is a neighbor of x ... if num(x)<3". - Not just games -- can express properties about type-checking, data structures (trees, ...), circuits, ... - exercises - negation of quantifiers. - vacuously true. - multiple quantifiers - alternation of quantifiers -exercises - meaning of; again stress the sentence vs the model - new proofs; new proof rules introduced as needed . pushing negations through quantifiers - re-visit: how this changes how we model waterworld & its deductions - optional: minimal sets of connectives; of deductions rules; when we cavalierly added new proof rules, were we just solving our own straw-man problem?

Why not begin with quantifiers We saw three stages of logics: Propositional logic, with statements like ... Predicate logic, where the same statement was phrased as .... This introduced the idea of variables, which ranged over atomic propositions. First-order logic, which included quantifiers; the above statements were superceded with the likes of .... So why, you might ask, didn't we just start out with first-order logic in the first lecture? One reason, clearly, is to introduce concepts one at a time: everything you needed to know about one level was needed in the next, and then some. But there's more: by restricting our formalisms, we can 't express all the concepts of the bigger formalism, but we can have automated ways of checking statements or finding proofs. In general, this is a common theme in the theory of any subject: determining when and where you can (or, need to) trade off expressibility for predictive value. For example, ... Linguistics: Having a set of precise rules for (say) Tagalog grammar allows you to determine what is and isn't a valid sentence; details of the formal grammar can reveal relations to other languages which aren't otherwise so apparent. On the other hand, a grammar for any natural language is unlikely to exactly capture all things which native speakers say and understand. If working with a formal grammar, one needs to know what is being lost and what is being gained. Dismissing a grammar as irrelevant because it doesn't entirely reflect usage is missing the point of the grammar; conversely, condemning some real-life utterances as ungrammatical (and ignoring them) forgets that the grammar is a model which captures many (if not all) important properties. Of course, any reasonable debate on this topic respects these two poles, and is actually about where the best trade-off between them lies. One example from psychology: Say, Piaget might propose four stages of learning in children. It may not trade off total accuracy, for (say) clues of what to look for in brain development. physics: trade off quantum accuracy for newtonian approximations, in large-scale. Or, trade off exact simulations for statistical ("stochastic") approximations. Understanding the theoretical foundations of a field is often critical for knowing how to apply various techniques in practice.