Introduction: Propositional Logic, and Proof Theories

Propositional logic uses terms that are either true or false, or a composition of terms

Predicate Logic


Formalizing English

Logical Connectives -> Quantifiers -> Constants -> Functions -> Predicates


Natural Deduction

We extend the rules used in predicate logic, with ones able to handle quantifiers


Hidden Premises

north_of(Ottawa, Toronto) and north_of(Toronto, Waterloo), therefore north_of(Ottawa, Waterloo)

An enthymeme is an argument that contains a hidden premise

A theory is a set of statements we want to make about some phenomenon

Predicate Logic with Equality

Theory of Arithmetic

Recall Theories are a set of axioms about constants, functions and predicate symbols; built on logic.


Distinct elements, unordered collection. Has predicates element of.


Set Functions

Derrived Laws of Set Theory:

Proofs in Set Theory

There's a whole bunch of rules, see slides for TP and ND extensions. George uses by sets % then the rule

Russell's Paradox: if a set can contain sets as elements, can it contain itself?


Proofs in relations

Can create new binary relations from subsets of existing relations by restricting or subtracting domain or range.

Relational overriding R ⊕ S = ((dom S) <-| R) u S

Z Specification

Formal specification language

Program Correctness

Show that program has correct behaviour. A spec describes desired output for input.

Formal Verification describe in logic the spec for code, verified with proof theory. Important for critical software, helps to find bugs and "tests for ALL inputs".

Programming Language

We will verify imperative (seq of commands), sequential (no concurrency) and transformational programs (guarantees output and termination).

Spec consists of pre and postcondition

Triples are assertions assert(P); C; assert(Q);

Proof Rules

We add rules to state whether commands in our programming language satisfy some precondition and post condition, given a set of premises and a conclusion consisting of a triple


Function mapping indicies to values starting at 0 or 1

Functions and Procedures

Formal parameters are the indentifiers, while actual parameters are the values passed during the function call

Procedures can change parameters and global variables

Logical Variable Introduction

For any any assertion with a variable, we can introduce a sort of temporary variable (that is currently not used) to represent a value at a given state.

Rule: Log Var Intro, P(w), then P(w0) & w = W0

Recursive Functions

We use induction in the correctness proofs of recursive functions

  1. base case, function satisfies its spec where there are no recursive calls
  2. induction step, assuming it satisfies its spec for all calls to the function, then it satisfies its spec

Look through the examples!!! around slide 200


A non terminating while loop or a non-terminating function or procedure recursion

To show termination, we identify an integer expression involving the variables of the loop condition that

  1. is guaranteed to be non-negative
  2. decreases with every iteration
  3. makes the loop's guard become false as it approaches 0

This expression is called the variant or bounding function.

For recursion, show there is a section of the function that does not make recursive calls and is entered as the bounding function approaches 0

The Decision problem is a subset of problems which have yes/no answers

Unsolvable (undecidable) problems: decison problems for which no algorithm exists to solve