1090 lecture notes 1-6 PDF

Preview

Summary

All chapters from 1 to 6 has some examples too...

Description

Section 1.1 Boolean Formulate Symbols for boolean or propositional variables p,q,r with or without primes or subscripts Ex: p,p’(prime),p123,q’’45 Symbols for boolean constant T called top, verum, or symbol “True” ⊥ called bottom, falsum, symbol “False” Brackets, ( and ) A string (or word, or expression) over a given alphabet is ordered sequence of the alphabet’s symbols, written adjacent to each other without any visible separators (no commas or spaces, etc) (P V ⊥) Is a string (P~Q) not a string -> p)q( two different strings given the boolean alphabet. Only ordering different (P -> Q) Is a string

String Variables Denoted by A B C with or without primes or subscripts Concatenation Ex: if A is abc and B is de then AB is abcde or BA is deabc Formula Calculation (Procedural Definition) Formula calculation is any finite (ordered) sequence of strings that we may write respecting the following requirements: 1. At any step we may write a Boolean variable or a Boolean constant 2. At any step we may write (not A) provided we have already written string A in a previous step 3. At any step we may write any of the strings (A ^B) (A V B) (A->B) (A=B) provided we have already written strings A and B in a previous step Well formed formula A string A over the Boolean alphabet is called a Boolean expression or a well formed formula iff it is a string written at some step of some formula calculation. WFF: set of all well formed formulae (wffs)

Which are wffs (T) Not a wff P V Q not a wff because no brackets Not symbol not a wff (T->(not(P->Q))) wff (p^q) wff ⊥ wf Prove (p^q) and (T->(not(P->Q))) are both wff: 1. P 2. Q 3. (p^q) 1. T P Q 2. (p->q) 3. (not(P->q)) 4. (T->(not(P->Q))) Formula Calculation Bottom up parsing Identify which of the following are valid formula calculations P,q,r, ((notP)≡(notQ))) No Q,r, (q≡r), (not q),p, (not p), ((not p ≡ (not q)), (((not p ≡ (not q)) ≡ (q ≡ r))

Yes P,q, (p^q), (not q), (p V (not q)), (p V (not q)) -> (p^q) No ● Variables can be defined anywhere Recursive definition of WFF The set of all well-formed formulae is the smallest set of strings Wff that satisfies 1. All boolean variables p,q,r and constants T, ⊥ 2. If A and B are any strings in WFF, then so are the strings (not A), (A ^B), (A V B), (A->B), (A ≡ B) Top down parsing of a wff is showing the recursive formula calculation steps The two definitions for WFF are equivalent Well formed formula Prove (p ^ q) and ((T->(not(P->Q))) are both wff using top-down parsing:

Removing Brackets Redundant Brackets Outermost brackets are redundant Any pair of brackets is redundant if its presence can be understood from the priority of the connectives ] Priorities The order of priorities (decreasing) is agreed to be not, ^, V, →, ≡

For same connectives, the rightmost has the highest priority Least parenthesize notation (LPN): writing wff with all redundant brackets removed Note writing wff in LPN is just a short notation and is not a correctly written formula (by formula calculation) Immediate Predecessors (I.P.) 1. Boolean variables or constants don’t have any immediate predecessors 2. A is an immediate predecessor of (not A) 3. A and B are IP of (A^B),(AVB),(A→ B),(A≡B) What are the IP of (T → (not(p→ q))) T and not(p→ q) Complexity The complexity of a formula is the number of connectives occurring in the formula The complexity of Boolean variables and constants is zero (also called atomic formulae) Ex Complexity of ((pVr) → (notq)) is 3 What is the complexity of (T → (not(p→ q))) is 3

1.2 Induction On The Complexity Of WFF Simple Induction On Natural Numbers P(n): Some property of the natural number n Goal: Prove that P(n) holds for all nEN (or prove P(n) is true for arbitrary n) Induction: Basis: Prove that p(0) holds Induction Step: Assume Induction Hypothesis (I,H) p(k) holds for k=n-1 Then prove P(n) holds

Prove 0+1+2+3+...+n = (n(n+1))/2 Basis Step: p(0)= (0(0+1))/2=0 Induction Step: Assume True for n=k 0+1+2+3+...+k = (k(k+1))/2 Show true for n=k+1 0+1+2+3+...+k+1 = ((k+1)(k+2))/2 if 0+1+2+3+...+k = (k(k+1))/2 (k(k+1))/2 +k+1= ((k+1)(k+2))/2 (k(k+1))/2 +2(k+1)/2= ((k+1)(k+2))/2 //times by 2 so all the denominator is 2 k(k+1)+(k+1)=(k+1)(k+2) k^2+k+2k+2=k^2+2k+k+1 Ls=Rs Strong Induction p(n): Some property of the natural number N Goal: Prove that P(n) holds for all nEN (or prove P(n) is true for arbitrary n) Induction: Basis:Prove that P(0) holds Induction Step: Assume Induction Hypothesis (I.H) P(k) holds for all k=0 Let p(x) be the property that x has the same number of left and right brackets Proof by induction on formula Basis step: Prove for x an atomic formula (n=0) Suppose X is an atomic formula, then x is a boolean variable or Boolean constant and hence has no brackets specifically x has 0 left brackets and 0 right brackets. Since 0=0 P(x) holds Induction Step: IH assume that for any wff a of complexity k,≡} These formulae have first symbol “(” left bracket and hence never have first symbol negation as

required

1.3 Inductive Definitions of Formulae Truth values: t(true), f(false) These symbols are not in Boolean alphabet and they never appear in a wff Definition, A state v is a function Assigns the value f or t to each Boolean variable, while It assigns necessarily the value f to the constant ⊥ It assigns necessarily the value t to the constant T This definition gives values to atomic formula only A state v is an infinite table Boolean Semantics Tables describing five functions, called Boolean functions, that take inputs from the set {f,t} and return values in the same set Not Or And Implies Equivalent

Definition (Value of a formula in a state v)

Infinite vs. Finite Tables A state v is by definition an infinite table Intuitively, the value of a formula A in any state v should depend only on the values of the variables that occur in A. For any formula A we therefore truncate the state into a finite appropriate table Proposition if v and v’ are two stages that agree on the variables of A, then v(A) = v’(A) Occurrence of a Variable Definition (Occurrence of a variable) Atomic case: p occurs in p, and does not occur in q,T,⊥ (where q is a diferent variable from p) P occurs in (not A) iff it occurs in A P occurs in (A o B), oE (^,V,->,≡), iff it occurs in A or B or both Tautology/ Satisfiable/ Contradiction Definition, A formula is a tautology iff it is true (t) in all possible states. This is denoted by |=tautA Definition A formula A is satisfiable iff there is at least one state v where v(A)=t Definition A formula A is unsatisfiable or a contradiction off for every state v, we have v(A)=f Definition. A set of formulae Γ is satisfiable iff there is at least one state v where for every formula A in Γ, v(A)=t. We say v satisfies Γ Definition Γ tautologically implies a iff for every state v that satisfies Γ, we must have v(A)=t.

This is denoted by Γ |=tautA Formulae in set Γ are called the hypotheses or premises A is called the conclusion

1.3 Substitution in formulae We will define an operation denoted by A[p:=B] A[p:=B] means substitute or replace every boolean variable p occurring in the formula A, by formula B A[p:=B] is a schema in the metatheory that stands for the string (in fact wff) we get after performing this operation This operation has the highest priority over all Boolean connectives It is left-associative (apple the left occurrence of this operation first)

Proposition For any formulae A and B and variable p, A[p:=B] is a formula in other words it is a wff Provable by induction Proposition if p does not occur in A then A[p:=B] is A(unchanged) Provable by induction 1.4 Proofs and Theorems Schemata A schema is a string over the following augmented alphabet: -The set if Boolean alphabet(V) union - {[,:=, ]} union - {A,B,C…} union } - {p,q,...} } Syntactic variables If we replace all syntactic variables in a schema with any formula or Boolean variable, we will obtain a wff. This formula would be an instance of the schema

1.4 Logical Axioms of Boolean Logic

Axioms We will use the capital Greek Letter “lambda” Λ to denote the set of all logical axioms Note that since the logical axioms are schemata, Λ is infinite All assumption or hypothesis for a specific problem are called special axioms or nonlogical axioms and are denoted by gamma Γ Note that Γ is not fixed 1.4 Rules of Inference and Theorem Calculation Primary Rules of Inference

The numerator shows the premises hypotheses or assumptions The denominator shows the conclusion or result of the rule The first rule is the rule Equanimity or Eqn requires two hypothesis The second rule is the Leibniz rule or Leib requires one hypothesis Theorem Calculation or Γ-proofs ‘Let Γ be given set of formulae (our assumptions) A theorem-calculation (or proof) from Γ is any finite (ordered) sequence of formulae that can be written following these rules 1. We may write a formula from ^ or Γ at any step 2. We must write the denominator of an instance of an inference rule provided all formulae in the numerator (of the same instance) have been written in a previous step Theorem Definition Any formula A that appears in a Γ-proof is called a Γ-theorem. This is denoted by Γ |- A The above proof is said to prove A from Γ. If Γ=0(empty set) we write |- A and call a just a theorem or an absolute theorem or logical theorem A Γ-proof is also called a hilbert proof Hilbert Style Proof-Framework

Annotations explain the step written in a proof In a Hilbert style proof, the conclusion appears at the last step (although by definition, it is not wrong to have more (unnecessary!) steps) Ex |-A V -A 1) AV-A (axiom) A |- A 1) A (hyp) A, A≡B |-B 1) A(hyp) 2) A≡B (hyp)

3) B A≡B |- C[p:=A] ≡ C[p:=B] 1) A≡B (hyp) 2)C[p:=A] ≡ C[p:=B] (Leib on 1)

A≡B, B≡C |- A≡C 1) A≡B (hyp) 2) B≡C (hyp) 3) (A≡B) ≡ (A≡C) ((2) + Lieb, C-part (A≡p), p-fresh) 4) A≡C ((1),(3),Eqn) |- (A≡(B≡C)) ≡ ((A≡B)≡C) 1) ((A≡B)≡C) ≡ (A≡(B≡C)) (axiom 1) 2) (((A≡B)≡C) ≡ (A≡(B≡C))) ≡ (A≡(B≡C)) ≡ ((A≡B)≡C) (axiom 2) 3) (A≡(B≡C)) ≡ ((A≡B)≡C) ((1),(2),Eqn) |- A V ⊥ ≡A 1) -A ≡ A ≡ ⊥ (axiom 4) 2) A V -A (axiom 9) 3) A V -A ≡ A V (A≡ ⊥) ((1)+Leib- C -part AvP, p fresh) 4) A V (A≡⊥) ((2)+(3) +Eqn) 5) (A V (A≡⊥)) ≡ (A V A ≡ A V ⊥) (axiom dist-of v over ≡) 6) A V A ≡ A V ⊥ ((4),(5), Eqn) 7) A ≡ A V ⊥ (axiom 7 AVA≡A + Lieb +Eqn + (6) +C-part) 8) (A V A ≡(A V ⊥)) ≡ (A ≡(Av⊥)) (Axiom 7 +Lieb C-part) 9) A ≡ Av⊥ ((6)+(8)+Eqn) 10) (A≡ Av⊥) ≡ (Av⊥ ≡ A) (axiom symmetry) 11) Av⊥≡A (9+10,Eqn) |- T ≡ A ≡ A 1) T ≡ (⊥≡⊥) (axiom) 2) ⊥≡⊥≡A≡A (Absolute Theorem) 3) T≡A≡A ((1),(2), Transitivity)

p≡A V ⊥

2.1 Logic Vs. Metatheory -

Inside Logic Vs. The Metatheory Formula calculations and theorem calculations occur inside Logic A theorem inside logic is simply a well-formed formula We will often abuse notation and use symbols outside of logic as a shortcut to ask you to write a Γ proof of a E.g prove Γ |- A Γ |- A is technically a statement in the metatheory and meta theorems are theorems about logic We will use meta theorems to help us take shortcuts in writing proofs

Strengthening Metatheories

2.2-2.4 Introduction to Equational Proof An Equational style proof is a proof of the form

Framework For Equational Style Proof

To prove |- A we use Template 2 or 3 To prove Γ |- A use Template 2 or 3 2,3 an axiom or a hypothesis or proven theorem

2.5 Using Special Axioms In Equational Proofs Redundant True Theorem |- T ≡ A ≡ A and |- A ≡ A ≡ T Redundant True Metatheorem For any Γ and A, Γ |- A if Γ }- A≡T Special case: A |- A ≡ T Using hypothesis (special axioms in Equational proofs) A |- A ≡ T Therefore using leibniz one can replace occurrences of hypothesis A by T Conversely any occurrence of T can be replace by A

Splitting and Merging Hypotheses A, B |- A ^ B A v A |- A A |- A v B A ^ B |- A

Equatinal Style Proof:

|- A v ⊥ ≡ A A v -A (-A≡A≡⊥ + Leib, C-part Avp p Fresh) Av(A≡⊥) (Axiom: Dist of v over ≡) AvA ≡ Av⊥ ⇔ (axiom: AvA≡A + Leib C-part p≡Av⊥ p fresh) A≡ Av⊥ (axiom: symmetry of ≡ ) Av⊥≡A Write a Hilbert style proof for the following. ⊢((AvB)≡¬A→B)→A

2.6 The Deduction Theorem Metatheorem. (Deduction Theorem) If ΓU{A} |- B, then also Γ |- A → B. Lemma. A → (B≡C) |- A → (D[p:=B]≡ Dp:=C]) Corollary Γ+A |-B iff Γ|-A → B 3.5 Resolution Definitions (Literal) Atomic formulae and their negation also formula variables and their negation are literals. (-B) Ex. p (-p) (-⊥) A (Clause) A clause is a disjunction of literals Ex pv-p -⊥vAv-B Resolution (1) 1 Using Deduction and proof by contradiction to move everything to the assumption side and have ⊥ on the conclusion side If Γ+A |-B then Γ|-A → B If Γ+-A|-⊥ then Γ|-A

Deduction Theorem Proof by contradiction

In other words instead of proving Γ|-A → B it is sufficient to prove Γ+{A,-B} |- ⊥

2 remove and ≡ using Ping-pong A≡B≡(A → B)^(B → A)

Ping pong theorem

3 remove and → using implication theorem A → B ≡ -AvB Implication theorem 4 Move negation inwards using deMorgan -(A^B) ≡ -Av-B De Morgan 1 -(AvB) ≡ -A^-B De Morgan 2 5 Distribute v over ^ Av(B^C) ≡ (AvB) ^ (AvC)

distributivity of v over ^

6 split ^ A^B |-A and A^B |-B

split

7 use cut rule to prove ⊥ AvB, -AvC |- BvC A, -A |- ⊥

Cut rule 1 Cut rule 2

3.1 Soundness Soundness: our Boolean logic is sound and truthful. Everything we can prove using the Boolean Logic is actually true. Completeness: Our boolean logic is complete. Everything that is true(and can be represented in Boolean logic) can be be proved using the boolean logic Soundness The primary rules of inference are truthful i.e.

All logical axioms are tautologies Metatheorem (soundness of propositional calculus)

Corollary if |- A then |=taut A

4.1 The First Order Of Predicate Logic Nonlogical symbols Zero or more object constans Ex: 1,1000,{1},{1,2,3},{} Denoted generally as a,b,c with or without primes or subscripts Zero or more functions Ex: +,-intersection,union Denoted generally as f g h with or without primes or subscripts Zero or more preducates Ex: >, 0) Terms Atomic terms (complexity=zero) More complex terms(complexity>0) Term calculation(term parse) A term calculator is and finite and ordered sequence of strings that we may write respecting the following rules 1) At any step we may write and object variable or and object constant 2) At any step for a function f of arity n we may write ft1 t2 tn provided that t1 t2 tn are terms written in a previous step Complexity of terms Def :the completion of a term is defined to be the number of function symbols We will use the symbols t and s to denote terms Since ft1t2tn is not familiar we sometimes write is as f(t2,t2,tn) but note this is not the formal definition Just like the boolean formula definition we can define terms recursively as well Top down and bottom up parse for terms Atmoic formulae Atomic formula of predicate logic are - Boolean variables or constants - The string s=t for and terms t and s - The string p t1t2tn for some predicate p with arity n and terms t1t2tn The complexity of the above formula is zero

Formula calculation (formula-parse)

Well formed formula Def: a string a over the alphabet introduced for predicate logic is a first order formula or a well formed formula wff iff it is a string written at some step of some formula calculation. Wff is used to denote the set of all wffs Def: the complexity of a wff is the total number of occurrences of upside down A, not, and, or, implies, equivalent in the formula Recursive definition of wff

Def: Subformulae B is subformula if a iff 1) B is identical to a or 2) A is not C and b is a subformula of C or 3) A is CoD and B is a subformula of c or d or both 4) A is Ax c and b is a subformula of C A subformula is a wff

Terms, Term Calculation, and Complexity z is a term TermCalculation z w+z is not a term Hwz is a term w,z,hwz p not a term pvq not a term f gygxy is a term TermCalculation x,y,gx,gy,fgygxy

Complexity 0 Complexity 1

Complexity 3

Which are valid First Order formula Calculation Yes Complexity2 p,q,⊥,(pvq),((pvq)≡⊥) x,y,fxy x=y,p,⊥,(pv(x=y)),((pv(x=y)) → ⊥) No because of (x=y) extra brackets fxy=z,⊥,p,(-fxy=z),((∀x)fxy=z),(((∀x)fxy=z)^p) No 2 for the last x,y,x=y,((∀y)x=y),((∀x)((∀y)x=y)) No 2 for the last

(((∀z)(p → x=z))^q) x=z,p,q,(p → x=z),((∀z)(p → x=z)),(((∀z)(p → x=z))^q) Complexity 3 → ∀ ^ Bound and free Occurrences of Variables ((∀x)((∀y)x=y)) Bound (((∀y)y=fx)v((-q)^z=0) ((∀x)x...