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 Tarski first order language is quite simple, and is explained below in a code fragment of hol_light/RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml which John essentially wrote for me years ago. But if someone had formalized an axiom schema for a different first order language that's surely good enough for me. Michael Beeson tells me that this is not necessary, as we can instead just adopt every axiom-instance of the axiom schema that we actually use. Do folks have an opinion on that? I'd like to install HOL Light on a Mac that's not connected to the net, and I'm intimidated by OPAM: http://caml.inria.fr/ocaml/release.en.html#idp1286576 Is there an earlier version of OCaml/Camlp for which inria distribute MacOS binaries that folks trust for building HOL Light? -- Best, Bill NewConstant("≃",`:TarskiPlane#TarskiPlane->TarskiPlane#TarskiPlane->bool`);; NewConstant("ℬ", `:TarskiPlane->TarskiPlane->TarskiPlane->bool`);; ParseAsInfix("≃",(12, "right"));; let A1 = NewAxiom `; ∀a b. a,b ≃ b,a`;; let A2 = NewAxiom `; ∀a b p q r s. a,b ≃ p,q ∧ a,b ≃ r,s ⇒ p,q ≃ r,s`;; let A3 = NewAxiom `; ∀a b c. a,b ≃ c,c ⇒ a = b`;; let A4 = NewAxiom `; ∀a q b c. ∃x. ℬ q a x ∧ a,x ≃ b,c`;; let A5 = NewAxiom `; ∀a b c x a' b' c' x'. ¬(a = b) ∧ a,b,c ≊ a',b',c' ∧ ℬ a b x ∧ ℬ a' b' x' ∧ b,x ≃ b',x' ⇒ c,x ≃ c',x'`;; let A6 = NewAxiom `; ∀a b. ℬ a b a ⇒ a = b`;; let A7 = NewAxiom `; ∀a b p q z. ℬ a p z ∧ ℬ b q z ⇒ ∃x. ℬ p x b ∧ ℬ q x a`;; ------------------------------------------------------------------------------ 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
