[FOM] First Order Logic

[Joe Shipman]

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

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