predicate logic

logical verification week 6 2004 10 13

advertisement

workshop in Nijmegen

Types for Mathematics / Libraries of Formal Mathematics

November 1–2, 2004

invited speakers Bruno Buchberger (of the Theorema system) Bob Constable (of the NuPRL system)

          http://www.cs.ru.nl/fnds/typesworkshop/
                  typesworkshop@cs.ru.nl

overview

from propositional to predicate logic

first order propositional logic ⟷ simply typed lambda calculus

type theory called λ→

first order predicate logic ⟷ type theory called λP
second order propositional logic ⟷ type theory called λ2

inductive types program extraction

applications of logic

• propositional logic logical circuits correctness of train track switching

• predicate logic software correctness ‘Hoare logic’ correctness of driverless metro in Paris

predicate logic

‘a logic’

• syntax of – terms

– formulas – judgments

• derivation rules

terms

• x

• f(M_{1}, …, M_{n}) symbols f taken from a fixed finite set of function symbols

formulas

• P (M_{1}, …, M_{n})

• ⊤

• ⊥

• ¬A

• A → B

• A ∧ B

• A ∨ B

• ∀x. A
• ∃x. A

symbols P taken from a fixed finite set of predicate symbols

random example

(∀x. ∃y. P (f(c, y)) ∧ Q(g(g(x)), y)) → (∃z. ∀w. ¬R(z, w)) here the signature is

function symbols {f, c, g, …}
predicate symbols {P, Q, R, …}

each symbol has an arity

the rules of predicate logic

introduction rules  elimination rules

I⊤

E⊥
I[x]¬  E¬
I[x]→  E→
I∧  El ∧ Er∧
Il ∨ Ir∨  E∨
I∀  E∀
I∃  E∃

rules for ⊤ and ⊥

⊤ introduction

\overline{⊤} I⊤

⊥ elimination

\frac{⋮ ; ⊥}{A} E⊥

rules for ¬

¬ introduction

\frac{[A^{x}] ; ⋮ ; ⊥}{¬A} I[x]¬

¬ elimination

\frac{⋮ ; ¬A  ⋮ ; A}{⊥} E¬

rules for →

→ introduction

\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→

→ elimination

\frac{⋮ ; A → B  ⋮ ; A}{B} E→

rules for ∧

∧ introduction

\frac{⋮ ; A  ⋮ ; B}{A ∧ B} I∧

∧ elimination

\frac{⋮ ; A ∧ B}{A} El∧  \frac{⋮ ; A ∧ B}{B} Er∧

rules for ∨

∨ introduction

\frac{⋮ ; A}{A ∨ B} Il∨  \frac{⋮ ; B}{A ∨ B} Il∨

∨ elimination

\frac{⋮ ; A ∨ B  ⋮ ; A → C  ⋮ ; B → C}{C} E∨

rules for ∀

∀ introduction

\frac{⋮ ; A}{∀x. A} I∀

variable condition: x not a free variable in any open assumption

∀ elimination

\frac{⋮ ; ∀x. A}{A[x := M]} E∀

rules for ∃

∃ introduction

\frac{⋮ ; A[x := M]}{∃x. A} I∃

∃ elimination

\frac{⋮ ; ∃x. A  ⋮ ; ∀x. (A → B)}{B} E∃

variable condition: x not a free variable in B

alternative versions of E∨ and E∃

∨ elimination

\frac{⋮ ; A ∨ B  [A] ; ⋮ ; C  [B] ; ⋮ ; C}{C}

∃ elimination

\frac{⋮ ; ∃x. A  [A] ; ⋮ ; B}{B}

variable condition: x not a free variable in B or any open assumption

minimal versus intuitionistic versus classical

• minimal predicate logic just the connectives → and ∀

• intuitionistic predicate logic the system just presented

• classical predicate logic

add any of A ∨ ¬A ¬¬A → A ((A → B) → A) → A (Peirce’s law)

empty domains

\frac{\overline{⊤} I⊤}{∃x. ⊤} I∃

∃x. ⊤ means

‘there exists an object x’

the I∃ rule is not valid when the domain is empty!

coq

terms

• x
• f M1 M2 . . . Mn

curried function application: not a first order system!

formulas

• P M1 M2 . . . Mn
• True
• False
• ~A
• A -> B
• A /\ B
• A \/ B
• forall x:D, A
• exists x:D, A

tactics

I[x]→ I∀  intro

 E→ E∀  apply

E⊥ El∧ Er∧ E∨ E∃  elim

       I∧  split
      Il∨  left
      Ir∨  right
       I∃  exists
       I⊤  exact I

examples

example 1

(∀x. P (x) → Q(x)) → (∀x. P (x)) → ∀y. Q(y)

example 2_{∀x. (P (x) → ¬(∀y. ¬P (y)))}

23

example 3_{(∃x. P (x) ∨ Q(x)) → (∃x. P (x)) ∨ (∃x. Q(x))}

24

variable conditions

∀ introduction

\frac{⋮ ; A}{∀x. A} I∀

variable condition: x not a free variable in any open assumption

∃ elimination

\frac{⋮ ; ∃x. A  ⋮ ; ∀x. (A → B)}{B} E∃

variable condition: x not a free variable in B

example 4: violates the variable condition of I∀

∀x. (P (x) → ∀x. P (x))

example 5: violates the variable condition of E∃

∀x. ((∃x. P (x)) → P (x))

detour elimination

detours

often called ‘cuts’

introduction rule of a connective

directly followed by the elimination rule of the same connective

detour elimination for →

\frac{\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→  ⋮ ; A}{B} E→ →  ⋮ ; A ; ⋮ ; B

‘proof of B using a lemma A’

detour elimination for ∧

\frac{\frac{⋮ ; A  ⋮ ; B}{A ∧ B} I∧}{A} El∧ →  ⋮ ; A

detour elimination for ∀

\frac{\frac{⋮ ; A}{∀x. A} I∀}{A[x := M]} E∀ →  \begin{matrix}⋮ & ∗ \\ A[x := M] \end{matrix}

∗ replace x everywhere by M

‘proof of A[x := M] from the generalization A’

decidability

a theorem by Gödel

• propositional logic provability is decidable

• predicate logic provability is undecidable

first order provers

• programs that search for proofs in predicate logic Otter Bliksem Vampire

E-SETHEO

…

• tactics that search for proofs in predicate logic coq: jprover

the CASC competition

CASC = CADE ATP System Competition
CADE = Conference on Automated Deduction
ATP = Automated Theorem Proving

yearly competition of first order provers this year the winner was: Vampire (solved 180 out of 200 problems)