Formalisation of Mathematics

Weyl’s predicative math in type theory : 

Weyl’s predicative math in type theory Zhaohui Luo Dept of Computer Science Royal Holloway, Univ of London (Joint work with Robin Adams)

Slide 2: 

April 2006 2 Formalisation of mathematics with different logical foundations in a type-theoretic framework

This talk : 

April 2006 3 This talk Maths based on different logical foundations Weyl’s predicative mathematics Type-theoretic framework Example: logic-enriched TT with classical logic Predicativity Impredicative and predicative notions of set Formalisations Real number system, predicatively and impredicatively

I. Applications of TT to formalisation of maths : 

April 2006 4 I. Applications of TT to formalisation of maths Formalisation in TT-based proof assistants Examples in Coq: Fundamental Theorem of Algebra Four-colour Theorem Maths with different logical foundations Variety of maths, all legacies (mathematical “pluralism”) Adequacy in formalisation? Uniform framework? Type theory and associated technology Not just for constructive math Also for classical math and other maths

Maths with different logical foundations: examples : 

April 2006 5 Maths with different logical foundations: examples Consider the “combinations” of the following and their “negations”: (C) Classical logic (I) Impredicative definitions We would have (CI) Ordinary (classical, impredicative) math Classical set theory/simple type theory, HOL/Isabelle (C°I°) Predicative constructive math Martin-Löf’s TT, ALF/Agda/NuPRL (C°I) Impredicative constructive math Constructions/CID/ECC/UTT, Coq/Lego/Plastic (CI°) Predicative classical math Weyl, Feferman, Simpson, … Uniform foundational framework for formalisation?

Weyl’s predicative mathematics : 

April 2006 6 Weyl’s predicative mathematics H. Weyl. The Continuum. (Das Kontinuum.) 1918. Historical development (paradox etc.) The notion of category Predicative development of the real number system Weyl/Feferman/Simpson’s work on predicativity Predicativity E.g., { x | φ(x) } with φ being “arithmetical” (without quantification over sets) Feferman’s development on “predicativism” Simpson’s work on reverse mathematics

II. Logic-enriched type theories in LFs : 

April 2006 7 II. Logic-enriched type theories in LFs Logic-enriched type theory Aczel & Gambino (LTT in the intuitionistic setting) [AG02,06] c.f. separation of logical propositions and data types in ECC/UTT [Luo90,94] Type-theoretic framework for mathematical “pluralism” Logic-enriched TTs in a logical framework: Logic Types \ / \ / Logical Framework

An example: T : 

April 2006 8 An example: T T = LF + Classical FOL + Ind types/universes Classical Ind types FOL + universes \ / \ / LF

Classical FOL (specified in a logical framework) : 

April 2006 9 Classical FOL (specified in a logical framework) Propositions (note: LF should be “extended” with Prop and Prf) Prop kind Prf(P) kind [P : Prop] Logical operators PQ : Prop [P : Prop, Q : Prop] [A,P] : Prop [A : Type, P[x:A] : Prop] ¬P : Prop [P : Prop] DN[P,p] : Prf(P) [P:Prop, p:Prf(¬¬P)]

Types : 

April 2006 10 Types Inductive types/families e.g. Nats, Trees, … (as in TTs such as UTT) Induction Rule: elimination over propositions. Example: the natural numbers N : Type, 0 : N, succ[n] : N [n : N] Elimination over types: ElimT[C,c,f,n] : C[n], for C[n] : Type [n : N] Plus computational rules for ElimT: eg, ElimT[C,c,f,succ(n)] = f[n,ElimT[C,c,f,n]] Induction over propositions: ElimP[P,c,f,n] : P[n], for P[n] : Prop [n : N]

Relative consistency : 

April 2006 11 Relative consistency Theorem (relative consistency of T) T is logically consistent w.r.t. ZF.

III. Formalisation : 

April 2006 12 III. Formalisation Consider Classical logic T \ / \ / LF with T = Inductive types + Impredicative sets (I) Predicative sets (I°)

Impredicative notion of set : 

April 2006 13 Impredicative notion of set Typed sets, impredicatively: Set[A:Type] : Type set[A:Type,P[x:A]:Prop] : Set[A] in[A:Type,a:A,S:Set[A]] : Prop in[A,a,set[A,P]] = P[a] : Prop Every set has a “base type” (or “category”) Sets are given by characteristic propositional functions { x : A | P(x) } – set(A,P) s  S – in(A,s,S) One can formulate powersets as …

Predicative notion of set : 

April 2006 14 Predicative notion of set Type universe and propositional universe type : Type and T[a:type] : Type (universe of “small types”) prop : Prop and V[p:prop] : Prop (universe of “small propositions”) [a:type,p[x:T[a]]:prop] : prop and V[[a,p]] = [T[a],V◦p] : Prop Predicative notion of set Set[A:Type] : Type set[A:Type,p[x:A]:prop] : Set[A] in[A:Type,x:A,S:Set[A]] : prop in[A,x,set[A,p]] = p[x] : prop

Formalisation in Plastic : 

April 2006 15 Formalisation in Plastic Plastic (Callaghan [CL01]) Plastic: proof assistant, implementing a logical framework Extending Plastic with “Prop” etc. Formalisation Weyl’s predicative development Nats, Integers, Rationals, and Dedekind cuts. Completion and LUB theorems for real numbers. Other features Types as informal “categories” Typed sets Setoids Comparison between predicative and impredicative developments