From: Jesse F. Hughes on
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
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
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
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
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