VALUATION SYSTEMS AND CONSEQUENCES

• Logics and Computer Science
• Summary

Valuation Systems

• Satisfaction
• Valuation systems
• Modal logic and possible worlds
• Predicate language
• Summary

Consequence relations and entailment relations

• Consequence relations
• Entailment relations
• The systems C and S4
• Levels of implication
• Consequence operator
• Summary

Proof theory and presentations

• Hilbert presentations
• Natural deduction presentations
• Natural deduction in sequent style
• Intuitionistic logic
• Gentzen sequent calculus for I
• Gentzen sequent calculus for C and S4
• Properties of presentations

Some further topics

• Valuation systems for I
• Maps between logics
• Correspondence theory
• Consistency

RECURSION THEORY

• Opening remarks
• A taster
• Contents of the chapter

Languages and notions of computibility

• Computibility and non-computibility
• Inductive definitions
• Recursion theory

UNIVERSAL ALGEBRA

• What is universal algebra?
• Universal algebra in mathematics and computer science
• Overview of the chapter
• Historical notes
• Acknowledgments
• Prerequisites

Examples of algebras

• Some basic algebras
• Some simple constructions
• Syntax and semantics of programs
• Synchronous concurrent algorithms
• Algebras and modularisation of software

Algebras and morphisms

• Signatures and algebras
• Subalgebras
• Congruence and quotient algebras
• Homomorphisms and isomorphisms
• Direct products
• Abstract data types

Constructions

• Subdirect products, residual and local properties
• Direct and inverse limits
• Reduced products and ultraproducts
• Local and residual properties and approximations
• Remarks on references

Classes of algebras

• Free, initial and final algebras
• Equational logic
• Equational Horn logic
• Specification of abstract data types
• Remarks on references

Further reading

• Universal algebra
• Model theory

BASIC CATEGORY THEORY

• Types, composition and identities
• Categories
• Relating functional calculus and category theory
• Compositionality is functorial
• Natural transformations

On universal definitions: products, disjoint sums and higher types

• Product types
• Coproducts
• Higher types
• Reasoning by universal arguments
• Another 'universal definition': primitive recursion
• The categorical abstract machine

Universal problems and universal solutions

• On observation and abstraction
• A more categorical point of view
• Universal morphisms
• Adjunction
• On generation
• More examples for separation and generation

Elements and beyond

• Variable elements, variable subsets and representable functors
• Yoneda's heritage
• Towards an enriched category theory

Data Structures

• Subtypes
• Limits
• Colimits

Universal constructions

• The adjoint functor theorem
• Generation as partial evaluation
• Left Kan extensions, tensors and coends
• Separation by testing
• On bimodules and density

Axiomatizing programming languages

• Relating theories of (-calculus
• Type equations and recursion
• Solving recursive equations

Algebra categorically

• Functorial semantics
• Enriched functorial semantics
• Monads

On the categorical interpretation of calculi

• Category theory as proof theory
• Substitution as predicate transformation
• Theories of equality
• Type theories

A sort of conclusion

Literature

• Textbooks
• References

TOPOLOGY

Example of topological spaces

• Sierpinski space
• Scott Topology
• Spaces of maximal elements. Cantor space
• Alexandroff topology
• Stone spaces
• Spectral spaces
• The reals

Alternative formulations of topology

• Closed sets
• Neighborhoods
• Examples
• Closure operators
• Convergence

Separation, continuity and sobriety

• Separation conditions
• Continuous functions
• Predicate transformers and sobriety
• Many-valued functions

Constructions: new spaces from old

• Postscript: effectiveness and representation

Metric Spaces

• Basic definitions
• Examples
• Completeness
• Topology and metric
• Constructions
• A note on uniformities

Compactness

• Compactness and finiteness
• Spectral spaces
• Positive and negative information: patch topology
• Hyperspaces
• Tychonoff's theorem
• Locally compact spaces
• Function spaces

MODEL THEORY AND COMPUTER SCIENCE

The set theoretic modelling of syntax and semantics

• First Order structures
• The choice of the vocabulary
• Logics

Model theory and computer science

• Computer science
• The birth of model theory
• Definability questions
• Preservation theorems
• Disappointing ultraproducts
• Complete theories and elimination of quantifiers
• Spectrum problems
• Beyond first order logic
• The hidden method

Preservation theorems

• Horn formulas

Fast growing functions

• Non-provability results in second order arithmetic
• Non-provability in complexity theory
• Model theory of fast growing functions

Elimination of quantifiers

• Computer aided theorem proving in classical mathematics
• Tarski's theorem
• Elementary geometry
• Other theories with elimination of quantifiers

Computable logics over finite structures

• Computable logics
• Computable quantifiers
• Computable predicate transformers
• L-Reducibility
• Logics capturing complexity classes

Ehrenfeucht-Fraisse games

• The games
• Completeness of the game
• Second order logic and its sublogics
• More non-definability results
• The games and pumping lemmas

Conclusions