Next:
Introduction
Logic, languages and computability
John Stalker
Introduction
A simplified example
Rules
Languages
Statements
A formal language
Logic
Parse trees
Graphs
Interpretation
Expressiveness
Parsing
Infix, prefix and postfix
A parser for the prefix language
A parser for the postfix language
Parser generators
A simple module selection checker
A simpler checker
Idealised machines
A hierarchy of languages
Satisfiability
Tautologies and consequences
Rules of inference
Formal systems
Sets
A regular language
Conclusion
Languages
A grammar example
Terminology
Example, continued
Natural languages
A formal language for linear equations
Thinking backwards
The language of balanced parentheses
The language of palindromes
More numerical examples
Ambiguous grammars
Constructing a parser from a grammar
Formal definition
Grammars
Hierarchy
Back to the beginning
Zeroeth order logic
Formal vs informal proof
Formal systems
A language for zeroeth order logic
Interpretation(s)
Truth tables
Informal proofs in zeroeth order logic
Analytic tableaux
Tableau rules
Satisfiability
Examples
Consequences
Axiomatic systems for zeroeth order logic
The Nicod formal system
The Łukasiewicz system
Natural deduction
A formal system for natural deduction
Introducing and discharging hypotheses
Some proofs
Substitution
From tableaux to proofs
Soundness, consistency and completeness
Non-deterministic algorithms
Puzzles
Linguistic examples
Zeroeth order logic as a non-deterministic computation.
Trees of trees
Making non-deterministic algorithms deterministic
First order logic
Varieties of first order logic
A language for first order logic
Free and bound variables
Interpretations
Informal proofs
Tableaux rules for equality and quantifiers
Example tableaux
Tableaux as nondeterministic computations
Natural deduction for first order logic
Soundness, consistency and completeness of first order logic
Elementary arithmetic
A language for arithmetic
Interpretation
Redundancy and ambiguity
Expressing more complex ideas
Arithmetic subsets and relations
Bounded arithmetic
Encoding
Encoding grammar
Encoding non-deterministic computations
Encoding formal systems
Encoding arithmetic in arithmetic
Tarski’s theorem
A formal system for arithmetic
Induction
Formal proofs
Gödel’s theorem
Rosser’s theorem
Set theory
A language for set theory
Simple set theory
Axioms (informal version)
Discussion
Axioms (formal version)
Non-sets
Set operations and Boolean operations
Finite sets
Definitions
Elementary properties of finite sets.
Induction for finite sets
Lists
Kuratowski pairs
Kuratowski triples?
Lists
Interfaces and implementation
Pairs again
Cartesian products
Relations
Basic definitions
Examples
Functions
Replacement
Order relations, equivalence relations
Notation
Natural numbers
Infinite sets
Cardinality
Diagonalisation
Countable sets
Properties of countable sets
Uncountable sets
Choice
Dependent choice
Zorn’s Lemma
Banach-Tarski
Additional axioms
Foundation
Extensionality, again
Zermelo-Fraenkel
Graph theory
Examples
Different notions of a graph
Definition
Ways to describe finite graphs
Bipartite graphs, complete graphs, colouring
Homomorphisms
Subgraphs, degrees
Walks, trails, paths, etc.
Connectedness
Eulerian trails and circuits
Hamiltonian paths and circuits
Spanning trees
Abstract algebra
Binary operations
Semigroups
Identity elements, monoids
Inverse elements and groups
Homomorphisms
Quotients
Integers and rationals
The power function
Notation
Regular languages
Regular grammars
Closure properties
Unions
Concatenation
Kleene star
Reversal
Finite state automata
Non-deterministic finite state automata
Deterministic finite state automata
Closure properties
Intersection
Relative complements
Regular expressions
The basic operations
Examples
From regular expressions to grammars
Regular expressions from automata
Reversal
Extended syntax
Regular languages
Pumping lemma
The statement of the lemma
Examples
Finite languages
The proof of the lemma
The Myhill-Nerode theorem
From languages to automata
An example
The converse
The syntactic monoid
Context free languages
Closure properties
Pushdown automata
Parsing by guessing
Deterministic pushdown automata
From pushdown automata to context free grammars
Pumping lemma
Application
Proof
Other idealised machines
More finite state automata
More pushdown automata
Turing machines
A Turing machine
The Church-Turing hypothesis
Universal Turing machines
The Halting Problem
Conclusion