CS 245

CS 245 - Logic & Computation
TTH 10:00AM - 11:20AM
MC 4045
Stephen Watt

10% quiz | 20% assignments | 30% midterm | 40% final

Office Hours:
Lila Kari: TTh 2:30-3:30 pm
Stephen Watt: M 11-12am F 1-2pm

Anthony Zhang Reference Sheet

1 | Propositional Logic

1.1 | Introduction

What is Logic?

“this course is like a broken toaster”

Logic = the Science of Reasoning Syllogism = a kind of logical argument in which a proposition (conclusion) is inferred from 2 or more others (premises)

Logic and CS

Computers are built from electronic digital circuits, which are formed out of logic gates

• Logic is used to reduce the number of necessary logic gates

Applications

• Automated theorem proving (proof verifiers)
• Fully / semi automated techniques to analyze the behavior of reactive programs
• Databases (SQL) use first-order logic
• Programming
  • Program specification
  • Formal verification

Propositional logic

Studies logical relationships between propositions (true/false statements)

Some important logical arguments: Hypothetical Syllogism

1. If p then q
2. If q then r
3. If p then r

Disjunctive Syllogism

1. p or q
2. Not q
3. p

Modus Ponens (crossing the pond)

1. If p then q
2. p
3. q

Modus Tollens

1. If p then q
2. Not q
3. Not p

Atomic Propositions = Proposition symbols which can’t be further subdivided Compound Propositions = Obtained by combining several atomic propositions

Logical Connectives = or / and / not / if-then

• Convention: Stating a proposition in English implies it’s true
• Negation (not) - is the only unary connective
• Conjunction (and)
• Disjunction (inclusive or) - p $\vee$ q should be translated as “p or q, or both”
• Implication (if-then) - is the only non-symmetric connective. reversing it is the converse
• Equivalence (if and only if)

Dealing with imprecision and ambiguity

• ”Don’t leave animals in cars because they rapidly turn into ovens”

Translations from English to Logic

1.2 | Propositional Logic Syntax

Syntax of propositional language $L^p$: atoms, formulas

Expressions

• Expressions = finite strings of allowed symbols
• Length = number of occurrences of symbols in an expression
• Empty expression = expression of length 0, denoted by $ϵ$
• Equal = two expressions that are the same
• Concatenating two expressions $U,V$ is denoted as $UV$
  • $ϵU=Uϵ=U$
• If $U=W_{1}V{W}_2$, then
  • $V$ is a segment of $U$
  • If $V\ne U$, then $V$ is a proper segment of $U$
• If $U=VW$, then $V$ is an initial segment (prefix) and $W$ is a terminal segment (suffix) of $U$

The set of formulas of $L^p$

• $Atom(L^p)$ is the set of expressions of $L^p$ that consist of a proposition symbol only
• $Form(L^p)$ is the set of formulas in $L^p$, defined recursively as any previous formulas joined by $\neg ,\wedge ,\vee ,⟹,⟺$

Generating and parsing formulas of $L^p$

Parse Tree = used to analyze formulas

Theorem: Unique Readability Theorem Every formula in $Form(L^p)$ is of exactly one of the six forms: an atom, $(\neg A),(A\wedge B),(A\vee B),(A⟹B),(A⟺B)$

Mathematical induction (review), structural induction

Principle of Mathematical Induction:

• Establish that property $P$ is true for 0
• Establish that $P(n)⟹P(n+1)$

Structural Induction for Recursively Defined Sets

1. Base case(s)
2. (Composite) Inductive step: Show that the property holds after applying each recursive rule

Lemma 1: Every formula in $Form(L^p)$ has an equal number of left and right parentheses

Proof: We use structural induction Base Case: $A$ is an atom, and has 0 left and right parentheses

For the subcase of $\neg$ Inductive Step: Assume $A$ is $(\neg B)$ Inductive Hypothesis: formula $B$ has property $R:l(B)=r(B)$

$$\begin{array}{rl}l((\neg B))& =1+l(B)\\ & =1+r(B)\\ & =r((\neg B))\end{array}$$

For the other subcases IH: Formulas $B,C$ both have property $R$ To prove $R$ for $(B\wedge C),(B\vee C),(B⟹C),(B⟺C)$ has property $R$. WLOG, consider $(B\wedge C)$:

$$\begin{array}{rl}l((B\wedge C))& =1+l(B)+l(C)\\ & =1+r(B)+r(C)\\ & =r((B\wedge C))\end{array}$$

Unique Readability Theorem

Proof: Use the following Claims

1. The first symbol of a formula $A$ is either ${}^{\prime }{(}^{\prime }$ or a proposition symbol
2. Every formula $A$ has an equal number of ${}^{\prime }{(}^{\prime }$ and ${}^{\prime }{)}^{\prime }$ (Lemma 1)
3. If $A^{\prime }$ is a non-empty proper initial segment of a formula $A$, then $A^{\prime }$ has more ${}^{\prime }{(}^{\prime }$ than ${}^{\prime }{)}^{\prime }$

Assume that a formula $F$ can be of the following forms

1. $F=p=A$
2. $F=(\neg A)=(B\ast C)$, where $\ast \in \{\wedge ,\vee ,⟹,⟺\}$
3. $F=(B\ast C)=(B^{\prime }{\ast }^{\prime }{C}^{\prime })$, where $\ast ,{\ast }^{\prime }\in \{\wedge ,\vee ,⟹,⟺\}$

Recall that $(B\ast C)=(B^{\prime }{\ast }^{\prime }{C}^{\prime })$ means they are equal

1. Assume $p=A$ which leads to a contradiction
2. Assume $(\neg A)=(B\ast C)$ which leads to a contradiction
3. Assume $(B\ast C)=(B^{\prime }{\ast }^{\prime }{C}^{\prime })$. Deleting the first symbol yields $B\ast C)=B^{\prime }{\ast }^{\prime }{C}^{\prime })$. Thus, B is:
   1. strictly shorter than $B^{\prime }$ - a contradiction
   2. strictly longer than $B^{\prime }$ - a contradiction
   3. the same length as $B^{\prime }$ - which proves the statement

Algorithm for parsing formulas: Count the excess of ${}^{\prime }{(}^{\prime }$ over ${}^{\prime }{)}^{\prime }$ to determine the number of sub-formulas

Precedence rules and scope for connectives

Precedence order:

1. $\neg$ not
2. $\wedge$ and
3. $\vee$ or
4. $⟹$ if
5. $⟺$ iff

1.3 | Propositional Logic Semantics

Syntax vs semantics, truth valuations, truth tables

Syntax = the rules used for constructing formulas in $Form(L^p)$ Semantics = are concerned with meaning (atoms and connectives)

Truth valuation:

$$t:Atom(L^p)\to \{0,1\}$$

Satisfiability, tautologies, contradictions

Satisfied = Something is valued at 1 under the truth valuation Tautology = Something that’s always true Contradiction = Something that’s always false

Plato’s 3 essential laws of thought:

1. Law of identity: $p=p$
2. Law of contradiction: $\neg (p\wedge \neg p)$
3. Law of excluded middle: $(p\vee \neg p)$

Proving argument validity semantically

Tautological consequence $(\models )$ \models

• Special case: $\varnothing \models A$ Tautological equivalence (|=|)

Proving tautological consequence by truth tables

Bash it (takes a long time and grows exponentially) Disproving by counterexamples

Edge cases: An unsatisfiable set (contradiction) tautologically implies any formula! The empty set is satisfied under any truth valuation!

General method for proving argument validity (semantically)

Test A will give a positive result if and only if either virus X or virus Y is present. Test B will give a positive result if and only if virus Y or Z is present. If test C is positive, virus Y can be excluded. The patient reacts positively to all three tests. Prove that the patient has virus X and virus Z but not virus Y

Solution:

1. $A⟺X\vee Y$
2. $B⟺Y\vee Z$
3. $C⟹\neg Y$
4. $A\wedge B\wedge C$

$$(X\vee Y)\wedge (Y\vee Z)\wedge (\neg Y)⟹X\wedge Z$$

1.4 | Propositional Calculus: Essential Laws, Normal Forms

Propositional calculus

Simplification: Removing implication:

$$A⟹B\models \neg A\vee B$$

Removing if and only if: (both true or both false)

$$A⟺B\models (A\wedge B)\vee (\neg A\wedge \neg B)$$

(first implies second or second implies first)

$$A⟺B\models (A⟹B)\wedge (B⟹A)\models (\neg A\vee B)\wedge (\neg B\vee A)$$

Essential laws for propositional calculus

• All laws come in dual pairs, which are obtained by swapping 0 and 1, as well as $\wedge ,\vee$
• (somewhat shaky) Analogy: $\vee$ is treated like addition, while $\wedge$ is treaded like multiplication

Absorption Laws I

$$A\vee (A\wedge B)\models A$$ $$A\wedge (A\vee B)\models A$$

Absorption Laws II

$$(A\wedge B)\vee (\neg A\wedge B)\models B$$ $$(A\vee B)\wedge (\neg A\vee B)\models B$$

A literal is a formula of the form $p,\neg p$ (complimentary literals)

Simplifying conjunctions (and)

• If an and contains 0, it always yields 0
• If an and contains 1 or any duplicate literals, they can be dropped

Simplifying disjunctions (or)

• If an or contains 1, it always yields 1
• If an or contains 0 or any duplicate literals, they can be dropped

Disjunctive / Conjunctive Normal Forms (DNF / CNF)

Def: Disjunctive Normal Form: A formula in DNF is of the form

$$(A_{11}\wedge \cdots \wedge A_{1n1})\vee \cdots \vee (A_{k1}\wedge \cdots \wedge A_{knk})$$

where $k\ge 1,n_1,\cdots ,n_k\ge 1$, and $A_{ij}$ are literals for $1\le i\le k$ and $1\le j\le n_i$. The formulas $A_{i1}\wedge \cdots A_{ini}$ are the conjunctive clauses of the formula in DNF.

Def: Conjunctive Normal Form: A formula in CNF is of the form

$$(A_{11}\vee \cdots \vee A_{1n1})\wedge \cdots \wedge (A_{k}1\vee \cdots \vee A_{knk})$$

Obtaining DNF and CNF from truth tables

Eliminate everything

1.5 | Connectives, Logic Gates, Circuit Design

n-ary connectives

Since $A⟹B\models \neg A\vee B$, the connective $⟹$ is said to be definable in terms of $\neg A\vee B$

There are 16 binary connectives (there are $2^{2^2}$ $n$-ary connectives)

Any set of connectives with the capability to express any truth table is said to be adequate

Proving adequacy and inadequacy of a set of connectives

Def: Adequacy A set S of connectives is called adequate iff any n-ary connective can be defined in terms of the connectives in S. For instance, the set $S_0=\{\neg ,\wedge ,\vee \}$ is adequate

• Proving adequacy: Show that all connectives in an adequate set $S_0=\{\neg ,\wedge ,\vee \}$ can be defined in terms of the connectives in $S$
• Proving inadequacy: Show that one of the connectives in the adequate set cannot be defined using the connectives in $S$

Pierce Arrow for NOR ($\downarrow$) is adequate

$$\begin{array}{rl}\neg p& \models p\downarrow p\\ p\wedge q& \models (p\downarrow p)\downarrow (q\downarrow q)\\ p\vee q& \models (p\downarrow q)\downarrow (p\downarrow q)\end{array}$$

Sheffer stroke for NAND $(\mid )$ is also adequate

$$\begin{array}{rl}\neg p& \models p\mid p\\ p\vee q& \models (p\mid q)\mid (p\mid q)\\ p\wedge q& \models (p\mid p)\mid (q\mid q)\end{array}$$

Ternary Connectives

• Define $\tau (p,q,r)$ too mean if p, then q, else r
• There are $2^{(2^3)}$ distinct ternary connectives

Boolean algebra and propositional logic

Using set theory to describe propositional logic

$$\cap =\wedge ,\cup =\vee$$

Definition: Joolean algebra An $n$-variable Boolean function is a function of the form

$$f:\{0,1{\}}^n\to \{0,1\}$$

Logic Gates

Binary computers = transistors != electric computers

Circuit Design

Half-adder ($s$ = sum, $c$ = carry)

$x$	$y$	$s$	$c$
0	0	0	0
0	1	1	0
1	0	1	0
1	1	0	1

Full-adder (with the additional carry bit $c_i$)

$x$	$y$	$c_i$	$s$	$c_{i+1}$
0	0	0	0	0
0	0	1	1	0
0	1	0	1	0
0	1	1	0	1
1	0	0	1	0
1	0	1	0	1
1	1	0	0	1
1	1	1	1	1

Formula simplification and circuit minimization

Circuits can be simplified in the same way that code and logical formulas can

1.6 | Formal deduction in propositional logic

Formal deducibility in propositional logic

Formal Deducibility $⊢$ has a similar meaning to $\models$, signifying argument validity To write that $A$ is formally deducible (or provable) from $\Sigma$, we write

$$\Sigma ⊢A$$

11 rules of formal deduction (but I’m only writing the 3 coolest ones)

$$(\neg ,-)$$

If $\Sigma ,\neg A⊢B$, and $\Sigma ,\neg A⊢\neg B$, then $\Sigma ⊢A$ (proof by contradiction)

$$(\vee ,-)$$

If $\Sigma ,A⊢C$, and $\Sigma ,B⊢C$, then $\Sigma ,A\vee B⊢C$ (proof by cases)

$$(⟹,+)$$

If $\Sigma ,A⊢B$, then $\Sigma \models A⟹B$ (assumption of a premise is the antecedent of a conditional)

Definition of “formal deducibility” $(⊢)$

Definition: Formal deducibility A formula $A$ is formally deducible from $\Sigma$ ($\Sigma ⊢A$) if A is generated by a finite number of applications of the 11 rules of formal deduction

• Subsequent steps are generated by a rule of formal deduction
• The sequence of steps is called a formal proof of the last term ${\Sigma }_n⊢A_n$

Checking a proof: Check each step Finding a proof: Work in reverse

Semantics vs Syntax:

• Tautological consequence $(\Sigma \models A)$ is semantics
• Deducibility $(\Sigma ⊢A)$ is syntax

Proving statements about formal induction: Use structural induction on the set of theorems

Theorems: Finiteness of premise set, reduction ad absurdum, transitivity

Theorem: Finiteness of premise set If $\Sigma ⊢A$, then there exists a finite

$${\Sigma }^0\subseteq \Sigma \mid {\Sigma }^0⊢A$$

Theorem: Transitivity of deducibility Let $\Sigma \subseteq Form(L^p),A_1,\cdots A_n\in Form(L^p),n\le 1$.

$$\Sigma ⊢A_i\text{ for all }i\in [1,n]\text{ and }{A}_1,\dots A_n⊢A⟹\Sigma ⊢A$$

Theorem: Reductio ad absurdum

$$\Sigma ,A⊢B\text{ and }\Sigma ,A⊢\neg B⟹\Sigma ⊢\neg A$$

Theorem of replaceability of Syntactically Equivalent Formulas $(⊢)$

Definition: Two formulas $A,B$ are syntactically equivalent if

$$A⊢B\text{ and }B⊢A$$

Theorem: Replaceability of syntactically equivalent formulas Let $B,C$ be syntactically equivalent. For any $A$, let $A^{\prime }$ be constructed from $A$ by replacing some (not necessarily all) occurrences of $B$ by $C$. Then $A,\neg A$ are syntactically equivalent.

Theorems of Soundness and Completeness of Formal Deduction

Theorem: Soundness Theorem (should not be able to prove incorrect statements)

$$\Sigma ⊢A⟹\Sigma \models A$$

Theorem: Completeness Theorem (should be able to prove every correct statement)

$$\Sigma \models A⟹\Sigma ⊢A$$

Connection between syntax and semantics The Soundness and Completeness Theorems say that with formal deduction (as defined by the 11 rules) we can prove The truth, the whole truth, (completeness), and nothing but the truth. (soundness)

Logical Fallacies: Formal deduction can’t prove invalidity Recall that Descartes famously said “I think, therefore I am”. The joke was that Descartes goes into a bar and the bartender asks him if he wants another drink. “I think not,” says Descartes, and vanishes in a puff of smoke.

1. $T⟹A$
2. $\neg T$ Conclusion: $\neg A$ (fallacy of affirming the consequent)

“Why are you standing on this street corner, waiving your hands?”
“I am keeping away the elephants.”
“But there aren’t any elephants here.”
“You bet: that’s because I’m here.”

1. $p⟹\neg q$
2. $\neg q$ Conclusion: $p$ (fallacy of affirming the consequent)

Formal deduction proof strategies

1. If the consequence is an implication is an implication ($\Sigma ⊢A⟹B$), use $(⟹,+)$
2. If one of the premises is a disjunction ($\Sigma ,A\vee B⊢C$), use proof by cases $(\vee ,-)$
3. If we have to prove $C⊢D$ and the direct proof doesn’t work, proof the contrapositive $(\neg D⊢\neg C)$
4. If all else fails, use proof by contradiction $(\neg ,-)$ or $(\neg ,+)$ in the case of $\Sigma ⊢\neg B$

Consistency and Satisfiability

Definition: Consistency A set of formulas $\Sigma$ is consistent (w.r.t. a system of formal deduction, herein $⊢$) if there is no formula $F$ such that $\Sigma ⊢F$ and $\Sigma ⊢\neg F$. Otherwise, $\Sigma$ is inconsistent.

Lemma: Satisfiability A set $\Sigma$ of logic formulas is satisfiable iff $\Sigma$ is consistent

Harry Potter and the 11 Rules of Formal Deduction

symbols	rule	words
$(Ref)$	$A⊢A$	(Reflexivity)
$(+)$	If $\Sigma ⊢A$, then $\Sigma ,{\Sigma }^{\prime }⊢A$	(Addition of premises)
$(\neg ,-)$	If $\Sigma ,\neg A⊢B$ and $\Sigma ,\neg A⊢\neg B$ then $\Sigma ⊢A$	($\neg$ elimination) or proof by contradiction
$(⟹,-)$	If $\Sigma ⊢A⟹B$ and $\Sigma ⊢A$ then $\Sigma ⊢B$	($⟹$ elimination) modus ponens
$(⟹,+)$	If $\Sigma ,A⊢B$, then $\Sigma ⊢A⟹B$	($⟹$ introduction)
$(\wedge ,-)$	If $\Sigma ⊢A\wedge B$ then $\Sigma ⊢A$ and $\Sigma ⊢B$	($\wedge$ elimination)
$(\wedge ,+)$	If $\Sigma ⊢A$ and $\Sigma ⊢B$ then $\Sigma ⊢A\wedge B$	($\wedge$ introduction)
$(\vee ,-)$	If $\Sigma ,A⊢C$ and $\Sigma ,B⊢C$ then $\Sigma ,A\vee B⊢C$	($\vee$ elimination) proof by cases
$(\vee ,+)$	If $\Sigma ⊢A$ then $\Sigma ⊢A\vee B$ and $\Sigma ⊢B\vee A$	($\vee$ introduction)
$(⟺,-)$	If $\Sigma ⊢A⟺B$ and $\Sigma ⊢A$ then $\Sigma ⊢B$	($⟺$ elimination)
	If $\Sigma ⊢A⟺B$ and $\Sigma ⊢B$ then $\Sigma ⊢A$
$(⟺,+)$	If $(\Sigma ,A⊢B)$ and $(\Sigma ,B⊢A)$ then $\Sigma \models A⟺B$	($⟺$ introduction)

1.7 | Automated Theorem Proving by Resolution

A formal deduction system with a single rule: resolution

Resolution theorem proving is a method of formal deduction

• ”a giga proof by induction”
• The only formulas allowed are disjunctions (OR)
• There is only one rule: resolution

$$(C\vee p),(D\vee \neg p)⊢(C\vee D)$$

• To prove that $A_1,\dots A_n\models C$ is valid, show that the following is not satisfiable

$$\{A_1,\dots ,A_n,\neg C\}$$

• Prove that from this set, we can derive both $B$ and $\neg B$
• Do this by converting everything to CNF
• The resolvent of $p,\neg p$ is called the empty clause, signifying a contradiction

$$p,\neg p⊢\{\}$$

Example: Proving

$$p,p⟹q⊢q$$

Proof:

1. $p$ (premise)
2. $\neg p\vee q$ (premise)
3. $\neg q$ (negation of conclusion)
4. $q$ (resolving 1, 2 over $p$)
5. $\{\}$ (resolving 3,4 over $q$)

Proving argument validity with resolution

Resolution strategies

David Putnam Procedure (DPP)

Any clause corresponds to a set of literals (the literals contained in the clause). Thus, we can use set notation to express resolution: $C\cup \{p\},D\cup \{\neg p\}$ produces:

$$[(C\cup \{p\})\cup (D\cup \{\neg p\})]\backslash \{p,\neg p\}$$

DPP:

1. Remote all clauses with $q,\neg q$
2. Choose a variable $p$ in one of the clauses
3. Add all possible resolvents using resolution on $p$
4. Discard all clauses with $p,\neg p$

If in some step one resolves $p,\neg p$, the output is the empty clause (valid, empty backpack) If one never has such a pair, the output is no clause (invalid, no backpack)

Apply DPP to

$$\{\neg p,q\},\{\neg q,\neg r,s\},\{p\},\{r\},\{\neg s\}$$

1. Eliminating $p$ gives $\{q\},\{\neg q,\neg r,s\},\{r\},\{\neg s\}$
2. Eliminating $q$ gives $\{\neg r,s\},\{r\},\{\neg s\}$
3. Eliminating $r$ gives $\{s\},\{\neg s\}$
4. Eliminating $s$ gives $\{\}$ - the output is the empty clause, and this statement is una

Soundness and Completeness of DPP (proofs optional)

2 | First-Order Logic

2.10 | First-Order Logic

First-order logic

FoL elements: Domain, individuals, variables, functions, relations, quantifiers

Negating quantifiers

Nested quantifiers

2.11 | Syntax of First-Order Logic

FoL syntax

Propositional logic: formulas are recursively built starting from atoms (proposition symbols) by the 5 formation rules that describe the use of connectives First-order logic: Modelled as individuals with relationships

• Domain
• Terms
• Atomic formulas
• Formulas

Formal language of FoL ($\mathcal{L}$) Equality symbol $(\approx )$

Terms

$Term(\mathcal{L})$ is an individual or variable

FoL formulas

$Atom(\mathcal{L})$ is the simplest formula that has a T/F value $Form(\mathcal{L})$ are formulas

Unique Readability Theorem for FoL

$Sent(\mathcal{L})$ is the set of sentences

First-order languages

Ex: First order language of elementary number theory

• Equality relation: Yes
• Relation symbols: <
• Individual (constant) symbols: 0
• Function symbols: $s,+,\times$

2.12 | Semantics of First-Order Logic

First-order logic semantics

Valuations

Value of a term

Value of formulas

2.13 | Logical Consequence: Argument Validity

Logical consequence ($\models$)

Proving argument validity

(Universally) valid formulas

Proving that a formula is (universally) valid

Logical equivalence, Replaceability theorem

2.14 | Formal Deduction for First-Order Logic

Formal deducibility in FoL

Harry Potter and the 6 additional rules for formal deduction

symbols	rule
$(\forall -)$	If $\Sigma ⊢\forall A(x)$ is a theorem then $\Sigma ⊢A(t)$ is a theorem
$(\forall +)$	If $\Sigma ⊢A(u)$ is a theorem and $u$ does not occur in $\Sigma$ then $\Sigma ⊢\forall xA(x)$
$(\exists -)$	If $\Sigma ,A(u)⊢B$ is a theorem and $u$ does not occur in $\Sigma$ or in $B$, then $\Sigma ,\exists xA(x)⊢B$ is a theorem
$(\exists +)$	If $\Sigma \models A(t)$ is a theorem then $\Sigma ⊢\exists xA(x)$ is a theorem where $A(x)$ results from $A(t)$ by replacing some (not necessarily all) occurrences of $t$ by $x$
$(\approx -)$	If $\Sigma ⊢A(t_1)$ is a theorem and $\Sigma \models t_1\approx t_2$ is a theorem, then $\Sigma ⊢A(t_2)$ is a theorem where $A(t_2)$ results from $A(t_1)$ by replacing some (not necessarily all) occurrences of $t_1$ by $t_2$
$(\approx +)$	$\varnothing ⊢u\approx v$ is a theorem

Understanding the rules of formal deduction

Definition of formal deduction

Replaceability & Duality in formal deduction

Replaceability: If $B=C$, we can replace $B$ with $C$ Duality: A formula is the same if we exchange $\wedge ,\vee$, $\exists ,\forall$, and negate all atoms

Soundness and completeness

2.15 | Resolution for FoL and Automated Theorem Provers

Prenex Normal Form (PNF)

PNF = All quantifiers at the front

• No quantifiers also counts as PNF

Converting into PNF

• Eliminate all $⟹,⟺$
• Move all negations inward (only as part of literals)
• Standardize the variables apart
• Move all quantifiers to the front

Preprocessing: Existential-free PNF

Skolem functions allow us to remove all existential quantifiers by replacing them with variables

$$\forall x_1\dots \forall x_n\exists yA\to (\ast )\forall x_1\dots \forall x_n{A}^{\prime }$$

When working with formulas in existential-free PNF, all variables are implicitly considered to be universally quantified

Preprocessing: Clauses

Sane as formal logic: Put everything in CNF

Valid arguments & satisfiability of a clause set

Clause unification & resolution for FoL

Unifying

$$Q(a,y,z),Q(y,b,c)\to y_1=a,y=b,z=c$$

Proving FoL arguments valid by resolution for FoL

3 | Decidability and Peano Arithmetic

3.16a | Computation and Logic: Turing Machines

What is an algorithm?

A finite sequence of well-defined, computer-implementable instructions, typically to solve a class of problems or perform a computation.

The Halting Problem

Halting Problem: Does there exist an algorithm (program) that operates as follows:

• Input: A program P , and an input I to the program.
• Output: “Yes” if the program P halts on input I, and “No” otherwise.

Proved unsolvable by Alan Turing

• Construct $K(P)$ which calls $H(P,P)$ and outputs the opposite of it’s result
• Then you cannot tell if $K(K)$ halts

Turing Machines as a formal model of computation

A Turing Machine is a 7-tuple $M=(Q,\Sigma ,\Gamma ,\delta ,q_0,B,F)$ where

• $Q$ = the finite set of states of the finite control
• $\Sigma$ = the finite set of input symbols
• $\Gamma$ = the set of tape symbols such that $\Sigma \subset T$
• $\delta$ = the (partial) transition function such that $\delta :Q\times \Gamma \times \{L,R\}$, where L, R are “left” and “right”
• $q_0$ = the start state, a member of $Q$
• $B$ = the blank symbol, which is in $\Gamma$ but not $\Sigma$
• $F$ = the set of final, or accepting states, a subset of $Q$

Language accepted as a Turing Machine

Can be graphs

Turing machines as computers of functions

Types of Turing Machines

Total Turing machine = halts on every input Universal Turing Machine = can simulate the computations of every TM

The Church-Turing Thesis

”Any problem that can be solved with an algorithm can be solved by a Turing Machine.”

• It was proved that a Turing Machine is equivalent in computing power to all other, most general, mathematical models of computation.

3.16b | Undecidability of Universal Validity for First-Order Logic

Decidability and computability

A decision problem for which there exists a terminating algorithm that solves it is called decidable (solvable), otherwise it is undecidable (unsolvable)

• Solvable means there exists a total TM that accepts those and only those problem instances that lead to a “yes” answer

A total function that can be computed by a total Turing machine is called computable, otherwise it is called uncomputable.

• Uncomputable function example: the Busy Beaver function
• Let $B(n)$ be the max number of 1s that a TM with $n$ states and alphabet $\{1,B\}$ may print on a blank tape before halting

The satisfiability (is any set satisfiable) and universal validity (is any formula valid) problems for FoL are undecidable

Proving undecidability

Reduce it to a previously solved problem. Suppose you can reduce $P_1$ to $P_2$:

• If $P_1$ is decidable, we can’t conclude anything
• If $P_1$ is undecidable, so is $P_2$
• If $P_2$ is decidable, then so is $P_1$
• If $P_2$ is undecidable, we can’t conclude anything

Examples of undecidable problems

decider = a total TM that solves a decision problem

Undecidability of universal validity of FOL formulas

3.17 | Application of FoL: Peano Arithmetic (successors)

Formal deduction proofs of properties of equality $(\approx )$

Introducing a new kind of equality: $\approx$

First-order languages (theories)

A set of domain axioms + a system of formal deduction = a theory

• Number / set / group / graph theory
• Euclidean geometry
• Computable functions (lambda calculus)
• Relational databases

Number theory (Peano Arithmetic)

Number theory

• Domain: natural numbers $0,1,2,\dots$
• Addition $+$
• Multiplication $\cdot$
• Ordering $<$

Peano Arithmetic (PA) Symbols

• Individual (constant): 0
• Functions s (successor, $s(x)=x+1$), $+,\cdot$
• Relation: equality Axioms
• Axioms defining the unary function successor and binary functions addition and multiplication
• Axioms for induction

Harry Potter and the 7 Axioms for Peano Arithmetic

1. $\forall x(\neg (s(x)=0)$ - negating the successor is false
2. $\forall x\forall y(s(x)=s(y)⟹x=y)$ - successor is one to one
3. $\forall x(x+0=x)$ - addition by 0
4. $\forall x\forall y(x+s(y)=s(x+y))$ - successor addition
5. $\forall x(x\cdot 0=0)$ - multiplication by 0
6. $\forall x\forall y(x\cdot s(y)=x\cdot y+x)$ - successor multiplication
7. $(A(0)\wedge \forall x(A(x)⟹A(s(x)))⟹\forall xA(x)$ - idk bruh

Proofs in Peano Arithmetic

1. successor of a thing doesn’t equal the thing
2. a natural number is 0 or has a predecessor

Defining new arithmetic relations

• $u\le v$ iff $\exists z(u+z=v)$
• $u<v$ iff $\exists z(u+s(z)=v)$
• $Even(u)$ iff $\exists y(u=y+y)$
• $Prime(u)$ iff $(1\le u)\wedge \neg (\exists z\exists y((u=y\cdot z)\wedge (1<y)\wedge (1<z))$

Godel’s Incompleteness Theorem

Godel’s Incompleteness Theorem: Any consistent formal theory T with a decidable set of axioms, and that is capable of expressing elementary arithmetic (e.g., Peano Arithmetic), is syntactically incomplete, that is, there exists a formula expressible in T that can neither be proved nor disproved in T .

Can be proved using a contradiction including the Halting Problem

4 | An important application of logic to CS

4.18 | Formal Verification

Introduction: What and Why?

Techniques for showing program correctness

• Inspection
• Testing:
  • Black-box: tests independent of code
  • White-box: tests based on code
• Formal design verification

Formal program verification:

• Formally state the specification of a program with FoL
• Prove that the program satisfies the specification for all inputs
• Although this is undecidable (no terminating algorithm), there are some techniques

Framework for formal verification

1. Convert the English description of $R$ to logic (${\Phi }_R$)
2. Write a program $P$ meant to realize ${\Phi }_R$ in some given programming environment
3. Prove that the program P satisfies ${\Phi }_R$

Imperative programming: Defines control flow as statements that change a program states / describes how a program operators (FORTRAN, PASCAL, OOP languages) Declarative programming: Focuses on what the program should accomplish without telling it how to do it (SQL, functional programming, HTML)

We are verifying imperative (uses variables), sequential (no concurrency), and transformational (turns inputs to outputs) languages.

We use the core features of C/C++ and Java

• ints and bools
• assignment
• sequence
• if-then-else conditionals
• while loops

Pre- and Post-conditions

Hoare Triples:

$$(|P|)C(|Q|)$$

• $(|P|)$ = precondition
• $C$ = program or code
• $(|Q|)$ = postcondition

Specification is not behaviour

• Instead of $(|y\cdot y<x|)$, write $(y\cdot y<x)\wedge \forall z((z\cdot z<x)⟹z\le y)$

Partial and Total Correctness

Definition: Partial Correctness A Hoare triple is satisfied under partial correctness, denoted

$${\models }_{par}(|P|)C(|Q|)$$

if and only if an input satisfying $P$ given to $C$ terminates and satisfies $Q$

Partial correctness can be vacuously satisfied if the program never terminates

while true { x = 0; } // infinite loop

Definition: Total Correctness Partial correctness + every valid input terminates

If the input is altered (“consumed”), a program is satisfied under NEITHER partial nor total correctness

A Formal Proof System for Partial Correctness

Rewriting the pre and postconditions for correctness using FoL. Domain: Programs, program states, and conditions

• State(s) - “s is a program state”
• Condit(P) - “P is a condition”
• Code(C) - “C is a program”
• Satisfies (s,P) - “State s satisfies condition P”
• Termiantes (C,s) - “Program C terminates when given state s”
• result (C,s) - A FUNCTION that gives the state resulting from executing C with state s if C terminates (undefined otherwise)

Expressing correctness with FoL (Hoare triple $(|P|)C(|Q|)$) Partial correctness

$$\forall S\forall P\forall Q[State(S)\wedge Condit(P)|\wedge Condit(Q)⟹$$ $$(Satisfies(s,P)\wedge Terminates(C,s)⟹Satisfies(result(C,s),Q))]$$

Total correctness

$$(Satisfies(s,P)⟹Terminates(C,s)\wedge Satisfies(result(C,s),Q))]$$

Assignments

To prove partial correctness, use sound inference rules To prove termination, use ad-hoc reasoning (even though program termination is undecidable)

A partial correctness proof is an annotated program with justifications

Inference rule for assignment (assignment)

$$\overline{(|Q[E/x]|)x=E;(|Q|)}$$

• If the condition(s) / Hoare triples above the line are proved, then the Hoare triple under the line holds
• This means ”$Q(x)$ will hold after substituting all values of $x$ for E”
• $Q[E/x]$ is read as “Q with E in place of x” (x is a free variable)

Example ($Q(x)=x\approx 7,E=y+1$)

$$(|y+1\approx 7|)=y+1;(|x\approx 7|)$$

We usually work backwards from the postcondition

$$\begin{array}{rlrl}& ??& & (|Q[E/x])\\ & x=y;& & x=E;\\ & (|x>0|)& & (|Q|)\end{array}$$

Inference rules about implications (NOT FRACTIONS, BUT UNDERLINES)

Precondition strengthening (implied)

$$\frac{P⟹P^{\prime }(|P^{\prime }|)C(|Q|)}{(|P|)C(|Q|)}$$

Postcondition weakening (implied)

$$\frac{(|P|)C(|Q^{\prime }|)Q^{\prime }⟹Q}{(|P|)C(|Q|)}$$

Inference rules for instruction (composition)

$$\frac{(|P|)C_1(|Q|),(|Q|)C_2(|R|)}{(|P|C_1:C_2(|R|))}$$

• We find a midcondition Q for which we can prove the top (like transitivity)

Most proofs are constructed from the bottom upwards

Conditionals

(if-then-else)

$$\frac{P(|P\wedge B|C_1(|Q|))(|P\wedge \neg B|)C_2(|Q|)}{(|P|)\text{ if }(B)C_1\text{ else }{C}_2(|Q|))}$$

(if-then)

$$\frac{P(|P\wedge B|C(|Q|))(|P\wedge \neg B|)⟹(|Q|)}{(|P|)\text{ if }(B)C_2(|Q|))}$$

Proof strategy

1. Annotate the program using appropriate inference rules
2. ”back up” the proof: add an assertion/condition before each assignment statement
3. Prove any “implieds” (annocations from 1, assertions from 2)

While-Loops and Total Correctness

(partial-while)

$$\frac{(|I\wedge B|)C(|I|)}{(|I|)\text{ while }(B)C(|I\wedge \neg B)}$$

• $I$ = loop invariant (true both before and after each execution of the body of the loop)