deimors said:
The problem appears to be that, for any language sufficient enough to describe all the propositions we'd want to create, there does not exist a set of axioms which could prove every proposition (Gödel's incompleteness theorem).
What about an inconsistent set of axioms? The set of all propositions is a set of axioms, so there you have it already, though a set of axioms technically does not prove anything, as axioms are just propositions. You need inference rules in order to prove anything.
Why would you want to be able to prove every proposition anyway? It seems to me that the whole point of studying logics and reasoning systems is to partition your set of propositions in some way, e.g., into ones that are true and ones that are false or into ones that are logically connected to some given set and ones that are not.
The "problem" with your expression doesn't seem to necessarily have anything to do with numbers or well-orderings. The problem seems to me to be that your expression is talking about its own interpretation and you identify a singleton referent with its own member.
Say that you have a set
E of nominal expressions (a certain type of string of some formal language), a set
O of objects (objects not necessarily being atomic individuals but possibly sets), and a map
I from
E to the power set of
O,
Power(O). Doesn't
1) the
o in
O that
I does not assign as the value of this expression
present the same problem as your original expression, only more directly? Under some
I, e.g., the standard English one,
Ien, (1) is making a claim about its own interpretation. Under
Ien, (1) is putting a condition on
Ien, a condition that
Ien cannot satisfy, and this seems to me to be the problem with your original expression.
Perhaps even more straightforward is
2) any
o in
O that
I does not assign as the value of any
e in
E
The referent of (2) is the set of all objects that aren't referents. So (2) seems to require, where
I(e) denotes the set assigned to
e by
I (i.e., a referent and member of
Power(O)) and
f is in
E,
3) \exists I \exists f \forall e \forall o \ [o \in I(f) \ \leftrightarrow \ \neg(o = I(e))]
If you let
I(f) be a member of
O, then, when
o = I(f) and
e = f, (3) becomes
4) \exists I \exists f \ [I(f) \in I(f) \ \leftrightarrow \neg(I(f) = I(f))
If you further identify singletons with their member (so that
p is a singleton and q is in p implies
p = q) and assume that
I(f) is a singleton (changing (2) to
the o in O...), then (4) becomes
5) \exists I \exists f \ [I(f) = I(f) \ \leftrightarrow \neg(I(f) = I(f))]
Hm, right? Does anyone see a mistake?