[FOM] First Order Logic

Sat Aug 31 10:29:55 EDT 2013

On Fri, Aug 30, 2013 at 3:10 PM, Joe Shipman <JoeShipman at aol.com> wrote:

Ok then, what is the most powerful deductive calculus for HOL that is ever
> used, which doesn't necessarily involve a choice of semantics at all and is
> not claiming completeness?
>

Good question.  I await any non-trivial answer that may come

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130831/c8dd61e1/attachment-0001.html>