[FOM] First Order Logic

[MartDowd at aol.com]

Arnon,
 
First-order logic is a formalized version of predicate logic.
This is a  semi-formal study of deductive principles, applicable more
generally than to  mathematical logic.  The study of predicate logic
was already in a  mature form in Aristotle's writings; see for example
http://www.britannica.com/EBchecked/topic/346217/history-of-logic/65921/Cate
gorical-forms
http://hume.ucdavis.edu/mattey/phi112/history.html
 
>From a modern perspective, predicate logic has individual variables,
and  predicates (ignoring functions for simplicity).  In first order
logic,  predicates are constants; they may be taken as
implicitly universally quantified.  In second
order logic, formulas  may include explicit quantifiers over predicates.
In modern axiom systems for  the first order validities (equivalently,
the second order validities with no  predicate quantifiers),
modes ponense may be taken as the only rule (see  Enderton's
logic book).  This may be seen to hold for full second order  logic
(where predicates range over relations on the universe of  discourse)
as well.  Indeed, the second order validities plus modes  ponens are
readily seen to be implicationally complete (for  implicational
completeness see
_www.andrew.cmu.edu/user/avigad/Papers/hardtaut.pdf_ 
(http://www.andrew.cmu.edu/user/avigad/Papers/hardtaut.pdf) 

The above certainly holds for various other semantics for
second order  logic.  In short, modes ponens reduces the problem of
deductive  reasoning to that of enumerating a set of validities.
In this sense, first  order logic is "the best you can do".
 
There is an analogous situation in propositional logic,
where even  though the tautologies are recursively enumerable,
one frequently gives a  polynomial time decidable set of axioms.
 
- Martin Dowd



In a message dated 9/7/2013 7:28:43 A.M. Pacific Daylight Time,  
aa at tau.ac.il writes:

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

_______________________________________________
FOM mailing  list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130907/fbf9a183/attachment-0001.html>