DOC PREVIEW
CMU CS 15398 - Lecture

This preview shows page 1-2-3 out of 10 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 10 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 10 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 10 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 10 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Axioms and TheoriesOne important use of predicate logic is to pin down the properties mathematical objects. You fix alanguage, and a collection of formulae, so-called axioms, and then study all the models of theseformulae.In a while, we will generalize our deduction rules to predicate logic. The theory associated with aset of axiomsisTh() =all'derivable fromThe formulae inTh()are called theorems.ISince our deduction rules are sound, any formula inTh()is valid in all models for.In other words, one single proof covers all models, we do not have to bother to prove the same factover and over again in countless different models of the axioms.IUsually try to keep axiom set small (ideally finite, at least very simple structure).1Peano Arithmetic (PA)We useL(+;;S;0;<)and omit the universal quantifiers.Sstands for the successor function,S(x) =x+1.IPeano AxiomsS(x)6= 0S(x) =S(y)!x=yx+0 =x x+S(y) =S(x+y)x0 = 0xS(y) = (xy)+x:(x <0)x < S(y),x=y_x < yInduction Axiom:'(0)^8x('(x)!'(S(x)))! 8x'(x)The “Induction Axiom” is actually a so-called schema: there is one axiom for any formula'.All elementary number theory can be handled within this axiom system.2Computational AspectsThe Peano axioms are almost like programs.In particular, the axioms provide recursive definitions of plus, times and less-than in terms of thesuccessor functionS.add( x, y )fif( y == 0 ) return x;return S( x, y1);gless( x, y )fif( y == 0 ) return false;return ( x == y1)jjless( x, y1);g3A Theorem of (PA)Claim:8x(0 +x=x)Proof.Consider the formula'(x)(0 +x=x).Then'(0)is the first addition axiom (more precisely, replacexby0there).Now assume'(x). Then by the second addition axiom0+S(x) =S(0 +x) =S(x)Hence we have shown'(0)^8x('(x)!'(S(x))).By the Induction Axiom and modus ponens we get8x'(x).Likewise, one can prove8x; y ; z(x+(y+z) = (x+y)+z)8x; y(x+y=y+x)Hence, it follows from the Peano axioms thathN;+;0iis associative, commutative, and has anidentity.4Primes in Peano ArithmeticRemember our formula that expresses primality?'(x)S(0)< x^8y; z(x=yz!x=y_x=z)With some more effort one could derive from(PA)8x9y(x < y^'(y))In other words, there are infinitely many primes.Likewise, one can show in(PA)that every number can be decomposed uniquely into a product ofprimes, and so on.All results of basic arithmetic can be deduced from just(PA).IHence we have a very succinct representation of the essential features of arithmetic: just 8axioms and one axiom schema (induction).5Recall: Natural Deduction RulesAnd ^ ^i^ ^e1^ ^e2Or_ _i1 _ _i2_ []....[ ]....(_e)Implication ! (!e): ! :(!mt)[].... ! (!i)Double negation::(::e)::(::i)Falsum?(?e): ?(?i)6Derivations in Predicate LogicWe need to augment our deduction rules. We keep all the rules from propositional logic, and addrules for the quantifiers.Intuitively, we would like to use(t)9x(x)(9i)9x(x)(c)(9e)(x)8x(x)(8i)8x(x)(t)(8e)wherexis a variable,ca constant, andta term.ICorrect in spirit.Alas, as stated these rules are not sound.7CounterexampleSuppose we adopt the quantifier rules from above. Then we can perform the following derivation.8x9y(x < y)premise9y(x < y)8e(x < c)9e8x(x < c)8i9y8x(x < y)9iIDisaster!The premise is valid overN, but the conclusion is not. This is exactly the wrong direction of thevalid implication9x8y'(x; y)! 8y9x'(x; y)The problem is that thecreally depends onx.To address this and similar problems, one has to add certain technical conditions to the quantifierrules.8Amended Quantifier RulesA termtis substitutable forxin'(x)iff no variable intbecomes bound in'(t).(t)9x(x)(9i)wheretis substitutable forxin'.9x(x)['(x)].... (9e)wherexis not free in , and does not occur in active assumptions.(x)8x(x)(8i)wherexis not free in any assumptions for'.8x(x)(t)(8e)wheretis substitutable forxin'.9ExampleAn example for a correct derivation, according to our rules:9x('(x)! (x))` 8x'(x)! 9x (x)This is valid (our structures are never empty).Here is the proof tree:[8x'(x)]'(x)(8e)['(x)! (x)] (x)(!e)9x (x)(9i)8x'(x)! 9x (x)(!i)9x('(x)! (x))8x'(x)! 9x


View Full Document

CMU CS 15398 - Lecture

Download Lecture
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 Lecture 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 Lecture 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?