[FOM] First Order Logic

[Christopher Menzel]

On Aug 27, 2013, at 5: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.

Not that it affects Colin's important point here, but "simple type theory" admits of the same ambiguity as "HOL". Notably, in his well-known text An Intro to Mathematical Logic and Type Theory, Andrews distinguishes between "standard" and "general" models of type theory (only the latter, of course, admitting of a sound, complete, and effective proof theory). Likewise the entry on Church's (simple) type theory in the SEP.

Chris Menzel

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130830/229b92fa/attachment-0001.html>