[FOM] First Order Logic

[Carl Mummert]

On Mon, Sep 2, 2013 at 2:43 PM, Joe Shipman <JoeShipman at aol.com> wrote:
> 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.

Won't it be the case that *every* deductive system of a very general
nature is merely many-sorted FOL in disguise? Suppose the formal
language in which we are working has very basic similarities to the
usual language of type theory. Then, given any deductive calculus, I
can interpret it via an analogue of Henkin semantics, and if I choose
the set of Henkin models correctly I will obtain a soundness and
completeness theorem for that set of deduction rules.  The key point
is that, after an arbitrary deductive system is fixed, the semantics
can be adjusted freely until a completeness result is obtained.  The
proof system might even be ineffective.

The argument above is necessarily heuristic, because of the
flexibility with the formal language, but specific cases go through
perfectly well. For example, the strongest deductive system normally
considered for second order logic has the usual deductive rules of
predicate logic along with the full comprehension scheme and a scheme
for the axiom of choice (e.g. section 3.2 of Shapiro's *Foundations
without Foundationalism*). There is a standard soundness and
completness theorem for that deductive system in Henkin semantics.

I would be interested in an example where this method cannot be used.

Best regards,

Carl