[FOM] First Order Logic
colin.mclarty at case.edu
Tue Aug 27 18:00:39 EDT 2013
On Tue, Aug 27, 2013 at 12:01 PM, Cris Perdue <cris at perdues.com> wrote
meaning to disagree with Friedman's claims for first order logic, and mine
so far as I agreed with Friedman:
> Proofs in type theory (e.g. simple type theory) are also "definite finite
> objects that can be objectively tested for correctness"; and speaking of
> software proof assistants, type theory / higher-order logic has strong
> communities that formalize mathematics in type theory.
There is some confusion here though. Simple type theory is a multi-sorted
first order logic. The term HOL is ambiguous. Sometimes it is meant to
have "semantics more expressive than first-order logic." That version
cannot be axiomatized and I don't see how you would even try to take it as
a foundation in the strict sense, since you cannot identify correct
reasoning in it. Sometimes HOL is taken "with Henkin semantics and a
complete, sound, effective proof system inherited from first-order logic."
That version where proofs can be tested for correctness is a multi-sorted
first order logic.
Many of the more intricate logics are not meant to be formal foundations
for mathematics. Their very description relies on previous mathematics.
And this is fine for many purposes.
Clear disagreement only comes about if you take foundations in the strict
sense of axioms in a formal logical system which defines correct inference,
and then want such a foundation with some logic essentially different from
classical first order.
Too often that issue gets confused with discussion over whether one wants
foundations in that sense -- and that discussion is too often confused by
failure to distinguish between different things one wants for different
As to axioms in a formal logical system which defines correct inference for
mathematics, i agree with Harvey that logic has to be classical first
order. Multi-sorted counts as classical for me, but classical does mean
>> 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.
>> Harvey Friedman
>> On Sun, Aug 25, 2013 at 11:56 AM, Sam Sanders <sasander at cage.ugent.be>wrote:
>>> Dear Carl,
>>> > Not everyone has been on same old conventional page as Tarski. For
>>> example, [Barwise 1985] critiqued the first-order thesis as follows:
>>> > "The reasons for the widespread, often uncritical acceptance of the
>>> first-order thesis are numerous. Partly it grew out of interest in and
>>> hopes for Hilbert's program. ... The first-order thesis ... confuses the
>>> subject matter of logic with one its tools. First-order language is just an
>>> artificial language structured to help investigate logic, much as a
>>> telescope is a tool constructed to help study heavenly bodies. From the
>>> perspective of the mathematics in the street, the first-order thesis is
>>> like the claim that astronomy is the study of the telescope."
>>> I believe I did not mention the "first-order thesis", but let me make it
>>> clear that I believe that (at the very least) we need second-order
>>> to formalize mathematics. Reverse Mathematics is a good example, though
>>> heavy on the coding sometimes; Classical logic is used there.
>>> > In particular, Computer Science has requirements that go far beyond
>>> classical first-order logic. The domination of classical logic is coming to
>>> an end because practical real-world theories are pervasively inconsistent.
>>> > Computer Science needs Inconsistency Robust mathematical foundations
>>> with the following characteristics:
>>> > * Standard Boolean equivalences hold for conjunction, disjunction,
>>> and negation
>>> > * Disjunctive Syllogism holds as well
>>> > * Capability to reason about arguments for and against propositions
>>> > Consequently, the range of acceptable CS solutions for Inconsistency
>>> Robust inference is actually quite narrow :-)
>>> Do people in applications really throw out classical (whatever order)
>>> logic and embrace paraconsistent logic as "the true way"? Or do they just
>>> think/work classically and somehow
>>> manage to contain the inconsistent information, i.e. prevent it from
>>> doing damage?
>>> I have seen examples of the latter, but not the former in practice.
>>> Chow similarly asked for a clear example (related to the ongoing saga
>>> mentioned), I believe.
>> FOM mailing list
>> FOM at cs.nyu.edu
> FOM mailing list
> FOM at cs.nyu.edu
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM