This is the first pass for the Nov 5 notes. It's needs to be organized some more. Feel free to pitch in.

Logic/decidability

Lynn’s solution to Grandfather proof in PS4 is “gold standard.” We are not expected to have proofs as detailed.

The grandfather problem helps motivate the topics of today’s lecture.

Computer should be able to read proof line by line. Proofs written this way can be automatically checked by computer.

Prolog example file->beginning of proof checker.

http://www.ps.uni.sb.de/~duchier/python/prolog.py

Lots of provers and proof checkers on web.

We can treat logic as data and manipulate logical artifacts. This is interesting in several contexts. Lynn’s favorite paradox: “every rule has an exception.” This begs the question whether that rule has an exception. “Everything I say is a lie.” These are not actually true paradoxes. A paradox is something that cannot be true or false. “This sentence is false” is a true paradox.

Paradoxes

Paradoxes have way for of reaching out and grabbing themselves. There is not enough machinery in propositional calculus, boolean logic, etc to reach out a grab a statement. Propositional logic does have enough machinery. For example, quotations and arithmetic do allow self-reference.

Godel incomplete theorem

Sound: if you can prove it, it’s true (consistent)

Completeness: if it’s true (expressible in the system), you can prove it

Consistent: no contradictions

p^~p is clearly false; from a false thing you can prove anything:

(p^~p)->we all win megabucks

Once you have inconsistency, the whole system is shot; garbage in/garbage out

Once you have inconsistency, you can infer anything

N proposition->2^n truth assignments

In propositional logical, there are 2^n things to check Predicate logic is more complicated b/c quantifiers, etc.

Godel said for any predicate logic formula, you can encode it as string of numbers (a piece of manipulatable data). He used arithmetic of primes, but today we would use data on a computer.

Any system that contain

You give me the encoding of the formula, I will tell you that X property holds for this formula or that it doesn’t hold

GroundConjunction(x) iff x is the Godel number (encoding of a sentence that is the conjunction of ground fact)

Encoding is independent of value of variable

Sunny(today) ^ raining(yesterday)

• x sunny(x) ^ raining(successor(x))

Godel devised way of deciding whether something is provable or not

2^x*3y*5^27 Using primes in order, allow reconstruction of order

In GroundConjunction(x), we have function that allows you take an input (an sentence) and mechanically check it

Barber’s paradox: There is a certain town where the barber who shave men only if they don’t shave themselves. Does the barber shave himself?

System we’re using is consistent-if we can come up with a proof, then the statement is true but may not be complete

Provable (x) iff is Godel # or provable sentence

Self-unprovable (z) iff x is Godel’s # of a sentence that is not provable when applied to self.

1. E is Godel # of some sentence/predicate F(x) 2. y is Godel # of F(Godel # F) 3. ~provable(y)

Asking self-unprovable (self-unprovable) gets you in trouble Assume provable that means (by #3) -> Provable(selfun(selfun))

Now, assume false. Then can’t prove (because sound). So it’s true. Is it possible for it to be true and unprovable?

When you add arithmetic to logical system or some other way of getting self-reference, you will encounter sentences that are true but not probable

Second Incompleteness theorem, let’s take machinery that let you say system is consistent to the system itself, the system becomes incomplete

Three levels:

-Works but not interesting

-Interesting but things you can’t quite reach

-You can reach everything

Barber’s paradox is variation of Russell’s Paradox:

{w| w is prime, W N} {w|w contains a prime N} {w| w has a prime # elts} {w|w doesn’t contain itself} {w|w is this set}

Does the set contain itself or not?