Does a statement exist which is its own proof?

Question

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

Answer 1

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

Answer 2

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

Answer 3

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

Answer 4

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.