On 15 Nov 2014, at 08:25, Bill Richter <[email protected]> wrote:
> Does anyone know how to formalize an axiom schema in HOL Light? I'm
> interested in formalizing the Tarski axiomatic geometry
> Axiom schema of Continuity
> http://en.wikipedia.org/wiki/Tarski%27s_axioms#The_axioms
> and the part I don't know how to handle involves the universal quantification
>
> Let φ(x) and ψ(y) be first-order formulae containing no free instances of
> either a or b
>
The easy way out is to represent the first-order formulas as boolean-valued
functions.
Then you get a single HOL axiom that represents the entire axiom schema. Thus,
with p and
q for φ and ψ, it would look like:
!p. !q. (?a. !x. !y. p x /\ q y ==> B a x y) ==> (?b. !x. !y. p x /\ q y
==> B x b y)
Compare the way the induction schema of arithmetic is represented by the single
theorem
num_INDUCTION. (By the way I am assuming you are still working in HOL Light,
though
I don’t recognise some of the functions you are using, like NewAxiom).
Note that that the stipulation that the formulas contain no free instances of a
or b
comes for free: the bound variables a and b will get renamed if necessary when
you instantiate p and q.
This approach is the natural thing to do in HOL, but it typically gives
something that
is much stronger than the corresponding first-order schema. E.g., I expect
you’d be able
to use the axiom of continuity to construct the reals and prove they are
complete, whereas
I would expect Tarski’s axiomatic geometry to have a model based on algebraic
reals that looks
complete to first-order eyes, but can be seen not to be complete if you can
quantify
over arbitrary sets of points.
If, for some reason, you need the first-order restriction, then you have a lot
more
work to do: you would have to build a representation of the syntax of the
first-order language and restrict the continuity axiom to properties that are
expressed
in that language.
Regards,
Rob.
------------------------------------------------------------------------------
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://pubads.g.doubleclick.net/gampad/clk?id=154624111&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
