DOC PREVIEW
CORNELL CS 2800 - Syntax of First Order Logic

This preview shows page 1-2-15-16-31-32 out of 32 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Syntax of First-Order LogicWe have :• constant symbols: Alice, Bob• variables: x, y, z, . . .• predicate symbols of each arity: P , Q, R, . . .◦ A unary predicate symbol takes one argument:P (Alice), Q(z)◦ A binary predicate symbol takes two arguments:Loves(Bob,Alice), Taller(Alice,Bob).An atomic expression is a predicate symbol togetherwith the appropriate number of arguments.• Atomic expressions act like primitive propositions inpropositional logic◦ we can apply ∧, ∨, ¬ to them◦ we can also quantify the variables that appear inthemTypical formula:∀x∃y(P (x, y) ⇒ ∃zQ(x, z))1Semantics of First-Order LogicAssume we have some domain D.• The domain could be finite:◦ {1, 2, 3, 4, 5}◦ the people in this room• The domain could be infinite◦ N, R, . . .A statement like ∀xP (x) means that P (d) is true for eachd in the domain.• If the domain is N, then ∀xP (x) is equivalent toP (0) ∧ P (1) ∧ P (2) ∧ . . .Similarly, ∃xP (x) means that P (d) is true for some d inthe domain.• If the domain is N, then ∃xP (x) is equivalent toP (0) ∨ P (1) ∨ P (2) ∨ . . .Is ∃x(x2= 2) true?Yes if the domain is R; no if the domain is N.How about ∀x∀y((x < y) ⇒ ∃z(x < z < y))?2First-Order Logic: Formal SemanticsHow do we decide if a first-order formula is true? Need:• a domain D (what are you quantifying over)• an interpretation I that interprets the constants andpredicate symbols:◦ for each constant symbol c, I(c) ∈ D∗ Which domain element is Alice?◦ for each unary predicate P , I(P ) is a predicate ondomain D∗ formally, I(P )(d) ∈ {true,false} for each d ∈ D∗ Is Alice Tall? How about Bob?◦ for each binary predicate Q, I(Q) is a predicate onD × D:∗ formally, I(Q)(d1, d2) ∈ {true,false} for eachd1, d2∈ D∗ Is Alice taller than Bob?• a valuation V associating with each variable x an el-ement V (x) ∈ D.◦ To figure out if P (x) is true, you need to knowwhat x is.3Now we can define whether a formula A is true, given adomain D, an interpretation I, and a valuation V , writ-ten(I, D, V ) |= A• Read this from right to left, like Hebrew: A is true at(|=) (I, D, V )The definition is by induction:(I, D, V ) |= P (x) if I(P )(V (x)) = true(I, D, V ) |= P (c) if I(P )(I(c))) = true(I, D, V ) |= ∀xA if (I, D, V0) |= A for all valuations V0that agree with V except possibly on x• V0(y) = V (y) for all y 6= x• V0(x) can be arbitrary(I, D, V ) |= ∃xA if (I, D, V0) |= A for some valuationV0that agrees with V except possibly on x.4Translating from English toFirst-Order LogicAll men are mortalSocrates is a manTherefore Socrates is mortalThere is two unary predicates: Mortal and ManThere is one constant: SocratesThe domain is the set of all people∀x(Man(x) ⇒ Mortal(x))Man(Socrates)—————————————–Mortal(Socrates)5More on Quantifiers∀x∀yP (x, y) is equivalent to ∀y∀xP (x, y)• P is true for every choice of x and ySimilarly ∃x∃yP (x, y) is equivalent to ∃y∃xP (x, y)• P is true for some choice of (x, y).What about ∀x∃yP (x, y)? Is it equivalent to ∃y∀xP (x, y)?• Suppose the domain is the natural numbers . Com-pare:◦ ∀x∃y(y ≥ x)◦ ∃y∀x(y ≥ x)In general, ∃y∀xP (x, y) ⇒ ∀x∃yP (x, y) is logically valid.• A logically valid formula in first-order logic is the ana-logue of a tautology in propositional logic.• A formula is logically valid if it’s true in every domainand for every interpretation of the predicate s ymbols.6More valid formulas involving quantifiers:• ¬∀xP (x) ⇔ ∃x¬P (x)• Replacing P by ¬P , we get:¬∀x¬P (x) ⇔ ∃x¬¬P (x)• Therefore¬∀x¬P (x) ⇔ ∃xP (x)• Similarly, we have¬∃xP (x) ⇔ ∀x¬P (x)¬∃x¬P (x) ⇔ ∀xP (x)7Bound and Free Variables∀i(i2> i) is equivalent to ∀j(j2> j):• the i and j are bound variables, just like the i, j innXi=1i2ornXj=1j2What about ∃i(i2= j):• the i is bound by ∃i; the j is free. Its value is uncon-strained.• if the domain is the natural numbers, the truth of thisformula depends on the value of j.8Axiomatizing First-Order LogicJust as in propositional logic, there are axioms and rulesof inference that provide a sound and c omplete axioma-tization for first-order logic, independent of the domain.A typical axiom:• ∀x(P (x) ⇒ Q(x)) ⇒ (∀xP (x) ⇒ ∀xQ(x)).A typical rule of inference is Universal Generalization :ϕ(x)———-∀xϕ(x)G¨odel proved completenes s of this axiom system in 1930.9Axiomatizing ArithmeticSuppose we restrict the domain to the natural numbers,and allow only the standard symbols of arithmetic (+, ×,=, >, 0, 1). Typical true formulas include:• ∀x∃y(x × y = x)• ∀x∃y(x = y + y ∨ x = y + y + 1)Let P rime(x) be an abbreviation for∀y∀z((x = y × z) ⇒ ((y = 1) ∨ (y = x)))• P rime(x) is true if x is primeWhat does the following formula say:• ∀x(∃y(y > 1 ∧ x = y + y) ⇒∃z1∃z2(P rime(z1) ∧ P rime(z2) ∧ x = z1+ z2))• This is Goldbach’s conjecture: every even numberother than 2 is the sum of two primes.◦ Is it true? We don’t know.Is there a nice (technically: recursive, so that a programcan check whether a formula is an axiom) sound and com-plete axiomatization for arithmetic?• G¨odel’s Incompleteness Theorem: NO!10Logic: The Big PictureA typical logic is described in terms of• syntax: what are the legitimate formulas• semantics: under what circumstances is a formulatrue• proof theory/ axiomatization: rules for proving aformula true Truth and provability are quite different.• What is provable depends on the axioms and inferencerules you use• Provability is a mechanical, turn-the-crank process• What is true depends on the semantics11Tautologies and Valid ArgumentsWhen is an argumentA1A2...An——Bvalid?• When the truth of the premises imply the truth of theconclusionHow do you check if an argument is valid?• Method 1: Take an arbitrary truth assignment v.Show that if A1, . . . , Anare true under v (v |= A1,. . . v |= An) then B is true under v.• Method 2: Show that A1∧. . . ∧An⇒ B is a tautology(essentially the same as Method 1)◦ true for every truth assignment• Method 3: Try to prove A1∧ . . . ∧ An⇒ B using asound axiomatization12Graphs and TreesGraphs and trees come up everywhere.• We can view the interne t as a graph (in many ways)◦ who is connected to whom• Web search views web pages as a graph◦ Who points to whom• Niche


View Full Document

CORNELL CS 2800 - Syntax of First Order Logic

Download Syntax of First Order Logic
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Syntax of First Order Logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Syntax of First Order Logic 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?