# Does a statement exist which is its own proof?

In fake/pseudo mathematical notation: does there exist a statement `S` such that `S = Proof(S)`?

• If you tried feeding S = Proof(S) into a computer, you would have just created an infinite recursive loop, and you'd kill your app with a stackoverflow within seconds. Perhaps we can take the computer's lead here...let's not create stackoverflows in our own minds. I tend to avoid circular logic. A natural property of circles is that you can keep going forever but you don't really get anywhere... Nov 29, 2014 at 4:13
• "This sentence is true" Nov 29, 2014 at 10:17
• Cogito ergo sum? or how about the Weak Anthropic Principle? isn't this about what is a tautology? Feb 21, 2015 at 6:01
• Just to point out that the question being asked is "does there exist a statement `S` such that...", rather than "please present me with a statement `S` which is such that..." . Would a non-constructive existence proof satisfy what you're looking for, whitman (which Mauro has the canonical demonstration of below), or do you actually want to see examples for what `S` might be? Feb 21, 2015 at 20:01

Exploiting the technique of arithmetization of syntax of Gödel's incompleteness theorem we can formalize in a system T whose language contains a "certain amount of elementary arithmetic", like (first-order) Peano arithmetic PA or Robinson arithmetic Q, a provability predicate Prf(x, y).

With it we can "manufacture" a formula Prov(x) [i.e. ∃yPrf(x, y)] that holds of the number g iff the formula with Gödel number g is provable in the system T.

Now we apply the so-called The Diagonalization Lemma :

Let T be a theory containing Q. Then for any formula B(y) there is a sentence G such that G ↔ B(g), where g is the Gödel number of the formula G.

Now we have only to apply the Diagonalization Lemma to the formula Prov(x) to get :

S ↔ Prov(s)

where s is the Gödel number of the "diagonalized" formula S.

This is a statement that "express" its own proof ...

I don't know much (or any) formal logic, but I believe the sentence "It is possible to construct an English sentence with thirteen words in it" serves as its own proof (since to prove it's possible to do something, you only have to produce an example of it).

• It actually hinges on the difference between statements and propositions, but roughly speaking what you get is a statement that expresses a true proposition and serves as evidence of the truth of the proposition. Nov 29, 2014 at 12:07

The answer is yes. In a formal system a formula "S" is provable/derivable/deducible from a set of formulas "Gamma" if there is a finite sequence of formulas A1, A2, ..., An such that An=S and each Ai (1<= i <= n) is either an axiom, or a member of Gamma or derived by one of the inference rules of the formal system (Ex. Modus Ponens) using previous elements of the sequence.

Therefore for any formula S, we can define proof(S) to be the finite sequence defined above. So for any axiom "A", we have proof(A)=A (because the sequence of proof of axioms has only one member which is the axiom itself).

• I agree in spirit, but the sequence (A) of length 1 is not really the same thing as A. Feb 21, 2015 at 14:30
• @WillO Good point! But I think it is not a big problem. It's just the representation. I think We can slightly change the representational part in definitions (of WFF or Proof) to resolve this issue. Feb 21, 2015 at 21:01
• Yes, I agree with you. Feb 21, 2015 at 21:06

In classical logic is no possible because a valid statement is a formula, which is a sequence of primitive symbols (and, or, implies, etc.). By other hand, a proof is a sequence of formulas, where one is a deduction of previous formula.

Although, exists something called intuicionist logic, where a statement is a "construct", i.e, a statement which is a "construction" from other statement; in short, this statement is in self a consctruction. So, if one see this construction like a proof, you can assert "S = proof(S)", in the sense of intuitionism.

• If you state this argument, you must take into account that a proof is a (finite) sequence of formulae where each formula in the sequnce is (i) an axiom, or (ii) derived with a rule of inference (e.g. modus ponens) from previous formulae of the sequnce. Thus, a one-line proof with only an axiom as conclusion is a formally valid proof. Having sais that, I think that the OP's question means something more "vague": a statement expressing its own proof, that sound different ... Nov 29, 2014 at 16:37