I. higher-order logic (chapter 3) ------------------------------------------ ASCII NOTATION We write: ``(\ x . t)'' for (\lambda x . t) ``|-'' for turnstile (latex's \vdash) ``\in'' for set membership ------------------------------------------ A. types and terms (3.1) ------------------------------------------ SYNTAX OF HOL def: A Nat-indexed set of type operators, AT = , where each Op_n is a set of symbols, is a *type structure*. The arity of Op_n is n. The constants of AT are C = Op_0. S ::= "types over AT" C "atomic types" | S1 -> S2 "function types" | Op(S1, ..., Sn) "app of type oper" t ::= "terms" | v "variable refs" | c "constants" | t1 . t2 "applications" | (\ v : S . t1) "abstractions" | t:S "typings" ------------------------------------------ Is it really reasonable to assume that constants are distinguished from variables? ------------------------------------------ TYPING RULES def: Let AT be given. Then a relation between constant symbols and types SG = {c:S | S a type}, is a *signature*. def: A *type environment*, TE, is a from from variables to types. Typing Rules, for a given signature SG TE |- v : S (tvar) * if (v:S) \in TE TE |- c : S (tcon) * if (c:S) \in SG and c \not\in dom(TE) TE |- t1: S1 -> S2, TE |- t2: S1 _________________________________ (tapp) TE |- t1 . t2 : S2 TE,(v:S) |- t2: S2 _______________________________ (tlam) TE |- (\ v: S1 . t2) : S1 -> S2 TE |- t: S __________________ (texplicit) TE |- (t : S) : S ------------------------------------------ Do we care about terms that don't have types? Do terms have unique types in this setup? 1. precedence and association 2. substitution and replacement What's the notation for substitution? 3. standard types and constants What types are built-in? What constants are built-in? 4. examples Can you give a typing derivation (\ x: Int . x == 641)? II. semantics (3.2) A. Semantics of types Can the meaning of a type S, M.S, be empty? Why? What is the universe, U, closed under? What distinguised sets are assumed in the universe, U? What's a model of a type structure? B. Semantics of terms What is a model of a signature, SG, over a type structure AT? What is a model of a type environment? ------------------------------------------ MEANING OF TERMS def: Let TE be a type environment. A TE-environment, E, is a function E : dom(TE) -> U such that for all (v:S) \in TE, E.v \in M.S def: Let be a signature. Let TE |- t: S. Let E be a TE-environment. Then M_E.t:S is defined by M_E.c:S == M.c if c:S \in SG, and c \not\in dom(TE) M_E.v:S == E.v if v:S \in TE M_E.(t1.t2):S == (M_E.t1).(M_E.t2) M_E.(\v:S.t):S == (\a.M_{E,(v:a)}.t) M_E.(t:S):S == M_E.t : S ------------------------------------------ III. Deductive Systems (3.3) A. defintions What's a formula over SG? So is a formula either true or false? What's a sequent, and what does it have to do with deduction? When is a sequent satisfied in a model? When is a sequent valid? What's an inference? When is an inference valid? What's the difference between an inference and a deductive system? What's a side condition? What role does it play in a deductive system? What's the difference between an axiom and an axiom scheme? 1. deductions What's the difference between a deduction and a proof? What's the difference between a metavariable and a variable? B. theorems (3.4) What's a theory? How is a theory specified? How can a theory be inconsistent? Is an inconsistent theory sound? complete? If we extend a theory's presentation, can we still prove everything we could prove before? What's a conservative extension? Why is it important?