I recently asked whether the axioms are tautologies, and got comments that seemed to me highly suspicious. Namely, that you can always prove an axiom from itself, that you can trivially say A therefore A, e.g.

"Axioms are unprovable from outside a system, but within it they are (trivially) provable."

And by another individual,

Every axiom has a proof. If A is an axiom, its proof is A. A one-liner.

It is my understanding that no system can prove its own validity without becoming inconsistent, via Gödel.

First, if we accept trivial proofs for various axioms don't we end up failing that? Second, what about, as another commenter noted, the Axiom of Identity? Since the one liner is basically A=A can't we prove this axiom from itself? It might be possible to trivially prove A therefore A for other axioms, but isn't this ability granted by the axiom that says A=A? How can this be valid?

  • A=A
  • "A=A" = "A=A"
    • Therefore A=A.

Doesn't at least one axiom need to assert essentially that all tautologies are true? And is it really valid to prove that with itself? And am I wrong to say that one of the implications of Gödel is that such things cannot be self-proved without the system being inconsistent?

  • I believe I was the same individual in both cases. Though I'm often not myself. The finite string of well-formed formulas "A" is a proof of A. If you don't get that, just go look up what a formal proof is. What I'm saying is neither dubious nor controversial.
    – user4894
    Apr 28, 2017 at 5:21
  • "no system can prove its own validity" is wrong. A system proves theorems; if inconsistent, it proves all and thus also false formulas. The conclsuion of G's Th is no "sufficiently strong" system can prove its own consistency. Apr 28, 2017 at 6:15
  • Maybe your (wrong) concern is due to the ambiguous use of "to prove". In a formal system, "to prove" means to formally derive from axioms; thus the 1-line long derivation of theorem A from axiom A is perfectly correct (but useless). But you are using "to prove" also to mean: establish the truth of a statement, and this is not the same as before: an inconsistent system proves all, and this does not mean that all formulae/statements are true (in some interpretation). Apr 28, 2017 at 7:43
  • Your second mistake is conflating prop logic with first-order one. x=x is the axiom for first-order equality, and x is an individual variable. = is not a prop connective, and we cannot use it with statements, like A. What we have is the "trivial proof" : (i) x=x : axiom. Again, it is a one-line derivation that is correct; and thus its conclusion: x=x, has been proved from the axioms. Apr 28, 2017 at 9:10

1 Answer 1


Yes, the axioms do trivially prove themselves. Your last derivation, however, is not valid: "A=A" can not be substituted for A because the latter is a symbol in a formal system, while the former is an object of it. You are free to postulate identity law as applied to symbols or laws, of course, in addition to just the identity law for objects, but that is a separate meta-law. I think OP's intuition might be of something like the universalist conception of logic that logicists envisioned, where everything has to be justified from within the system, and hence some axioms must be at the foundation and "unprovable". This, of course, is very different from the modern theory of formal systems, where (following Hilbert) meta-linguistic manipulations are "silently granted" without axiomatizing them in the system itself. If need be, a separate meta-language can be introduced for that purpose.

The confusion is understandable since, in Hilbertian terms, the universalist conception mixes the object language of the formal system with the meta-language used to talk about statements of that language, see semantic theory of truth. These were separated by Tarski exactly to avoid the paradoxes of self-reference, after Gödel's incompleteness results made the universalist logicism unattractive. Tarski proved that a formal first order theory that contains Peano arithmetic and is capable of expressing claims about the truth of its sentences, is necessarily inconsistent. This is his Undefinability of Truth theorem, and it might be the "one of the implications of Gödel" mentioned in the OP:

"This implies a major limitation on the scope of "self-representation." It is possible to define a formula True(n) whose extension is T but only by drawing on a metalanguage whose expressive power goes beyond that of L. For example, a truth predicate for first-order arithmetic can be defined in second-order arithmetic. However, this formula would only be able to define a truth predicate for sentences in the original language L. To define a truth predicate for the metalanguage would require a still higher "metametalanguage", and so on."

The requisite tower of meta-languages is known as the Tarski hierarchy. It is this hierarchy that prevents things like the Liar sentence "I am not true" from being formally expressible.

Now to another "implication of Gödel", Löb's theorem, which deriving A from A "can be shown to violate", according to the OP's earlier question. Of course, no such thing can be shown, but it does not help that Wikipedia's "formulation" of the Löb's theorem is highly misleading:

"in any formal system F with Peano arithmetic (PA), for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F".

It can not be "provable in F" that "if P is provable in F then P is true", because such a thing would require F to contain its own truth predicate, and hence be inconsistent by the Undefinability of Truth. SEP gives a precise formulation of the Löb's theorem, and explains why Wikipedia's "lame terms" version of it is, well, lame:

"In order to understand Löb's theorem properly it is useful to first consider the so-called “reflection principles”. Above, the focus has been on expressing, inside a formal system, that the system is consistent, i.e., on Cons(F). But naturally the theory should not merely be consistent but also sound, i.e., prove only true sentences. How should the soundness of a system, i.e., the claim that everything derivable in the system is true, be expressed? If one wants to express this in the language of the system itself, it cannot be done by a single statement saying this, because there is, by the undefinability of truth, no suitable truth predicate available in the language. Various restricted and unrestricted soundness claims can, however, be expressed in the form of a scheme, the so-called Reflection Principles...

Exactly which instances of the reflection scheme are actually provable in the system? Löb's Theorem gives a precise answer to this question (assuming that Prov_F(x) satisfies the derivability conditions). [...] the instances of soundness (reflection principle) provable in a system are exactly the ones which concern sentences which are themselves provable in the system."

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .