[FOM] First Order Logic

Wed Sep 4 15:00:52 EDT 2013

Joe,

Could you help clarify a bit further your criteria for a suitable HOL?

In particular, you are looking for something more than "simply many-sorted
FOL in disguise". Are you looking for something more than "FOL plus a
useful fraction of set theory in disguise"? It has seemed to me that a more
common criticism of HOL has been that it "sneaks in set theory" rather than
"sneaking in sorts" (though some versions of HOL do include concepts much
like sorts).

FOL + ZFC can prove more than the HOL systems I have heard of except
perhaps Girard's System F or extensions of it as used in the HOL-Omega
theorem prover (as in http://www.trustworthytools.com/holw/holw-lncs5674.pdf
).

Aside from that, I think proponents of HOL logics often consider them more
powerful than FOL in practical ways, by providing a language closer than
FOL to the language they use intuitively through variables that range over
sets, relations, and functions; and by reducing some of the implicit
reasoning about existence that is implied by FOL plus ZFC. But I am not
sure this is of interest to you.

Regards,
Cris

On Mon, Sep 2, 2013 at 11:43 AM, Joe Shipman <JoeShipman at aol.com> wrote:

> Yes, but I was specifically referring to a proof system which, while
> effective, is neither complete nor inherited from first-order logic, and
> whose soundness is a meta-theoretical question that I don't need to address
> until I give a semantics. Such a system is what I desire to do mathematics,
> rather than metamathematics, and I am willing to argue informally for the
> soundness of the axioms and inference rules of such a proof system if
> appropriate.
>
> I don't want to create a system that the logicians will be able to prove
> nice things about, I just want to formalize mathematics in HOL using the
> most powerful deductive calculus for HOL that I can informally justify. So
> FOL need not come into it at all, unless nobody is able to offer me a
> deductive calculus that isn't simply many-sorted FOL in disguise.
>
> -- JS
>
> Sent from my iPhone
>
> On Aug 31, 2013, at 10:29 AM, Colin McLarty <colin.mclarty at case.edu>
> wrote:
>
>
> I don't see why you need to call such a thing "first order" simply because
>> you have rules for enumerating valid sentences and deductions.
>>
>
> On the other hand when a system has  "a complete, sound, effective proof
> system inherited from first-order logic" then you do have reason to call it
> first order logic.  That quote is not my phrase.  It is copied from
> Wikipedia.  The thought can be found in many places (including Harvey's
> posts in this thread also cited by Dustin Wehr) and it is correct.
>
> best, Colin
>
>
>
>> -- JS
>>
>> Sent from my iPhone
>>
>> On Aug 27, 2013, at 6:00 PM, Colin McLarty <colin.mclarty at case.edu>
>> wrote:
>>
>>
>>
>> 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
>> purposes.
>>
>> 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
>> boolean.
>>
>> best, Colin
>>
>>
>>
>>
>> >
>> >
>>>
>>>
>>>> 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
>>>>> arithmetic
>>>>> 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.
>>>>>
>>>>> Best,
>>>>>
>>>>> Sam
>>>>>
>>>>>
>>>> _______________________________________________
>>>> FOM mailing list
>>>> FOM at cs.nyu.edu
>>>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>>>
>>>>
>>>
>>> _______________________________________________
>>> FOM mailing list
>>> FOM at cs.nyu.edu
>>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>>
>>>
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>
>>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
> _______________________________________________
> 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/20130904/ad985408/attachment-0001.html>