[FOM] First Order Logic
MartDowd at aol.com
MartDowd at aol.com
Sat Sep 7 16:28:22 EDT 2013
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
>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
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
> 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
(with contributions of others) that started within a thread that was
"First-order arithmetical truth", and continued with various postings
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
> 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.
FOM mailing list
FOM at cs.nyu.edu
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM