[FOM] First Order Logic

[Arnon Avron]

On Sun, Aug 25, 2013 at 03:59:02PM -0400, Harvey Friedman wrote:
> 
> Furthermore, first order logic is apparently the unique vehicle for such
> foundational purposes. (I'm not talking about arbitrary interesting
> foundational purposes). However, we still do not know quite how to
> formulate this properly in order to establish that first order logic is in
> fact the unique vehicle for such foundational purposes.

Very similar declarations have been made by Harvey about 7 years ago.
Thus in his posting on Tue Oct 24 22:00:59 EDT 2006 
(http://www.cs.nyu.edu/pipermail/fom/2006-October/011020.html) he wrote:

"FOL (through its practically driven variants) is the only appropriate
vehicle for the foundations of mathematics. I doubt if many people would
disagree with this. The only issue is how to go about carefully formulating
just what this means."

 Obviously, no much progress has been made on this front in the last 
7 years. Anyway, this statement was made as a part of an exchange between us
(with contributions of others) that started within a thread that was called 
"First-order arithmetical truth", and continued with various postings under 
the titles: "Are first-order languages adequate for mathematics?", 
"First Order Logic/status", and "Concerning Ancestral Logic". I do not
have much to add to the arguments I made in this exchange 7 years ago
(and neither does Harvey, or so it seems to me). So I do not
see much point in repeating what I wrote then in several postings.
I'll just repeat the words  started that debate (in my posting from Fri 
Oct 20 19:32:16 EDT 2006): 

"For many years I maintain that the appropriate language
for formalizing logic and mathematics is neither the first-order 
language nor the second-order one. The first is too weak for 
expressing what we all understand, the second involves too strong 
ontological commitments. The adequate language
is something  in the middle: what is called "ancestral logic"
in Shapiro's book "Foundations without Foundationalism". This logic 
is equivalent to weak second-order logic (as is shown
in Shapiro's book, as well as in  his chapter in Vol. 1 of the 
2nd ed. of the Handbook of Philosophical logic). However, I prefer 
the "ancestral logic" version, because the notion of "ancestor" 
is part of everybody's logic, 100% understood also by 
non-mathematicians." 



> In summary, whereas it can be interesting and important to give second
> order formulations of various theories, ultimately in each case you are
> compelled to provide a clarifying first order associate.

So again: the right choice is neither first-order logic
nor higher-order logic, but something in the middle: ancestral
logic. This logic is in fact 
absolutely necessary even to define what first-order logic
is, because all the basic notions of first-order logic,
like formulas and formal proofs, are defined inductively.

Arnon Avron