[FOM] First Order Logic

Wed Sep 4 10:00:31 EDT 2013

On Mon, Sep 2, 2013 at 2:43 PM, 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,
>

Of course that is what you were referring to.  And you said

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.
>

I was pointing out that you commit a non sequitur since no one here had
called anything first order simply for that reason.  The versions of HOL
that people call first order do in historical and pedagogical fact inherit
their logic from first order logic.

You say

> 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.
>

When someone produces such a system, stronger than first order logic in
some useful credible way, I will be interested to see it.

Colin

>
> -- 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/766bfa3c/attachment-0001.html>