From: Jesse F. Hughes on 23 May 2010 08:24 stevendaryl3016(a)yahoo.com (Daryl McCullough) writes: > Nam Nguyen says... > >>Daryl McCullough wrote: >>> Nam Nguyen says... >>>> How could any formula be true in a model in which its universe >>>> U and any n-ary predicate are empty? >>> >>> In the empty model, any formula of the form forall x Phi(x) >>> is true, >> >>Can you explain in some details why? > > Well, in classical logic, "forall x, Phi(x)" is interpreted to mean > the same thing as "not (exists x, not Phi(x))". Strictly speaking, does "empty model" mean anything at all? We're talking FOL=, right? So, if I'm not mistaken, one can conclude in FOL= that (Ex)x = x. (Ax) x = x x = x (A-Elim) (Ex) x = x (E-Intro) Hence, a model must have non-empty support, since (Ex) x = x must be true in every model. Unless I'm simply being butt-stupid here. To be sure, this doesn't negate Daryl's primary point. If we try to interpret a language in the trivial "model", we will find that every universal statement is true. My point is only that such interpretations don't have the property that, if P is provable, then P is true under the interpretation. -- Jesse F. Hughes "If you are a consumer that's taking advantage of the technologies that exist ... then the spam problem for you is solved." --MS spokesman verifying that the spam problem has been solved.
From: Marshall on 23 May 2010 09:30 On May 22, 11:14 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > Jesse F. Hughes wrote: > > Nam Nguyen <namducngu...(a)shaw.ca> writes: > > >> It's now your turn (as well as WH's) to answer my question: if you > >> think my answer is incorrect, then where and why (in some technical > >> details)? > > > Not my turn. I don't bother with substantive discussions with you. > > It is obvious that you don't really understand logic at all and these > > discussions never seem to have a positive effect on your ignorance. > > > I just wanted to see if you'd be prodded to actually answer William's > > question. I'll leave the replies to him. > > If you "don't bother with substantive discussions" with me on technical > matters then you don't ask or prod me. Your role here is not to make the rules of discussion. Your role is to misunderstand technical definitions in ways that astonish and amuse the general audience. > You, Jesse F. Hughes, are an intellectual dishonest and coward. Bullshit. He's the exact opposite. You, however, are a talentless buffoon. And a crank. Marshall
From: Marshall on 23 May 2010 09:31 On May 22, 11:38 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > William Hughes wrote: > > On May 22, 9:41 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > >> William Hughes wrote: > >>> On May 22, 7:37 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > >>>> there's no formula is true in M3 > >>> Nonsense The formula > >>> (not(exits x) or blue(x)) > >>> is true in M3 and provable in T3. > >> Did I already say "by definition of model it's false" > > > Many times. You are under the delusion that by saying > > something many times you can change it from incorrect to > > correct. > > Oh, I offered explanations with technical details and all that > anyone could search or see from the ng server so that is never > an issue with me. This is completely consistent with what WH said. You would understand that you haven't supplied any refutation, if you didn't fail so badly at basic logic. Marshall
From: Marshall on 23 May 2010 09:53 On May 23, 5:24 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote: > stevendaryl3...(a)yahoo.com (Daryl McCullough) writes: > > Nam Nguyen says... > >>Daryl McCullough wrote: > >>> Nam Nguyen says... > >>>> How could any formula be true in a model in which its universe > >>>> U and any n-ary predicate are empty? > > >>> In the empty model, any formula of the form forall x Phi(x) > >>> is true, > > >>Can you explain in some details why? > > > Well, in classical logic, "forall x, Phi(x)" is interpreted to mean > > the same thing as "not (exists x, not Phi(x))". > > Strictly speaking, does "empty model" mean anything at all? I'm disinclined to think so. I am under the impression that in ordinary usage, for something to qualify as a "model" its domain needs to have at least two elements. Certainly we can meet all the other criteria for a model with only a 1-element domain, but that's quite the degenerate case. In the cardinality-1 model, there is only one possible table for each arity; the constants are all the same; every possible such model of every possible signature can be fully axiomatized by the same degenerate axiom, "x=y". > My point is only that such > interpretations don't have the property that, if P is provable, then P > is true under the interpretation. Yes, and I would suggest that that fact by itself is enough to disqualify any structure with an empty domain from being called a model. It can't be the model *of* anything. Marshall
From: Daryl McCullough on 23 May 2010 10:05
Jesse F. Hughes says... >Strictly speaking, does "empty model" mean anything at all? > >We're talking FOL=, right? So, if I'm not mistaken, one can conclude >in FOL= that (Ex)x = x. This is a matter of convention as to whether we allow empty models or not. Usually, people assume that there is a nonempty domain, (because the theory of the empty domain is trivial). >(Ax) x = x > x = x (A-Elim) >(Ex) x = x (E-Intro) The latter rule of inference is only sound for nonempty domains. I had a discussion with David Ullrich (I think) a few years back, and we couldn't find a good, non-cumbersome set of inference rules for untyped first-order logic that didn't assume nonempty domains However, in *typed* first-order logic, you usually don't want to assume non-empty domains for each type. The way that typed first-order logic works (or at least one way to do it) is to have kinds of "assumptions": assumptions that a certain proposition is true, and "type assignments" for variables. There are similarly two kinds of conclusions: theorems, (some proposition is true) and type judgment (some term has some particular type) So your proof above would look like this (where T is a type symbol, and where |- separates the assumptions, on the left side, from the conclusions, on the right side). The rules are something like this: (A-Elim) (where Gamma is a list of assumptions, t is a term, and T is a type symbol) Gamma |- t:T Gamma |- (Ax:T) Phi(x) ---------------------- Gamma |- Phi(t) (A-Intro) (where Gamma is a list of assumptions, x is a variable not occurring in Gamma) Gamma, x:T |- Phi(x) -------------------- Gamma |- (Ax:T) Phi(x) (E-Intro) Gamma |- t:T Gamma |- Phi(t) --------------- Gamma |- (Ex:T) Phi(x) The rules for type conclusions are: (Assumption) Gamma, x:A |- x:A (Function application) (where A => B means the type of all functions from type A to type B) Gamma |- f:(A => B) Gamma |- t:A ------------------- Gamma |- f(t) : B The types are usually closed under various operations, such as product formation, disjoint union formation, function space formation, etc. If you try to carry through your proof in a typed system, it doesn't quite work: 1. |- (Ax:T) x=x (Axiom) 2. y:T |- y=y (A-Elim) 3. y:T |- (Ex:T) x=x (E-Intro) 4. |- (Ay:T) (Ex:T) x=x (A-Intro) To actually prove "(Ex:T) x=x", you need, based on no assumptions, to be able to prove the existence of an object of type T. >Hence, a model must have non-empty support, since (Ex) x = x must be >true in every model. > >Unless I'm simply being butt-stupid here. No, the usual assumption in untyped first order logic is that the domain is nonempty. Ex x=x is valid for nonempty domains. -- Daryl McCullough Ithaca, NY |