Propositional and First Order Logic

• quantumdude
In summary: I think the situation for second order systems is that they are usually not decidable, but can be "incomplete" in the sense that there exist statements that are true, but not provably so.HurkylIn summary, it is believed that total formalization of mathematics is possible in theory, but it is a tedious and time-consuming process. This is due to the need for rigorous proof and the use of reducibility to reduce higher level contexts to formal set theory. There have been attempts at creating a mathematical database that combines automated theorem proving with a comprehensive reference, but it has not been fully realized. However, the study of mathematical logic remains a useful and

quantumdude

Staff Emeritus
Gold Member
Is total formalization possible? If not, why not?

The following is a first course in formal mathematical logic.

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.

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

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. :)

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.

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

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.

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".

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

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.

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.

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.

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

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)

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

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

From page 8, paragraph 2:
"For example, A1123, (A2-->(~A0)), and (((~A1)-->(A1-->A7) are all formulas, but X3,..., are not."

Why is X3 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?

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

>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...

1. What is propositional logic?

Propositional logic, also known as sentential logic, is a branch of mathematical logic that deals with the study of propositions and logical relationships between them. It uses symbols to represent propositions and logical connectives to combine them to form compound propositions.

2. What is first-order logic?

First-order logic, also known as predicate logic, is a branch of mathematical logic that extends propositional logic by incorporating the use of quantifiers and variables to create more complex statements. It allows for the representation of relations between objects and enables reasoning about objects and their properties.

3. What is the difference between propositional and first-order logic?

The main difference between propositional and first-order logic is that propositional logic does not allow for the representation of relations between objects, while first-order logic does. This means that first-order logic is more expressive and can capture more complex statements and arguments.

4. How are propositional and first-order logic used in science?

Propositional and first-order logic are used in science to formalize reasoning and make arguments more precise and rigorous. They are particularly useful in computer science, artificial intelligence, and mathematics, where they can be used to model and solve problems in a systematic and logical manner.

5. What are the practical applications of propositional and first-order logic?

Propositional and first-order logic have numerous practical applications in various fields, including computer science, linguistics, philosophy, and mathematics. They are used in automated reasoning systems, natural language processing, database querying, and automated proofs, among others.