The best way of writing FOL with identity and membership.
in [Logic]
|
From: zuhair on 7 May 2010 04:50 Logical connectives: Negation ~ Disjunction | Implication > Conjunction juxtapositioning of the formulae. Example: QP stands for: Q and P Biconditional <> Quntifiers Existential quantifier _ _x stands for "there exist x" Unique existential quantifier ! !x stands for "there exist unique x" Universal quantifier no symbol just mention the quantified variable on the left of the formula with space in between x Q(x) is read as for all x Q(x). x _y stands for "for all x, there exist y". x _y Q(x,y) is read as: for all x there exist y such that Q(x,y). Primitives: Membership no symbol, just juxtapositioning the variables so xy stands for "x is a member of y" Identity = Functions: same as traditional f(x0,...,xn) and f:A -> B standing for f is a function having A as its domain, and B as its co-domain. Ordered pair: ( , ) Constants are zero-arity function symbols, usually written using upper case letters. Predicates: same as traditional Q(x0,...,xn) Set builder: same as traditional {:} or {|}. Strings of variables: x0,...,xn examples: used in n-arity functions and predicates, and also in quantification: _x0,...,xn Q refers to Exist x0,..., Exist xn such that Q while x0,...,xn Q stands for: for all x0,...,for all xn such that Q so when we have multiple quantification of the same type (i.e. existential versus universal), then it is sufficient to write the string of the variables quantified preceded by the quantifier which is _ in case of existential quantification or (no symbol) in case of universal quantification. Now _x0 x1,...,xn refers to Exist x0, for all x1,...,for all xn while x0 _x1,...,xn refers to For all x0, exist x1,....,exist xn notice the space between x0 and x1, since there is a change in the type of quantification from existential to universal. So the rule is: if we have a change in type of quantification then a space must be left to demarcate that change, as shown in the above examples. THE FOUR RULES OF ABBREVIATION: RULE 1: Rule of minimal required notation for unique interpret-ability: "A formula must have only ONE interpretation, with the minimal amount of symbols to achieve that". RULE 2: Rule of dot notation: A dot notation is only to be placed on the left of a connective. we have different powers of dot notations:- .. is a unit power dot notation : is a double power dot notation :. is a triple power dot notation :: is a quadruple power dot notation ::. is a five unit power dot notation and so on, the power of a dot notation is the number of dots in it. "The less is the power of the dot notation placed on the left of a connective, the earlier this connective is processed". So first connectives to be processed in a formula are those having no dot notation on the left of them, then those having unit power dot notations, then double power, then triple, till the maximal power dot notation in the formula. Examples: P|Q.|Q:>D.S<>K this would be ( (P|Q) | Q ) > (D and (S<>K)) so instead of 8 brackets, we only have three dot notations. Another example: P|Q:.|Q:>D.S<>K this would be (P|Q) | (Q>(D and (S<>K))) so 8 brackets are reduced to 4 dot notations. so smaller dot notations replace inner brackets, while higher ones replace outer brackets. RULE 3: Rule of Hidden quantifiers: "Quantifiers are hidden if their appearance would be consecutive otherwise; or in case of universal quantification the details of which is totally decidable without their appearance". Example: Exist x For all y ( y e x iff Q ) this is written as _x y yx<>Q however we see that y is appearing consecutively, so it is better to hide the first y so this can be written as _x yx<>Q Example: zx<>zy>y=x this is: for all x for all y ( for all z (zex <->zey) -> x=y ). Note: hiding quantifiers is optional, so writing all hidden quantifiers is not a violation of Rule-1. RULE 4: Exhaustive quantification: Sub-rule A: "All occurrences of a variable in a formula are either free in that formula or bound in that formula by the same quantifier". So we cannot have a formula like _yx > _yx _cy cx because y is quantified twice. so we need to choose another variable instead of a second y like _yx > _zx _cz cx which is axiom of foundation. According to rule 4_sub-rule A we cannot have the same variable being bound and free, or bound by two different quantifiers. Sub-rule B: "The scope of quantification of a variable z would end immediately after the last formula in which z or a variable that is visually recursively known to be within the scope of quantification of z, appears in". Knowledge by Visual Recursion: In first order logic the scope of quantification over a variable x having its first appearance (i.e. in the quantification statement like Exist x, or for all x, i.e. the quantificational appearance of x) within the scope of quantification of say variable y, then the scope of quantification over y extends over the whole of the scope of quantification over x. Now using rule 4_sub-rule A, if x first appearance is before an occurrence of the variable y and after the first appearance (i.e. the quantificational appearance) of y, then x lies within the scope of quantification of y, thus according to the above the scope of quantification over x would be a sub-scope of the scope of quantification over y. Now if a variable u having its first appearance before an occurrence of x but after the first appearance of x then u lies within the scope of quantification over x, and thus u would lie within the scope of quantification over y. We say that x and u above are *visually recursively* known to be within the scope of quantification of y. A general definition of visual recursion, would be the following: we say that x is visually recursively known to be within the scope of quantification of y iff (1)the first appearance of x is between the first appearance of y and an occurrence of y. or (2) the first appearance of x is between the first appearance of z and an occurrence of z , were z is visually recursively known to be within the scope of quantification of y. / definition finished. Since all formulas are finite in FOL(=,membership) then this recursive process would come to an end, so it can be used. Now according to this method, the scope of quantification of a variable y would end immediately after the last formula in which y or a variable that is visually recursively known to be within the scope of quantification of y, appears in. Now if this is not the case, then we need to write the formula y=y were y is the quantified variable who's scope of quantification is not decidable using the above method of visual recursion *alone*, or we can use the semi-colon to mark such undecidable scope of quantification. If the scope of quantification of a variable is decidable by visual recursion alone, then there is no need to add anything. Most of the times, the scope of quantification of a variable merely follow the above visual recursive rule. Example: Suppose we want to write the following: for all x for all y for all z ( z e x -> x=y ) suppose we wrote: zx>x=y then this would be read according to rule 4 as for all z ( z e x ) -> x=y thus visual recursion *alone* fails to do the job here, so we need to use the above rule itself to elucidate that the scope of quantification extends over the implication to the other side. This is done by adding the formula z=z on the other side so we write zx>x=y z=z An alternative approach would be to add a semi-colon to mark the end of the quantification zx>x=y; Example: the following formula t _x yt <> w _k uw. <> u is a wiener ordered pair i _s,r isru > i subset k j _p,q jpqu 0q > j=x > yw is the abbreviation of: for all t Exist x for all y ( y e t <-> for all w ( Exist k for all u ( u e w <-> (u is a wiener ordered pair & for all i (Exist sr (iesereu) -> i subset k)& for all j (Exist pq (jepeqeu & 0eq) -> j=x))) -> yew)). examine how the sub-rules of Rule 4 work. Writing ZF set theory axioms: _____________________________________________ Extensionality: zx<>zy > x=y Foundation: _yx > _zx _cz cx Empty: _x ~yx Pairing: a,b _x yx.<> y=a|y=b Union: a _x yx <> _z yza Power: a _x yx<> zy>za Separation: a _x yx.<> yaQ Replacement: x!yQ(x,y)> a _b zb <>_xaQ(x,z) Infinity: _x 0x yx > z uz.<>uy|u=y > zx _______________________________________________ This syntax is both elegant, abbreviating and easily readable. I claim that: "Any formula that can be written in the standard manner, can be written in a uniquely interpretable manner using this method". I don't have a proof though, but I think it can be proved, because the use of dot notations already has been proven to have unique readability, all the other rules are alternatives of already used standard notations, so definitely it is the case that the statement above is correct. However this methodology is superior to the standard notation in its abbreviation power, clarity, and elegance. The standard notation appears as too long, crowded, boring, and clumsy by comparison, that is besides it contains inverted symbols and rotated symbols without an obvious justification. In my personal opinion the above record is the *best way of writing first order logic with identity and membership*, known thus far! Zuhair
From: Marshall on 7 May 2010 09:18 On May 7, 1:50 am, zuhair <zaljo...(a)gmail.com> wrote: > > In my personal opinion the above record is the *best way > of writing first order logic with identity and membership*, > known thus far! I would disagree. You overuse juxtaposition. It means both conjunction and set membership. How do you distinguish? You also use it, with a space, to mean universal quantification. Juxtaposition is the biggest weapon in the syntax designer's arsenal; it should be fired only with the utmost care for the greatest need. Your dot notation is at least somewhat creative, but it has some unfortunate characteristics. For one thing, it apparently requires the writer to distinguish between terms where there is no requirement to do so. For any operator with the associative property, there is no meaningful difference between different orderings. (P|Q)|R = P|(Q|P). Requiring the distinction to be written down is requiring people to attend to a difference that makes no difference. Another problem in that it requires expressions to be rewritten during substitution. Marshall
From: Marshall on 7 May 2010 10:50 On May 7, 1:50 am, zuhair <zaljo...(a)gmail.com> wrote: > > This syntax is both elegant, abbreviating and easily > readable. Maximizing abbreviation has the opposite effect as improving readability. > The standard notation appears as too long, > crowded, boring, and clumsy by comparison, that is > besides it contains inverted symbols and > rotated symbols without an obvious justification. The standard notation is already quite terse, to the point that compressing it further strikes me as a bad idea. The symbols you describe as rotated aren't. Does the English alphabet contain rotated symbols? I would say not, and yet lowercase u and n are the same modulo rotation. The "shortening" of the implication arrow to a greater-than symbol is an ASCII-specific optimization. The right arrow is a single symbol in unicode, and when written by hand. Also, this makes is difficult/ambiguous to write anything involving numeric comparison. This may not be a goal of yours, but it is a common application of standard notation. > In my personal opinion the above record is the *best way > of writing first order logic with identity and membership*, > known thus far! "Best" is relative to a given set of requirements, and any design is going to involve making tradeoffs. Marshall
From: facemelter1729 on 7 May 2010 10:52 Shut the hell up, you camel-sodomizing towel-head. "zuhair" <zaljohar(a)gmail.com> wrote in message news:9b71985e-af64-4976-b013-6012c4148d1c(a)r11g2000yqa.googlegroups.com... > > Logical nothingness: muh brane > >---------------------------------<@
From: zuhair on 7 May 2010 17:20
On May 7, 8:18 am, Marshall <marshall.spi...(a)gmail.com> wrote: > On May 7, 1:50 am, zuhair <zaljo...(a)gmail.com> wrote: > > > > > In my personal opinion the above record is the *best way > > of writing first order logic with identity and membership*, > > known thus far! > > I would disagree. > > You overuse juxtaposition. It means both conjunction and > set membership. How do you distinguish? In the case of membership, we are juxtaposing individual terms (variables, constants, or functions). On the other hand, in the case of conjunction we are juxtaposing *formulas* . You also use it, > with a space, to mean universal quantification. No that is not correct, I use the space between a quantifier (weather universal or existential) and the formula having the variables quantified upon by these quantifiers, that is clear actually, the space is between a single symbol (that is precessed by the symbol "_" , or not preceded by any symbol) and a formula. so there is a difference between the three cases. Juxtaposition > is the biggest weapon in the syntax designer's arsenal; > it should be fired only with the utmost care for the greatest > need. Agreed. > > Your dot notation is at least somewhat creative, but it has > some unfortunate characteristics. For one thing, it apparently > requires the writer to distinguish between terms where > there is no requirement to do so. For any operator with > the associative property, there is no meaningful difference > between different orderings. (P|Q)|R = P|(Q|P). Requiring > the distinction to be written down is requiring people to > attend to a difference that makes no difference. Another > problem in that it requires expressions to be rewritten > during substitution. No that is not true. Although I didn't know about the dot notations that exist in PM (principa mathematica) and when I did it it was my own creative thought, but I later realized that it actually existed since Frege's days, used in PM, and used by Quine also, so it is know very well to be equivalent to the Bracket notation, and actually superior to it. Second point, about your remark about attending to differences that makes no difference. Suppose you want to write Q or P or R This can be written here as Q|P|R there is no problem here, the dot notation is only required when matters make a difference, like brackets exactly. As regards your latest statement, let met quote it: \Another problem in that it requires expressions to be rewritten during substitution.\ I really don't know what you mean by that, I usually write the whole formula, then make the punctuation (the dot notation), same thing is done with the brackets. > > Marshall |