[FOM] Why not this theory be the foundational theory of mathematics?
Patrik Eklund
peklund at cs.umu.se
Fri Mar 29 03:42:15 EDT 2019
Thanks, Colin, for raising that question. You may have seen my posting
by know, where I also raise that question, and try to provide some lines
of insight.
My main objection to foundations is indeed that sentences/formulas are
"constructed" too freely. I cannot see something like Ex.Proof(Q(x)) as
a formula of the same "type" as e.g. the formula Ex.Q(x), simply because
we have to define 'Proof' AFTER we already fixed all those Qs.
I've often said we have to "close the door" to forming sentences, and
this closing must be done BEFORE we can define machineries like proof
ruling about those sentences. This is what we have tried to explain as
the "lativity" of logic (www.glioc.com).
Categorically it is also clear how term functors (also in a many-sorted
way, which is non-trivial!) can be extended to monads so as to enable
substitutions (a la Kleisli), but sentence functors are not extendable
to monads. Otherwise sentences are terms (which happens in some special
cases like in lambda calculus, and in propositional calculus, of
course).
So when Church mentions the o type in his 1940 paper, I cannot see how
'Q' and 'Proof' generate formulas of the "same type". Q(x) is a term,
Ex.Q(x) is a sentence maybe in the style of complying with Church's o
type, but Ex.Proof(Q(x)) is different. I have difficult to accept that
"E" in "Ex.Q(x)" is the same symbol as the "E" in "Ex.Proof(Q(x))".
Artemov's justification "types" are similar and in my view related more
to Church's o than to his iota. However, as there are type constructors
on the iota side, there are no similar type constructors on the o side.
Artemov allows a certain algebraic manipulation of justification types,
but that magma operator for combining justification types is not
syntactically constructed. It is only semantically explained.
Maybe the main problem of foundations is indeed that syntax is ALWAYS
justified ONLY by semantics, because "syntax" in Foundation is
"constructive" only in the sense of putting characters one by one
side-by-side (the "supermagna") by certain "rules" presented in natural
language and "fully justified" only by semantics.
So in this view there is basically no constructive syntax, because
semantics comes FIRST, and semantics justifies syntax. Category theory
enables purely syntactic constructions. The solution is not complete,
but there are constructions that look pretty promising, I would like to
say.
Logic and math doesn't break down because of my view, but the Liar
business breaks down. The Liar technique is quite "illative". GdM II
says the same thing, maybe in other words, but indeed says the same
thing.
Best,
Patrik
On 2019-03-28 02:00, Colin McLarty wrote:
> I am curious to know what this means:
>
> On Wed, Mar 27, 2019 at 7:55 PM Thomas Klimpel
> <jacques.gentzen at gmail.com> wrote
>
>> (The category of all sets is
>> specified by a sort of "last word quantification", but this is
>> troublesome for a foundational theory. A foundational theory should
>> lay down the first words, not insist on having the last word.)
>
> Colin
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
More information about the FOM
mailing list