Information Proof Theory

Table of Contents

Chapter 1. Structure of logical expressions and proofs

Chapter 2. Proof execution

Chapter 3. Predicate logic formula and proof

Chapter 4. Logical correctness of hardware

Chapter 5. Semantic correctness of hardware

Chapter 6. Logical model 1 of software

Chapter 7. Logical model 2 of software

Chapter 8. Making programs with functions


Mizar Library Ver.7.0.05m4.09.842


Information Proof Theory

Information proof theory is a new field. In the past, "proof" was a field of mathematics. This does not necessarily mean this word was not used in other fields. However, it does not seem that people have the question "what is a proof?".

Mathematicians like the word "exactitude", but few know what a proof is "exactly".

The world is infested with things that are "not exact". The curriculum guidelines of textbooks in high schools say "developing logicality". However, if a student who is excellent in logicality goes out into the real world, he/she cannot live because the world is full of illogical things.

People who lead others tend to be illogical. "Chops and changes" are normal. Men in power can say what they want like "a wise man changes his mind, a fool never".

The subordinates fall victim to a leader's absurdities. They try to cover organizational disadvantages caused by the leader's absurdities, maximizing their positive attributes.

Therefore, subordinates are more logical than leaders. Plant foremen can predict that an inadequate placement of a heavy equipment is dangerous. That is due to his experience, but he seems to make a deduction logically.

Engineers also think pretty logically in their field.

As well, district courts judge more logically in the field of law. The higher the court, the more the judgment is sometimes avoided for "a highly political matter". Was the "separation of three powers" that we learned a mistake?

Unfortunately, people who are exactly logical have been disadvantaged until now.

Despite this, why do we have to learn it here?

This is because it appears certain that it has been true until now, but it will not be true from now on. The reason is that the utilization of computers in the world has increased because of the development of computers.

A computer consists of millions of logic elements. In addition, when software is running there is code of millions of steps defined exactly.

Human beings are being released to the world of logic which exceeds the limits of their mental capacities from the logic of the level such as "every man is mortal, Socrates is a man, therefore, Socrates is mortal".

I mentioned that mathematicians like the word "exactitude", but actually they are not exact at all in terms of the strictness of computers.

There has been an attempt in trying to prove the exactitude of computer programs mathematically for quite a long time, but it has not been practical. Proofs by mathematicians with papers and pencils were very inaccurate, the result of which could not been trusted. Only very easy programs could be proved.

However, currently there is a tool for proof, which is a software application called Proof Checker. The typical one is Mizar.

This tool allows exact checking even with a proof of millions of steps. And it has a high affinity for the environment of LSI design and program development because computers are used.

In addition, because propositions proved are disclosed on the Internet, correct propositions, software and circuits can be accumulated by volunteers around the world.

If this excellent tool can be mastered, advanced products will be able to be designed and produced, and tangible and intangible goods which allow gaining an advantage over competitors will be obtained.

In addition, the logicality and the tool to check it will not only give a technical advantage, but also affect the human mind. As a matter of fact, logicality is important to understand others.

Assume there is a man who says "we may hit someone other than oneself". Logically speaking, people who agree with it may hit him freely.

The library of Mizar is an asset shared by all human beings. This means that it is the commonest assemblage of ideas. Regardless of the difference between skin colors, the differences of sex, rich and poor, this assemblage of ideas is available and applicable.

The difficulty of persuading someone by logic will generally continue in the future. However, it will be useful when you decide your action. In addition, even if there are not many powerful people in the world who place importance on logicality, they will be on your side. We cannot touch the hearts of others by the logic, but you do not have to feel pessimistic. Think that people who are unmoved by logic are much the same as a beast that takes a bait and is caught.

Now, I will introduce you to the "exact" world of "proof". If you want to learn Mizar in more detail or you do not understand it well from the description so far, please read the text "Transcript of a lecture on Mizar".