the Poincaré principle versus reduction in the logic

Freek Wiedijk Radboud University Nijmegen

Types 2006 University of Nottingham 2006 04 19, 14:00

advertisement

Logic Colloquium 2006

Nijmegen, July 27 – August 2  http://www.cs.ru.nl/lc2006/

• tutorials Rodney Downey, algorithmic randomness and computability Ieke Moerdijk, introduction to algebraic set theory Boban Velickovic, forcing axioms

• special sessions computability theory / computer science logic / model theory / proof theory & type theory / set theory

• 14 plenary talks & many contributed talks

• plenary ‘100th birthday’ discussion on Gödel’s legacy

my discussion with Henk

the Poincaré principle

⊢ 2 + 2 = 4

Ce n’est pas une démonstration proprement dite, c’est une vérification. … La vérification diffère précisément de la véritable démonstration, parce qu’elle est purement analytique.

—Henri Poincaré, La Science et l’Hypothèse

This is not a demonstration properly so called; it is a verification. … Verification differs from proof precisely because it is analytical.

—Henri Poincaré, Science and Hypothesis logics for formalized mathematics

top 100 reduction in the logic Poincaré

• type theory

Coq  31  +  +
NuPRL  8  +  +
Agda  +  +
Plastic  +  +

• higher order logic

HOL Light  62  −  +
Isabelle/HOL  33  −  +
ProofPower  36  −  +
PVS  −  +

• set theory

Mizar  30  −  −
Isabelle/ZF  −  +
B method  −  −

• higher order set theory

Isabelle/HOLZF  −  +

type theory without reduction λP = LF

\frac{Γ ⊢ a : A  Γ ⊢ A′ : s}{Γ ⊢ a : A′} A =_{β} A′

λF explicit conversions

\frac{Γ ⊢ a : A Γ ⊢ H : A = A′}{Γ ⊢ a^{H} : A′}

does the four color theorem need type theory? Georges Gonthier, late 2004 full formalization of the proof of the four color theorem in Coq the core of the proof is a large functional program

       refl_equal true : (check_reducible cf ) = true

Georges : the use of type theory was essential

(this only could have been done in Coq)

Henk : … because it needs reduction inside the logic …
Georges : no, the use of reduction in the logic is not essential

(it only makes things run a bit faster)

me : ???

programs for set theory

while programs for ZF

Tucker & Zucker: ‘while programs’ over an arbitrary many-sorted algebra

proposal: add new kind of definition to set theory ‘while programs’ over the set theoretic universe V

– old-fashioned imperative programs

– all variables hold untyped ZF sets

possibility to actually execute program: not an issue but: some programs will be executable! example

func leastfixedpoint(f) begin

var X := emptyset, X′; while true do

X′ := apply(f,X);

if X′ == X then break fi; X := X′

od; return X

end;

transfinite loops possibility to loop ‘beyond’ omega

value of the variable x at iteration γ we call x_{γ}

x_{α} := ⋃_{β<α} ⋂_{β<γ<α} x_{γ}

or, alternatively

x_{α} := ⋂_{β<α} ⋃_{β<γ<α} x_{γ}

experimenting with HOL Light

evaluation by rewriting

# let PLUS = define                              (* ‘ Fixpoint ’ *)
  `(!m. plus 0 m = m) /\
   (!n m. plus (SUC n) m = SUC (plus n m))`;;
val PLUS : thm =
  |- (!m. plus 0 m = m) /\
     (!n m. plus (SUC n) m = SUC (plus n m))
# REWRITE_CONV[PLUS] `plus (SUC (SUC 0)) (SUC (SUC 0))`
                                          (* ‘ Eval compute in ’ *);;
val it : thm =
  |- plus (SUC (SUC 0)) (SUC (SUC 0)) =
     SUC (SUC (SUC (SUC 0)))
#

programs should not have to terminate!

let COLLATZ = new_definition
`COLLATZ = Y \COLLATZ n.
if n = 1 then 0 else
  let n' = if EVEN n then n DIV 2 else 3*n + 1 in
  COLLATZ n' + 1`;;
let COLLATZ =
`COLLATZ =
(DO \x. x,0) SEQ
(WHILE (\(x,n). ~(x = 1))
  ((DO \(x,n). x,(n + 1)) SEQ
   (IF (\(x,n). EVEN x)
      (DO \(x,n). (x DIV 2),n)
      (DO \(x,n). (3*x + 1),n)))) SEQ
(RETURN \(x,n). n)`;;

evaluation by C compiler importing external computations through an extra proof rule …

… that is conservative over the existing logic

reduction in the logic: ^{kernel}^{logic}^{conversion} evaluation by rewriting:

kernel logic

external evaluation: ^{kernel}^{logic}^{external}

rewriting

conclusion

should reduction be built into the logic? logics with a natural notion of computation

• beautiful

• complex (‘is ZF a hack?’)

can one afford not to have computation in the logic? slowdown by a constant factor (trading speed for simplicity)

my answer: yes!