MATHEMATICAL REASONING

By THOMAS RODRIGUEZ

CONTENTS INTRODUCTION SUMMARY OF THE CONTENTS ANSWERS TO READERS’ QUESTIONS WHY LOGIC? WHY A PRACTICAL LOGIC? WHY SIMPLE TYPE THEORY? WHY NOT FIRST-ORDER LOGIC? WHY NOT SET THEORY? WHY NOT DEPENDENT TYPE THEORY? WHY UNDE?NEDNESS? WHY MODEL THEORY INSTEAD OF PROOF THEORY? PRELIMINARY CONCEPTS WHAT IS MATHEMATICS? MATHEMATICAL VALUES SETS SEQUENCES RELATIONS FUNCTIONS BOOLEAN VALUES AND PREDICATES BINDERS UNDE?NEDNESS MATHEMATICAL STRUCTURES EXAMPLES OF MATHEMATICAL STRUCTURES CONCLUSIONS EXERCISES CONTENTS SYNTAX NOTATION SYMBOLS TYPES EXPRESSIONS BOUND AND FREE VARIABLES SUBSTITUTION LANGUAGES SEMANTICS INTERPRETATIONS GENERAL MODELS FINITE GENERAL MODELS STANDARD MODELS SATIS?ABILITY, VALIDITY, AND SEMANTIC CONSEQUENCE ISOMORPHIC GENERAL MODELS EXPANSION OF A GENERAL MODEL STANDARD VS GENERAL SEMANTICS EXAMPLES OF STANDARD MODELS 5 10 CONCLUSIONS 5 11 EXERCISES ADDITIONAL NOTATION BOOLEAN OPERATORS BINARY OPERATORS QUANTI?ERS DE?NEDNESS TUPLES MISCELLANEOUS NOTATION QUASITYPES AND DEPENDENT QUASITYPES 6 10 CONCLUSIONS 6 11 EXERCISES BETA-REDUCTION AND SUBSTITUTION BETA-REDUCTION UNIVERSAL INSTANTIATION INVALID BETA-REDUCTION ALPHA-CONVERSION PROOF SYSTEMS BACKGROUND A PROOF SYSTEM FOR ALONZO AXIOMS RULES OF INFERENCE PROOFS SOUNDNESS FRUGAL GENERAL MODELS COMPLETENESS THEORIES AXIOMATIC THEORIES THEORY EXTENSIONS CONSERVATIVE THEORY EXTENSIONS CATEGORICAL THEORIES COMPLETE THEORIES FUNDAMENTAL FORM OF A MATHEMATICAL PROBLEM MODEL THEORY 10 SEQUENCES 10 1 SYSTEMS OF NATURAL NUMBERS 10 2 NOTATION FOR SEQUENCES 10 3 CONCLUSIONS 10 4 EXERCISES 11 DEVELOPMENTS 11 1 THEORY DEVELOPMENTS 11 2 DEVELOPMENT OF NATURAL NUMBER ARITHMETIC 11 2 1 BASIC DE?NITIONS AND THEOREMS 11 2 2 COMMUTATIVE SEMIRING 11 2 3 WEAK TOTAL ORDER 11 2 4 DIVIDES LATTICE 11 3 CONCLUSIONS 11 4 EXERCISES 12 REAL NUMBER MATHEMATICS 12 1 COMPLETE ORDERED FIELDS 12 2 ALTERNATIVES TO THE CONSTRUCTION OF COF 12 3 DEVELOPMENT OF REAL NUMBER MATHEMATICS 12 3 1 SOME BASIC DE?NITIONS AND THEOREMS 12 3 2 NATURALS, INTEGERS, AND RATIONALS 12 3 3 ITERATED SUM AND PRODUCT OPERATORS 12 3 4 CALCULUS 12 3 5 EUCLIDEAN SPACE 12 4 SKOLEM’S PARADOX 12 5 CONCLUSIONS 12 6 EXERCISES 13 MORPHISMS 13 1 A MOTIVATING EXAMPLE 13 2 THE LITTLE THEORIES METHOD 13 3 THEORY MORPHISMS 13 3 1 THEORY TRANSLATIONS 13 3 2 MORPHISM THEOREM 13 3 3 EXAMPLES OF THEORY MORPHISMS 13 3 4 FAITHFUL THEORY MORPHISMS 13 4 DEVELOPMENT MORPHISMS 13 4 1 DEVELOPMENT TRANSLATIONS 13 4 2 TRANSPORTATIONS 13 5 MATHEMATICS LIBRARIES 13 5 1 THEORY GRAPHS 13 5 2 DEVELOPMENT GRAPHS 13 5 3 REALM GRAPHS 13 6 THEORY GRAPH COMBINATORS 13 7 CONCLUSIONS 13 8 EXERCISES 14 ALONZO VARIANTS 14 1 ALONZO WITH INDE?NITE DESCRIPTION 14 1 1 INTRODUCTION 14 1 2 SYNTAX CONTENTS CONTENTS 14 1 3 SEMANTICS 14 1 4 PROOF SYSTEM 14 1 5 THEOREMS 14 2 ALONZO WITH SORTS 14 2 1 INTRODUCTION 14 2 2 SYNTAX 14 2 3 SEMANTICS 14 2 4 PROOF SYSTEM 14 2 5 THEOREMS 14 3 ALONZO WITH QUOTATION AND EVALUATION 14 3 1 INTRODUCTION 14 3 2 SYNTAX 14 3 3 SEMANTICS 14 3 4 PROOF SYSTEM 14 3 5 THEOREMS 14 4 CONCLUSIONS 15 SOFTWARE SUPPORT 15 1 BASIS SUPPORT 15 2 ADVANCED SUPPORT 15 2 1 ORGANIZATION 15 2 2 INFERENCE 15 2 3 COMPUTATION 15 2 4 CONCRETIZATION 15 2 5 NARRATION 15 3 FULLY INTEGRATED SUPPORT 15 4 CONCLUSIONS