Compare the way the induction schema of arithmetic is represented by the single theorem num_INDUCTION.
Thanks, Rob! It's good to have a HOL Light example of an axiom schema. (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). Yes, I'm using the dialect of HOL Light defined by hol_light/RichterHilbertAxiomGeometry/readable.ml 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. Excellent! 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. Yes, you're indeed correct, and 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. Yes, that was the work I didn't know how to do. Since the main point of Tarski's axioms is to get a ``model based on algebraic reals that looks complete to first-order eyes,'' it sounds like a bad idea to use your ``much stronger axiom of continuity'' that gives us the reals. Tarski's first order continuity axiom is strong enough because it specifies the real-closed fields, and then we can use Tarski's big theorem http://en.wikipedia.org/wiki/Real_closed_field Alfred Tarski (1951) proved that [...] The theory of real closed fields is complete, o-minimal and decidable. -- Best, Bill ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
