Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9404121930.AA18742@maui.cs.ucla.edu>
To: schneide <schneide@ira.uka.de>
Subject: Re: number theory
Cc: info-hol@cs.uidaho.edu
Date: Tue, 12 Apr 94 12:30:51 PDT
From: chou@cs.ucla.edu


% In order to pick up another issue, I want to add a piece of discussion
% with M.Kaufmann. He wrote:
% 
% |> But perhaps instead you are imagining two-sorted models of arithmetic, where
% |> one sort ("type") contains the numbers and the other contains the "classes"
% |> (sets of numbers), and the universal class quantifier ranges over those classes
% |> in the model rather than over all classes.  Then you can stay in the realm of
% |> first-order logic.  But in that case, once again the axioms do not characterize
% |> the standard model.  One can obtain models of this version of PA in which the
% |> number part is non-standard, and the class part is (necesssarily) a proper
% |> subset of the power set of the number part -- in fact, there are such models
% |> (by the Lowenheim-Skolem theorem) in which the class part is countable.
% 
% So, one has always to be careful when working with higher order theories.
% I think there is a real problem if objects of the real world are to be modelled,
% i.e. is my special HOL-theory really a model of my considered piece of world?

You might be interested in the following "paradox", discovered by Skolem.
Consider the usual first-order formulation of set theory, say ZF.
Within the theory you can prove, using Cantor's argument, that there are
uncountable sets.  However, since the language of ZF is countable,
Lowenheim-Skolem Theorem says that ZF must have a countable model, in
which the power set of the set of natural numbers is countable!
Of course, this isn't really a "paradox", because what Cantor's argument
really proves is that there is no bijection between the set of natural
numbers and its power set, which is true for all models of ZF including
any non-standard model.

The sad fact of life is this.  On the one hand, first-order logic is not
as expressive as we would like it to be, as first-order formulations of
most interesting things have non-standard models.  On the other hand,
"true" second-order logic is too powerful, as it can't have a complete
deductive system.  By "true" second-order logic I mean that the domain
of second-order variables must be the whole of the power set of the
domain of the first-order variables, so things like Skolem's paradox
cannot arise.

Cheers,
- Ching Tsun