Propositional and First Order Logic

[quantumdude]

Is total formalization possible? If not, why not?

The following is a first course in formal mathematical logic.

http://www.trentu.ca/academic/math/sb/pcml/pcml-i-15.pdf

Looking through the book, I do not see any that the author presupposes any mathematical knowledge. Volume II, Computability and Inccompleteness, will lead us to Goedel's theorem.

 

[Hurkyl]

I believe so. The whole idea of rigorous proof is that any proof can be formalized in a given context. Then the idea of reducibility allows you to take a high level context (like Differential Geometry) and reduce it through a ladder of contexts until you're at formal set theory which is, of course, formal.

So, in theory, we already know how totally formalize mathematics. The problem is that it's a pain to do by hand. Actually, there is a proof style that partially encompasses this idea. You write your proof in outline format. The highest level is the general sequence of steps you use to prove the theorem. Beneath each level is a sketch of the proof of that step. Beneath each step in that sketch is a proof, and so on. Eventually you get to a point where you consider it obvious, go one more step, and voila! The advantage to this is that the reader can choose his level of detail when reading your proof. The disadvantage is that it's a lot of work explicitly writing things instead of the common practice of leaving it to the reader.


I once had a grand idea of making a mathematical database of theorems that essentially follows the above ideas. In the proof of any theorem you could follow hyperlinks to the proofs of the substeps, which the database manager would provide automatically (or prompt the person who enters the theorem to provide more detail, should the database be unable to flesh it out automatically). And, of course, you could submit a set of premises to the database and it could spit back a list of things you can conclude from it.

I've abandoned the idea, not because I think it won't work, but because I don't think I can carry it out myself.

Hurkyl

 

[damgo]

I hope you get someone interested in going through this, Tom... it's cool stuff. I might be able to answer questions... van Dalen's logic book is around here somewhere, and I sort of remember how to keep my |-'s and |='s straight.

Hurkyl -- you might try a web search on "automated theorem proving"... there's a lot of stuff on this! There's a program called Otter that does OK on easy proofs, but it's a tough problem. :)

 

[selfAdjoint]

Total formilization is not possible. As you will find out when you get to volume II, first order propositional calculus is decidable, but second order propositional calculus is not. That is, there exist formal statements within it that can both be proved and disproved.

The great mathematician Hilbert, at the turn of the twentieth century, started a program to develop all of mathematics from a few axioms by formal logic. In the 1930s Goedel proved this program was impossible.

But not to worry, even if you can't prove all of mathematics with it, mathematical logic is a beautiful and useful branch.

 

[Hurkyl]

Yah, I know some elementary automated theorem provers exist. My goal for the database was a combination of being a comprehensive reference as well as an automated theorem verifyer.

That is, there exist formal statements within it that can both be proved and disproved.

I assume you meant "can't" not "can"?


Incompleteness is indeed an obstacle to automation... but since you can't prove an unprovable statement, formalization will never be faced with an unprovable proof to formalize.

Hurkyl

 

[quantumdude]

Originally posted by Hurkyl
I assume you meant "can't" not "can"?

No, I think he meant "can".

Incompleteness (snip)

He's not talking about incompleteness, he's talking about inconsistency. Correct me if I'm wrong, but what Goedel showed is that a formal system at least as powerful as arithmetic is either incomplete or inconsistent.

In the latter case, there are statements that can be both proved and disproved.

But, we digress, that is the subject of Volume II.

I'll post a few notes on Ch I of Volume I soon.

 

[selfAdjoint]

I did indeed mean "can". There exists a valid proof of such a statement ( a series of logical propositions each one implying the next, beginning with the axioms and ending at the statement in question), and there also exist another valid proof of the denial of the statement.

And such a statement is not just theoretical. Actual undecidable propositions have been constructed. Penrose discusses one of them in his book "The Emperor's New Mind".

 

[Hurkyl]

I did indeed mean "can".

That's a new one for me, then. *hurries off to download the second volume*


I know inconsistent axiomatic systems can have statements that are both provable and disprovable, but I've never heard it said that 2nd order logic is inherently inconsistent.

Hurkyl

 

[damgo]

selfAdjoint, I think you are talking about inconsistency? If a proposition is both provable and unprovable, then ALL propositions in that particular formal system are both provable and unprovable and the system is useless.

In first-order logic, Godel's Completeness theorem states that all statements that are "always true" (true in all models/structures) can be proved and vice versa.

In (some defs of) second-order logic, this is not true in general.

 

[selfAdjoint]

If a proposition is both provable and unprovable, then ALL propositions in that particular formal system are both provable and unprovable and the system is useless.

Sigh, you guys study some more. What I said was accurate. There exist undecidable propositions in second order propositional calculus. It doesn't follow that if one proposition is undecidable then all are. This is all old math and you can find it online, I am sure.

 

[damgo]

Undecidability is usually something different: a system is decidable if there exists either a proof or disproof for any given statement. Alternatively, if there is an algorithm to determine validity of any statement in a finite amount of time.

 

[Hurkyl]

Yes, undecidability is, pardon the pun, decidably different!

I skimmed the second volume (by looking for all occurances of "second") and it does give assert that recursive systems are incomplete and cannot prove their own consistency, but it does not prove that they're inconsistent.

Hurkyl

 

[damgo]

Just on a side note... you've got to be really careful skimming/interpreting logic stuff. I've got books that appear to blatantly contradict each other, and even themselves, because so much rests on subtle but important definitions. eg there are at least three different notions of proof:
1) Formal proof in a system... eg natural deductions
2) Proofs about a formal system or all formal systems done in plain English... sort of "meta-proofs"
3) Sentences constructed in a formal system designed to express some notion of proof/provability.

So all the "ifs" and "thens" and "->"s are in one of these contexts... also there are more having to with diff models... and if you change one in some theorem you read you can easily end up with a false statement and get confused. (happened to me many times)

 

[Hurkyl]

Yah, I had a couple of those problems trying to teach myself the chapter on logical theories in my Theory of Computation text (we didn't cover it in class).

Good advice, though, I'll have to keep it in mind when I take the time to delve more deeply into the subject.

Hurkyl

 

[quantumdude]

OK, now that the 'completeness' argument has died down , I have a few questions on Ch. 1.

From page 8, paragraph 2:
"For example, A₁₁₂₃, (A₂-->(~A₀)), and (((~A₁)-->(A₁-->A₇) are all formulas, but X₃,..., are not."

Why is X₃ not a formula? Is it just the simple fact that the letter "A" must be used? This also has me confused on Exercise 1.1.2, where "Y" is used.

Now, on to Exercises 1.2-1.5. These are all intuitively obvious, but the exercises call for proofs. They are supposed to be proofs by induction, but I'll be damned if I know what the statement P(n) for the integer n is. Any ideas?

 

[Hurkyl]

I think a restatement of part 4 of definition 1.2 may help:

"If &alpha is a formula, then it can be created using a finite number of applications of rules 1, 2, and 3"

Hurkyl

 

[damgo]

>Is it just the simple fact that the letter "A" must be used?
Yup.

These first proofs are all induction on the construction rules. For p(formula) consider the ways to construct formulae with a max and min number of parenthesis...