I recently become interested in math and math proofs and I started doing math proofs and researches and I am interested in how actually a math proof is made? Which steps can lead us from axioms and definitions to actual goal?
So, I tried to write computer program which will be able to prove or disprove given statement just by following path from axioms to the statement. Of course, according to Godel's theorem there are infinitelly many unprovable stetements for any set of axioms. However, if it is unprovable, it should be possible to prove that it cannot be proved using existing axioms.
Now, lets forget about known math and lets introduce just axioms and definitions we need and lets try to prove the simplest possible statement. First of all, lets use standard mathematical definitions of sets. Basically {} is a set, it has no definition, it exists by itself. It can contain finitelly or infinitelly other sets or can be empty (standard properties of set).
Also, lets introduce set relations:
Set $b$ contains set $a$: $a\in b$
Set $a$ contains only sets which are in $b$: $a=b$
Set $b$ contains all sets which are in $a$ and at least one more: $a\subset b$
Set $c$ contains only sets which are either in $a$ or $b$: $c=a\cup b$
Set $c$ contains only sets which are both in $a$ and $b$: $c=a\cap b$
Set $c$ contains only sets which are in $a$ and not in $b$: $c=a\setminus b$
Finally, lets introduce quantificators:
There are at least one set $a$ which is in set $b$ for which statement $P$ is true: $(\exists a\in b)P$
For all sets $a$ which are in set $b$ statement $P$ is true: $(\forall a\in b)P$
Ok, now we need to introduce some new definitions to make the above definitons useful. So, let $\mathbb{N}$ be the set defined as: $$\mathbb{N}=\left\{\{a\}|a\in\mathbb{N}\right\}\cup\{\{\}\}$$ Each element of $\mathbb{N}$ is called a natural number. Also, let $$1=\{\}$$ And the final definition I want to introduce is comparison. Lets define comparison of two natural numbers as following: $$(\forall a,b\in\mathbb{N})a>b\iff a=\{b\}\lor(\exists c\in\mathbb{N})a>c>b$$
Thats all of definitions (or you can call them axioms). Then I came up with the following problem:
Prove the following statement: $$(\exists a\in\mathbb{N})a>1$$
The problem is very obvious, but is it really simple as it looks? Of course, this is one solution:
By definition of comparison we have that $\{\{\}\}>1$ and by definition of natural numbers $\{\{\}\}\in\mathbb{N}$. Finally, by definition of quantificators, if there is at least one set which satisfiest the given condition, then the statement is true.
But this solution doesn't explain how we came up with it. As I said, I'm trying to create a program which will be able to prove statements just by following the given axioms. We defined everything very preciselly, so the steps from axioms to the proof should be precise and clear as well.
How would you explain what is the reasonable explanation why would someone came up with the solution I posted? I was thinking a lot about it and I couldn't find any explanation. How would I explain computer which steps to follow to come up with such a proof. In the proof someone just said "By definition of comparison we have that $\{\{\}\}>1$". That doesn't explain why they choosed exactly that example. Why not chosing other examples? As you know, in sets there are no order of elements, there is no next or previous. For example if we just say that $27^5+85^5+11^5+133^5=144^5$ is a counterexample to Euler's conjecture on sums of like powers, does it explain how we came up with exactly that counterexample? Of course not. So basically, in such an easy environment of definitions and axioms, what are some general logic ways of generating a proof or disproof to some statement from given set of axioms? Also, how would you prove the example problem I posted? Have you any other approach?
Stripping away some commentary, I think there are a couple main questions here:
This is the subject of automated theorem proving. If we drop the word "efficiently," then it's not hard to write a "proof-searching" program, which will eventually find a proof of $p$ if such a proof exists. Of course, this is an absolutely terrible approach, since the number of possible proofs of length $n$ grows exponentially with $n$.
If we try to do things efficiently, then stuff gets interesting. Researchers into automated theorem proving have found a number of techniques for simplifying the search for proofs, and in a number of cases have managed to use ATPs to prove new theorems! However, the task of improving the methods of proof search is essentially an endless one.
You also say:
This suggests the question:
While related to the previous question, it's ultimately a different one - a formal proof need not, sadly, provide understanding! It just has to prove that the statement in question is true. Issues around picking "test counterexamples" efficiently are seriously studied in automated theorem proving, but it's important to point out the difference between efficiently finding proofs and finding explanations for proofs; in particular, what constitutes a satisfying explanation is not at all precisely definable.
I suggest you take a look at the (extremely extensive) literature around automated theorem proving (and related subjects, like interactive/computer-assisted theorem proving, and computer proof verification).