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 axiomsisTh() =all'derivable fromThe 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)x0 = 0xS(y) = (xy)+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, y1);gless( x, y )fif( y == 0 ) return false;return ( x == y1)jjless( x, y1);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=yz!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