[FOM] Why not this theory be the foundational theory of mathematics?

[Patrik Eklund]

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