Hi, just a quick comment before this becomes into some HOL vs FOL issue: (conservative) extension by definitions (http://en.wikipedia.org/wiki/Extension_by_definitions) is a standard FOL method that used very often (e.g., when building up math in ZFC). I believe standard logic textbooks (like Mendelson) discuss this early.
Best, Josef On Fri, Sep 7, 2012 at 5:54 AM, Gottfried Barrow <[email protected]> wrote: > On 9/4/2012 1:53 AM, Ramana Kumar wrote: > > THIS IS FROM: Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light > >> >> I don't understand the question. You know more than I do about types & >> constants in HOL than I do, and I think these don't exist in FOL. I tried >> to explain that much of the ZC/FOL axioms (power set, products...) are >> encoded in the HOL type system (->, prod/#). > > > > Constants do exist in FOL: they are called function/relation and predicate > symbols. In ZC/FOL you have constants like set-membership and equality (both > relations). But you can be more or less formal about how you define new > constants. In HOL, since we actually define things like the logical > connectives and quantifiers (and,or,not,forall,etc.) rather than having them > built into the syntax, we have principles of definition. > > > Ramana, > > I haven't been paying attention completely, so I don't know if the FOL > constants you're talking about are the same constants I'll be asking about. > > I'm interested in FOL constants because I'm trying to answer the question of > whether ZF sets, as a FOL language, justifies statements like this: > > (Classic Set Theory, by Derek Goldrei, page 71) > Before we give axioms for set theory, we must specify the framework > within which these axioms sit. > That is the aim of this section. We shall write the axioms using a very > limited language, one that fits > a formal logical treatment using the predicate calculus. For the purposes > of this book, it is important > to be able to use and interpret the formal language, but not to construct > formal proofs using it. > > It is, however, important to realize that such formal proofs can in > principle be given. (emphasis mine) > > So supposedly, we can translate any proof into the formal, first-order > language of ZF sets as originally specified, that is, by not substituting an > enhanced FOL language in its place. > > As I'm seeing it, ZF sets gives us no ability to define constants and > notation, and so it must be supplemented as a language, or it must be > replaced by another language of FOL. > > For example, how do I name the empty set using only the FOL symbols that ZF > sets has been specified to have? > > That's my basic question. Whether that can or can't be done answers my > bigger question. > > For reference, I'm using "A Problem Course in Mathematical Logic" by > Bilaniuk. Unlike him, I assume all the standard logical symbols. > http://euclid.trentu.ca/math/sb/pcml/pcml.html > Definition 5.1: Symbols (page 24) > Definition 5.2: Terms (page 26) > Definition 5.3: Formulas (page 27) > > I can see that theorems and axioms can be stated for ZF sets with FOL > formulas. > > However, please consider the empty set. It is described by a formula: > > \<exists> x \<forall> y ~(y IN x) . > > For ZF sets we have the following available: > > Definition 5.1 > LOGICAL SYMBOLS: (, ), ~, -->, \<exists>, \<forall>, an infinite number > of variables, =. > NON-LOGICAL SYMBOLS: membership predicate, no constants, no functions. > > Definition 5.2: > TERMS: the only terms are the variables. > > Definition 5.3: FORMULAS > (1) If x and y are variables, then (x IN y) is a formula. > (2) If x and y are variables, then x = y is a formula. > (3) If phi is a formula then (~phi) is a formula. > (4) If alpha and beta are formulas, the (alpha --> beta) is a > formula. > (5) If phi is a formula and x is a variable, then (\<forall>x. phi) > is a formula. > (6) Nothing else is a formula. > > Okay, so I assume the other formulas from the other standard logical > connectives, and I paraphrased some of the sentences, because the only terms > are variables. > > So maybe you can tell me how to define a constant for the empty set, so we > can use it on the LHS or RHS side of the two predicates, membership and > equal. > > The empty set is inseparable from the universal quantifer. You can't use a > FOL formula on the LHS or RHS of the membership predicate. > > My answer to my question is that what's being done is a new FOL language for > ZF sets is replacing the previous FOL language every time a new set constant > is introduced. > > After all, in the FOL specification, a FOL language can have as many > constants as it wants, and I'm thinking that typical set builder notation is > a string of characters that qualifies for item (6) in Definition 5.1: > > (6) A (possibly empty) set of constant symbols. > > If you can help answer my question, please do. > > Regards, > GB > > > > > ------------------------------------------------------------------------------ > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
