Foundations of mathematics has stopped making progress.
It started making progress a century ago, but stalled due to lack of constructive dialogue, that was replaced by
rebuttal, refusal and denial. Counter arguments became largely accepted,
and the foundation of mathematics hasn't changed ever since.
Even worse, those counter argumentation, as they were identified during early days of foundations
of mathematics, are now, a century later, turned into standard arguments and legacies, placed on piedestals
for everyone to repsect and never by-pass. Arguments from those days, which were targeted by counter arguments,
are surpressed and basically forgotten.
Looking at the very fons-et-origo of foundations,
it really shouldn't make sufficient sense to create foundations based on putting arbitrary symbols side by side,
and using natural language to define which sequences of symbols to accept and which not.
Since such syntactics couldn't be driven but small steps forward,
the urge to assign meaning took over, and soon semantics controls syntax. Consequences of circular thinking was recognized,
but at the same time seen as unavoidable once handled with sufficient care.
The Liar, composing outside in self-predication, was no longer seen as a producing bad themes,
and even worse, the Liar soon became fugued as a pillar of all foundations.
Novel, yet historical, foundations is based on syntax being before semantics, and the existential symbol
definitely not being an operator.
In fact, it's not even a symbol. It's an informal one.
A predicate 
is not a symbol,
but an operator symbol. This involves typing and arity. The foundations of typing is yet to be developed.
We can't put characters side by side forever, can we? Let's start with the quantifier.
An existential quantifier does not read "there exists" but
"there exists such that". So a quantifier is in fact indexed by the operator symbol that underlies the expression it quantifies,
even if that index is deliberately hidden. A quantifier "binds", but that binding is not well defined.
In fact, it is not defined at all.
There cannot be anything like an general existential quantifier, a general symbol to be freely used
in "sequences of symbols like"
)
and
))
.
Allowing the quantifier symbol to appear broadly in this way enables the Liar to enter the scene, and things become ugly.
It's time to call the Liar for what he or she actually is, namely, a Liar,
and start to rebuild the foundations of mathematics now over a forthcoming century with "the second incompleteness theorem" being a Paradox, not a Theorem.
A solution will probably solve "the computability problem" simply in a corollary.
Let us join forces to build community in support of novel yet historical Foundations of Mathematics!
You are invited to express your interest to join the discussions.
Contact:
Patrik Eklund