Skip to main content

5. Predicate Logic

21/10/22 Lecture conducted by a tutor

Prove propositions using tactics

  • assume & applying for \to, ¬
  • constructor & cases for ^
  • left/right & cases for v
  • constructor for true
  • cases for false Intuitonistic logic: prove theorems by combining... Classical logic: use magic (em & raa)

Types​

#check ℕ - \bn, natural numbers 0,1,2,.... #check bool - tt,ff #check list ℕ

Types are like sets Types have terms (elements)

#check 3
#check tt
#check [3,4,5]

Predicates and Relations​

Predicates (properties of elements)​

Prime : ℕ → Prop Prime 3 : -- Prop, Prime 4: Prop isZero : ℕ → Prop

def isZero : ℕ → Prop | 0 := true | _ := false
#check isZero
#check isZero 0
#check isZero 4
#check isZero 3

Relations (Predicates with several inputs)​

le : ℕ → (ℕ → Prop) le 2 3 means 2 is less or equal to 3

#check 2 ≤ 3
#check 5 ≤ 3

A relation for every type: equality

#check 3 = 3
#check 3 = 4

namespace social - Non-mathematical example: type of social media access constant Account : Type - Predicate: is this account a bot? constant isBot : Account → Prop - Relation: the 'follows' relation follows acc1 acc2 means that acc1 follows acc2

constant follows : Account → Account → Prop
constant account1 : Account
constant account2 : Account
#check account1 = account2

Quantifiers​

∀ : universal quantifier (\forall) #check ∀ x : Account , isBot x

∃ : existential quanitifier (\exists) #check ∃ x : Account, isBot x

Can use quantifiers in definition

def haveCommonFollower (acc1 acc2 : Account) : Prop
  := ∃ acc3 : Account, follows acc3 acc1 ∧ follows acc3 acc2
#check haveCommonFollower

def fakeFollowing (acc : Account) : Prop
  := ∀ acc' : Account, follows acc' acc → isBot acc'
#check fakeFollowing

end social

∀ x : A, (∃ x : A ..x..) .. x .. scope, shadowing

variables A B C : Type
variables P Q R : Prop
variables PP QQ : A → Prop

example : (∀ x : A, PP x) → (∀ y : A, PP y → QQ y) → (∀ z : A, QQ z) :=

begin
  assume h g z,
  apply g,
  apply h,
end


example : (∃ x : A, PP x) → (∀ y : A, PP y → QQ y) → (∃ z : A, QQ z) :=
begin
  assume h g,
  cases h with z pz,
  existsi z,
  apply g,
  exact pz,
end

Example Proofs​

example : (∀ x : A, PP x ∧ QQ x) ↔ (∀ x : A, PP x) ∧ (∀ x : A, QQ x) :=
begin
  constructor,
  assume h,
  constructor,
  assume x,
  have f : PP x ∧ QQ x,
  apply h,
  cases f with px qx,
  exact px,
  assume x,
  have f: PP x ∧ QQ x,
  apply h,
  cases f with px qx,
  exact qx,
  assume h x,
  cases h with Px Qx,
  constructor,
  apply Px,
  apply Qx,
end