Re: [mizar] [Timothy Y. Chow] Re: [FOM] Formalization Thesis

[Jesse Alama <alama@stanford.edu>]

Freek Wiedijk <freek@cs.ru.nl> writes:

>>>Personally I always worry about the choice operator, which is
>>>implicitly present in Mizar.  I like foundations that don't
>>>have that, but then how do you translate your formal
>>>mathematics that implicitly is built on it?
>>
>>The Axioms of Choice is a theorem in TG.
>
> I wasn't talking about AC.  (Who would want to do mathematics
> without AC?)  I was talking about a choice _operator._  So
> a functor that given a non empty set gives you an element
> of that set.  In Mizar one can define such a functor (as
> you taught me):
>
>   environ
>    vocabularies NEWTON;
>    notations XBOOLE_0, SUBSET_1;
>    constructors TARSKI, SUBSET_1;
>    registrations XBOOLE_0;
>    requirements BOOLE, SUBSET;
>
>   begin
>    reserve X for non empty set;
>
>   definition
>    let X such that A1: contradiction;
>    func choose X -> Element of X means contradiction;
>    correctness by A1;
>   end;
>
>   theorem choose X in X;
>
> AC just states that there _exists_ a choice function,
> but a choice operator actually allows you to define one.
> That is much stronger.  (And too strong to my taste.)

I'm not sure if this is directly related, but you may be interested in
the epsilon calculus, a formulation of predicate logic due to Hilbert.
The characteristic feature of the logic are so-called epsilon terms

  e x A(x),

where x is a variable and A(x) is a formula.  (The "e" should be an
epsilon.)  The intended interpretation of e x A(x) is "an x such that
A(x)", so the axiom of choice is "built in" to the underlying logic. One
can then define the quantifiers as

  exists x A(x)  --->  A(e x A(x))

  all x A(x) ---> 
    not exists x not A(x) --->
    not not A(e x not A(x))  --->
    A(e x not A(x))

A proof system can be specified by adding as axioms all tautologies,
equality axioms, and two special "e-axioms"

  1. A(t) -> A(e x A(x))

  2. all x (A <-> B) -> (e x A) = (e x B).

A translation from predicate logic into the epsilon calculus is given by
the above procedure; one has |- A (in FOL) implies |- A' (in
e-calculus).  One of the highlights of e-calculus is the so-called
epsilon theorem, which states the reverse implication: if |- A (in
e-calculus) then |- A (in FOL).  Thus the epsilon calculus, based on a
choice operator, is no more stronger than predicate logic.

For more information, see 

  http://plato.stanford.edu/entries/epsilon-calculus/

Jesse

-- 
Jesse Alama (alama@stanford.edu)