<p>I am not sure if the question is on topic here, it seems to contain basic misunderstandings about logic and mathematics (e.g. "This seems ridiculous because 1+1=2 is commonly known as correct, which doesn't need a complicated proof."), and therefore seems more appropriate for Math.SE. </p>

<p>Nonetheless, there is something interesting and related to it in proof complexity:</p>

<p>I assume that you are familiar with the notion of a Cook-Reckhow <a href="http://en.wikipedia.org/wiki/Propositional_proof_system">propositional proof system</a>. Jan Krajicek has studied something similar to what you describe in the context of proof complexity named <a href="http://www.karlin.mff.cuni.cz/~krajicek/implicit.ps">Implicit Proofs</a>.</p>

<p>The idea is that sometimes we can give a proof of a tautology succinctly by providing a small circuit that generates the bits of a proof in a propositional proof system $Q$. The problem is how can we know the bits generated by the circuit really represent a proof? The size of the circuit can be small (polynomial in $n$) with $n$ inputs and can describe an object of size $2^n$, so constructing the complete proof and checking its correctness can be an unfeasible task. The solution is to give a proof of correctness of the succinctly represented proof in $Q$ in a proof system $Q&#39;$. This new proof system is called $[Q,Q&#39;]$ (note the $Q$ and $Q&#39;$ can be the same system). Furthermore, Krajicek shows that for reasonable behaving propositional proof systems $Q$, the resulting system $[Q,Q]$ can p-simulate the $Q$. And you can repeat this processes and obtain potentially stronger and stronger systems (note that if there is optimal proof system then this construction will not give a stronger system, but just another optimal one), and then you can take union of these systems and continue.</p>

CC BY-SA 3.0
2011-11-02T13:44:07.697Z
I think you'll get completely different (but both interesting) answers to this question here and Math.SE, so it's not clear one forum is better than the other.
Peter Shor 
CC BY-SA 3.0
2011-11-02T13:49:56.240Z
@Peter, I agree. My point is that these answers although potentially interesting are not what the OP is looking for. The problem with the question is the OP doesn't seem to be familiar with the basics, e.g. there is no complete recursively enumerable set of axioms for arithmetic. Similarly for the second question. We can salvage interesting on-topic question out of it (e.g. what are the obstacles current propositional theorem provers/SAT solvers are facing? or similarly in first order theorem proving) but they are different questions.
Kaveh
CC BY-SA 3.0
2011-11-02T13:34:36.617Z
2011-11-02T13:34:36.617Z
Kaveh
<p>A one-line proposition $A$ can generate a 100-page proof $p(A)$. Since the proof is very long, it's highly suspectable that there is a mistake in it, which cannot be found out even after careful proofread by many people. </p>

<p>So we should write a proof $p(p(A))$ to make sure $p(A)$ is correct. By a similar argument, we should have $p(p(p(A))), p(p(p(p(A)))), \dots$.</p>

<p>This seems ridiculous because $1+1=2$ is commonly known as correct, which doesn't need a complicated proof. So (from my own point of view) it's better to regard a proof as a decomposition of a proposition into a series of axioms. But there are two problems:</p>

<ul>
<li><p>How many axioms do we need? Are they consistent?</p></li>
<li><p>What is the structure of this decomposition (that makes it hard for a machine to do automatic proof)?</p></li>
</ul>

<p>It seems the first problem has something to do with Gödel's Incompleteness Theorem. I'd sincerely thank those who recommend me very clear and illustrative materials about it. I'd also like to know what background will be needed to understand it. I tried to read the original paper but didn't quite understand 
what are the more fundamental facts that we can rely on to prove this theorem. (Maybe Peano Arithmetic and ZFC?)</p>

CC BY-SA 3.0
2011-11-02T12:41:49.757Z
I think that A and p(A) have different types, and therefore your notation p(p(A)) does not make sense to me.
Tsuyoshi Ito
CC BY-SA 3.0
2011-11-02T13:25:45.643Z
I am reminded of Lewis Carroll "What the Tortoise Said to Achilles" [ http://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achilles ].
Ohad Kammar
CC BY-SA 3.0
2011-11-02T13:43:54.063Z
If you want to learn about incompleteness, IIRC, there was a question on Math.SE (or possibly on MO) about good books to learn the theorems. The first question "how many axioms..." is not research level (more suitable for Math.SE), and the second question is vague. Since it seems that you are talking about general theorem proving in first order logic (a provably undecidable problem), it seems again that you are not familiar with basics in logic and theorem proving which makes the question more appropriate for Math.SE.
Kaveh
CC BY-SA 3.0
2011-11-02T13:59:57.023Z
Maybe related : [how to shoot down your proofs](http://cstheory.stackexchange.com/questions/6589/how-to-shoot-down-your-proofs), however it wasn 't clear to me what the exact question is.
Gopi
CC BY-SA 3.0
2011-11-02T14:11:22.963Z
It's not meant to be about first order logic. I'm trying to understand the ambiguity of natural language, which seems to be more fundamental and difficult than (first order) logic. I want to decompose natural language in a structural way, and I'd like to know what ideas CS theorists and mathematicians may have. You can see mainstream natural language processing techniques are almost all about statistics and machine learning, which is not a structural way. And no practial machine translation system has ever worked decently. Anyway, I'm just interested in how other people think about it.
Cyker
CC BY-SA 3.0
2011-11-02T15:16:46.257Z
A considerable number of researchers in NLP, CL (Computational Linguistics), and KR (Knowledge Representation and Reasoning) work on non-statistical computational linguistics. Check the AI Q&A sites mentioned in the FAQ, I think they can be useful for what you want to know.
Kaveh
CC BY-SA 3.0
2011-11-02T15:25:00.147Z
ps: I would suggest that you also check [Torkel Franzen's book](http://books.google.com/books/about/G%C3%B6del_s_theorem.html?id=71pK8Zz9Dd8C), Godel's incompleteness has been quite prone to misuse.
Kaveh
CC BY-SA 3.0
2017-07-06T03:59:56.117Z
@Cyker in response to your comment, this is slightly off topic but if you are okay with picking up a new language [Lojban](https://en.wikipedia.org/wiki/Lojban) is a conlang where every sentence you say in it is unambiguous.
Phylliida
<lo.logic>
How to prove a proof is correct
Cyker
# How to prove a proof is correct

(Asked by: username_0 on 2011-11-02)

A one-line proposition $A$ can generate a 100-page proof $p(A)$. Since the proof is very long, it's highly suspectable that there is a mistake in it, which cannot be found out even after careful proofread by many people.

So we should write a proof $p(p(A))$ to make sure $p(A)$ is correct. By a similar argument, we should have $p(p(p(A))), p(p(p(p(A)))), \dots$.

This seems ridiculous because $1+1=2$ is commonly known as correct, which doesn't need a complicated proof. So (from my own point of view) it's better to regard a proof as a decomposition of a proposition into a series of axioms. But there are two problems:

* How many axioms do we need? Are they consistent?
* What is the structure of this decomposition (that makes it hard for a machine to do automatic proof)?

It seems the first problem has something to do with Gödel's Incompleteness Theorem. I'd sincerely thank those who recommend me very clear and illustrative materials about it. I'd also like to know what background will be needed to understand it. I tried to read the original paper but didn't quite understand
what are the more fundamental facts that we can rely on to prove this theorem. (Maybe Peano Arithmetic and ZFC?)

**Tags:** lo.logic

> **Comments:**
> **username_1**: I think that A and p(A) have different types, and therefore your notation p(p(A)) does not make sense to me.  
> **username_2**: I am reminded of Lewis Carroll "What the Tortoise Said to Achilles" [ http://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achilles ].  
> **username_3**: If you want to learn about incompleteness, IIRC, there was a question on Math.SE (or possibly on MO) about good books to learn the theorems. The first question "how many axioms..." is not research level (more suitable for Math.SE), and the second question is vague. Since it seems that you are talking about general theorem proving in first order logic (a provably undecidable problem), it seems again that you are not familiar with basics in logic and theorem proving which makes the question more appropriate for Math.SE.  
> **username_4**: Maybe related : [how to shoot down your proofs](http://cstheory.stackexchange.com/questions/6589/how-to-shoot-down-your-proofs), however it wasn 't clear to me what the exact question is.  
> **username_0**: It's not meant to be about first order logic. I'm trying to understand the ambiguity of natural language, which seems to be more fundamental and difficult than (first order) logic. I want to decompose natural language in a structural way, and I'd like to know what ideas CS theorists and mathematicians may have. You can see mainstream natural language processing techniques are almost all about statistics and machine learning, which is not a structural way. And no practial machine translation system has ever worked decently. Anyway, I'm just interested in how other people think about it.  
> **username_3**: A considerable number of researchers in NLP, CL (Computational Linguistics), and KR (Knowledge Representation and Reasoning) work on non-statistical computational linguistics. Check the AI Q&A sites mentioned in the FAQ, I think they can be useful for what you want to know.  
> **username_3**: ps: I would suggest that you also check [Torkel Franzen's book](http://books.google.com/books/about/G%C3%B6del_s_theorem.html?id=71pK8Zz9Dd8C), Godel's incompleteness has been quite prone to misuse.  
> **username_5**: @username_0 in response to your comment, this is slightly off topic but if you are okay with picking up a new language [Lojban](https://en.wikipedia.org/wiki/Lojban) is a conlang where every sentence you say in it is unambiguous.  

---

## 1 answers

### Answer by username_3 on 2011-11-02. Score: 6 | Accepted answer

I am not sure if the question is on topic here, it seems to contain basic misunderstandings about logic and mathematics (e.g. "This seems ridiculous because 1+1=2 is commonly known as correct, which doesn't need a complicated proof."), and therefore seems more appropriate for Math.SE.

Nonetheless, there is something interesting and related to it in proof complexity:

I assume that you are familiar with the notion of a Cook-Reckhow [propositional proof system](http://en.wikipedia.org/wiki/Propositional_proof_system). Jan Krajicek has studied something similar to what you describe in the context of proof complexity named [Implicit Proofs](http://www.karlin.mff.cuni.cz/~krajicek/implicit.ps).

The idea is that sometimes we can give a proof of a tautology succinctly by providing a small circuit that generates the bits of a proof in a propositional proof system $Q$. The problem is how can we know the bits generated by the circuit really represent a proof? The size of the circuit can be small (polynomial in $n$) with $n$ inputs and can describe an object of size $2^n$, so constructing the complete proof and checking its correctness can be an unfeasible task. The solution is to give a proof of correctness of the succinctly represented proof in $Q$ in a proof system $Q'$. This new proof system is called $[Q,Q']$ (note the $Q$ and $Q'$ can be the same system). Furthermore, Krajicek shows that for reasonable behaving propositional proof systems $Q$, the resulting system $[Q,Q]$ can p-simulate the $Q$. And you can repeat this processes and obtain potentially stronger and stronger systems (note that if there is optimal proof system then this construction will not give a stronger system, but just another optimal one), and then you can take union of these systems and continue.

> **Comments:**
> **username_6**: I think you'll get completely different (but both interesting) answers to this question here and Math.SE, so it's not clear one forum is better than the other.  
> **username_3**: @Peter, I agree. My point is that these answers although potentially interesting are not what the OP is looking for. The problem with the question is the OP doesn't seem to be familiar with the basics, e.g. there is no complete recursively enumerable set of axioms for arithmetic. Similarly for the second question. We can salvage interesting on-topic question out of it (e.g. what are the obstacles current propositional theorem provers/SAT solvers are facing? or similarly in first order theorem proving) but they are different questions.  

---

