It is possible to construct first-order theories which prove their own consistency (and which are incomplete). Here is one example.

Consider a first-order theory with equality with a constant symbol 0 (zero), a unary predicate symbol N (the natural numbers), and a binary predicate symbol σ (the sequential relationship). Make the usual Peano Axiom assumptions, with the exception that one does not assume that σ is a total function, i.e. one does not assume that, for every natural number, there exists a natural number which is its successor. That is, it assumes every axiom in the following list except PA3:

(PA1) Ν0

(PA2) ∀n∀m ( Νn & σn,m ⇒ Νm )

(PA3) ∀n ( Νn ⇒ ∃m σn,m )

(PA4) ∀n∀m∀m' ( Νn & σn,m & σn,m' ⇒ m = m' )

(PA5) ∀n∀m∀n' ( Νn & Νn' & σn,m & σn',m ⇒ n = n' )

(PA6) ∀n ( Νn ⇒ ¬ σn,0 )

(PA7) Induction schema. Let φ be a well-formed formula where m does not occur
and n is not a bound variable. Suppose φ[0\n] and
∀n∀m ( Νn & σn,m & φ ⇒ φ[m\n] ). Then ∀n ( Νn ⇒ φ ).

Now add a 3-ary symbol ∂. ∂f,x,n can be thought of as meaning that f is a sequence whose nth term is x. Make four assumptions about ∂:

(SEQ1) ∀x ( Nx ⇒ ∃f ∀i∀y (∂f,i,y ⇔ i = 0 & y = x) )

(SEQ2) ∀f ∀n∀m∀x ( ∂f,m,x & Nn & σn,m ⇒ ∃y ∂f,n,y )

(SEQ3) ∀f ∀n∀m∀x∀y ( ∂f,n,x & Ny & Nm & σn,m
⇒ ∃g ( ∂g,m,y & ∀i(¬ i = m ⇒ ∀z(∂f,i,z⇔∂g,i,z)) ) )

(SEQ4) ∀f∀i∀x∀y ( ∂f,i,x & ∂f,i,y ⇒ x = y )

Call this theory fpa. The most important thing to take away from fpa is that its ontological assumptions about the naturals are downward. That is, if a natural number n exists, then one can prove that all natural numbers less than n exist and have all the normal properties, but not that any number greater than n exists. As to sequences, if a natural number n exists, one can prove that there is a sequence from 0 to n but not any longer, and all properties of sequences and subsequences up to length n hold.

It is easy to define addition and multiplication formulas which have all the usual properties, with the exception of totality. E.g. one can prove commutativity of addition

+(x,y,z) ⇒ +(y,x,z)

even though one can't prove, given x and y, that there exists such a z.

Continue in this way. Define a predicate one(x) to abbreviate Nx & σ0,x. Again, one can prove all the usual properties of 1 except that it exists. Define two(x) and so forth.

Prove simple facts about sequences, in particular what it means for h to be the concatenation of f and g. Again, remark that given f and g, one cannot prove that h exists.

Now provide some Godel numbering for your system. Say use one(x) to represent left-parenthesis and two(x) to represent right-parenthesis and so forth. variable(x) can be defined by ∃y (ten(y) & x > y). (I haven't said how to define > but it's defined in the obvious way.)

A string, a formula, and a proof are just sequences of symbols. You can define what it means to be a term, an atomic wff (it's a particular kind of sequence), and then a wff (another particular kind of sequence). Eventually you can define the particular sequences which are proofs. That is, Proof(s) will state that sequence s represents a proof (as usual one will not be able to prove that there exists a sequence which is a proof). Finally, define the consistency of fpa as the wff Cons asserting the non-existence of a proof of the wff ¬ 0 = 0.

One proves Cons as follows. Suppose there exists a sequence-proof of the contradiction ¬ 0 = 0. But fpa can be modeled by a model of a single element, 0. For atomic wffs Nt, ∂f,t,u, and t = u assign the value of true. For atomic wffs St,u assign the value false. Continue in the obvious way. For instance a wff equivalent to ∀x(W) gets assigned the value that W has. Then one can prove that every wff gets assigned one and only one value (true or false), all the axioms will be assigned true, and that Modus Ponens and Generalization preserve truth. Hence, one can prove that every step in any proof in fpa must be true. But ¬ 0 = 0 is assigned the value false. This is a contradiction. Hence there does not exist a sequence-proof of a contradiction, i.e. fpa is consistent. But one has proved this *in* fpa, i.e. fpa has proved its own consistency.

Whether a statement is equivalent to consistency of the theory might be ambiguous: indeed.Is there a standard way of addressing this issue: not really, I’m afraid. Generally, you just hope that your readers will recognize a “reasonable” formalized expression of consistency when they see it. Therearemore-or-less standard ways how to construct provability predicates for sufficiently strong theories (which are then subject to the 2nd incompleteness theorem), but this is no good for your question. $\endgroup$ – Emil Jeřábek supports Monica Feb 26 '16 at 17:31presumablynot expressive enough to meaningfully formulate its own consistency (but I have no idea how to state this formally). $\endgroup$ – Emil Jeřábek supports Monica Feb 26 '16 at 17:36