Topics Logic

Question I have a question about existence withing a formal system. Can we construct it so that a theorem t implies "there exists" theorem t itself? Thanks, Paul

Accepted:
September 10, 2010

Comments

I'm not quite sure what the question is here, but here's what I think is meant: Can we construct a statement S such that S implies that S itself exists? If that is the question, then the answer is "Yes", assuming we have some fairly minimal syntactic resources (namely, those sufficient for the purposes of Gödel's theorem).

If we have those resources, then we know, by the so-called diagonal lemma, that, for any formula A(x) we can find a sentence G such that the following is provable:

A(*G*) <--> G

where *G* is itself a name of the sentence G. G itself will be fairly long, but is something that can actually be written down. So now let A(x) be the formula:

∃y(y = x)

I.e., this means "x exists". Then, by the diagonal lemma, we have a formula G such that we can prove:

∃y(y = *G*) <--> G

I.e.: G itself is provably equivalent to the statement that G exists.

We can in fact say more. If we have the syntax we need, then we can prove that G exists. Hence, we can prove G itself, too.

In fact, any such system will prove that all of the sentences within it exist, so in that sense it is very easy to construct systems that prove, not just for theorems but for all their sentences, that those sentences exist.

Question I have a question about existence withing a formal system. Can we construct it so that a theorem t implies "there exists" theorem t itself? Thanks, Paul Accepted:September 10, 2010

Question I have a question about existence withing a formal system. Can we construct it so that a theorem t implies "there exists" theorem t itself? Thanks, Paul

Accepted:
September 10, 2010