second order propositional logic

logical verification week 11 2004 11 24

the course

1st order propositional logic ↔ simple type theory

λ→

1st order predicate logic ↔ type theory with dependent types

λP

2nd order propositional logic ↔ polymorphic type theory

λ2

2nd order propositional logic

propositional logic

a b c … A → B ⊥ ⊤ ¬A A ∧ B A ∨ B

predicate logic

\begin{matrix}a & (…) & b & (…) & c & (…) & … \\ A → B \\ ⊥ \\ ⊤ \\ ¬A \\ A ∧ B \\ A ∨ B \\ ∀x . & A \\ ∃ x . & A \end{matrix}  \begin{matrix}x y z … \\ f(…) & g & (…) & h & (…) & … \end{matrix}

second order propositional logic

a b c … A → B ⊥ ⊤ ¬A A ∧ B A ∨ B

∀a . A
∃ a . A

example

a → a ∀a. a → a

if it’s tuesday, then it’s tuesday

for every proposition, that proposition implies itself

the rules

introduction rules  elimination rules
I[x]→  E→
E⊥

I⊤

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

propositional logic: rules for implication

implication introduction

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

implication elimination

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

propositional logic: rules for falsum and truth

falsum elimination

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

truth introduction

\overline{⊤} I⊤

propositional logic: rules for conjunction

conjunction introduction

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

conjunction elimination

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

propositional logic: rules for disjunction

disjunction introduction

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

disjunction elimination

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

2nd order propositional logic: rules for universal quantification

universal quantification introduction

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

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

universal quantification elimination

\frac{⋮ ; ∀a. A}{A[a := B]} E∀

2nd order propositional logic: rules for existential quantification

existential quantifier introduction

\frac{⋮ ; A[a := B]}{∃a. A} I∃

existential quantifier elimination

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

variable condition: a not a free variable in B

variable conditions

• for rule I∀ check: variable does not occur in any of the available assumptions

• for rule E∃ check: variable does not occur in the conclusion

example 1_{(∀b. b) → a}^{examples}

14

example 2_{a → ∀b. ((a → b) → b)}

15

example 3_{(∃b. a) → a}

16

example 4_{∃b.((a → b) ∨ (b → a))}

17

example 5

∀a. ∀b. ((a → b) ∨ (b → a))

this needs classical logic

∀a. (a ∨ ¬a)

non-example 6

a → ∀a. a

(∃a. a) → a

higher order logic

the ‘order’ of a variable

first order  object
second order  set of objects

predicate on objects

function from objects to objects

third order  set of second order objects

predicate on predicates on objects

function from second order objects to …

etc.

example from 2nd order predicate logic

induction principle for natural numbers

∀a. (a(0) → (∀m. a(m) → a(S(m))) → ∀n. a(n))
m 1st order variable
n 1st order variable
0 1st order constant
a 2nd order variable
S 2nd order constant

only predicates without arguments

quantify over predicates  → 2nd order predicate logic
… the same without terms → 2nd order propositional logic

impredicative encoding of inductive types

the connectives in Coq

→ hard-wired into the type theory
∀ hard-wired into the type theory
⊥ inductive type
∧ inductive type
∨ inductive type
∃ inductive type

inductive definition of False

Inductive False : Prop :=
  .

                   False_ind : ∀a. ⊥ → a

the constructors are the introduction rules the induction principle is the elimination rule

inductive definition of and

Inductive and (a b : Prop) : Prop :=

conj : a → b → a ∧ b .

and_ind : ∀a b c. (a → b → c) → (a ∧ b) → c

the constructor is the introduction rule the induction principle gives the elimination rules

alternative version of conjunction elimination

conjunction elimination: alternative version

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

conjunction elimination: normal version

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

inductive definition of or

Inductive or (a b : Prop) : Prop :=
  or_introl : a → a ∨ b
| or_intror : b → a ∨ b .

or_ind : ∀a b c. (a → c) → (b → c) → (a ∨ b) → c

the constructors are the introduction rules the induction principle is the elimination rule

impredicative definition of False

⊥ := ∀a. a

induction principle next to impredicative definition

\begin{matrix}∀a. ⊥ → a \\ ∀a. a \end{matrix}

impredicative definition of and

a ∧ b := ∀c. (a → b → c) → c

induction principle next to impredicative definition

\begin{matrix}∀a b. ∀c. (a ∧ b) → (a → b → c) → c \\ ∀c. (a → b → c) → c \end{matrix}

impredicative definition of or

a ∨ b := ∀c. (a → c) → (b → c) → c

induction principle next to impredicative definition

\begin{matrix}∀a b. ∀c. (a ∨ b) → (a → c) → (b → c) → c \\ ∀c. (a → c) → (b → c) → c \end{matrix}

impredicative definitions for other inductive types

impredicative definition of the booleans

∀a. a → a → a

impredicative definition of the natural numbers

∀a. a → (a → a) → a

why have inductive types as primitive then?

• one can prove less equalities

• one gets weaker induction principles

• some people don’t like impredicativity