[FOM] First Order Logic

Joe Shipman JoeShipman at aol.com
Mon Sep 2 14:43:03 EDT 2013 

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

More information about the FOM mailing list