Well you see, Jesse, that's your major source of confusion. The sad thing
is I already explained it to you before but you ignored it.
Let's let L1(e,*,+) be a language. Let's now consider the following formulas:
F1: Ax[x=e]
F2: Axy[x*y=y*x]
F3: Axyz[x*(y+z)=(x*y)+(x*z)]
Of course all F1, F2, F3 formulas are written in L1. Note, however, L1 is
*not the only language* the 2 formulas F1 and F2 would be written in!
There are infinite number of languages, besides L1, F1 and F2 would be
written in: L(e,*), L'(e,*,+, <), L''(e,*,+, <'), L'''(e,*,+, +', <, <''),...
But amongst all of them stands out _the_ language L(e,*) where each
of the non-logical symbols would be in some axioms of the axiom-set
(which is just a formal system), say, T1 = {F1, F2}. You could give
L(e,*) a name like the-minimum-language-of-T1 if you'd like, but standard
text books would name it the-language-of-T1, symbolized as L(T1). And in
this case we could also just give it another alias L2 df= L(T1) = L(e,*).
Do you now understand what L2, L(T1), and L(e,*) are the very same language?
The point I've been defending is then, in this case of the above
T1 = {F1, F2}, the Inference rules such as the Expansion and Universal
Instantiation rules would operate *only* on T1's theorems that are written
in L2 = L(T1) = L(e,*). For example, from T1's theorem F1, you can't say
(F1 \/ Ax[x < x]) is a T1's theorem, because although both F1 and
Ax[x < x] are formulas written in, e.g., the language L'(e,*,+, <) or
L'''(e,*,+, +', <, <'') above, only F1 is in *the language of the theory*
T1, namely L2 = L(T1) = L(e,*).
>
> Now, if you mean that T1 is the *set* of axioms (and not the theory in
> L1), then L(T1) is not thus far defined.
You got to make it clear in your head that T1's theorem-formulas can be
said to be written in infinite number of languages. But that doesn't
diminish the fact that L(T1) - i.e. the (unique) language of T1 can
be perfectly defined. I've both defined and given an example right above!
> Maybe it means the set of
> non-logical symbols occurring in formulas in the set T1.
That's correct. I said before i's basically the summation of all nonlogical
symbols of a theory's axioms, which is basically what you've just said here.
> In that case, of course, L(T1) may be a proper subset of L2.
No. You just misread what I wrote. As shown above L2 is defined to be L(T1),
which is L(e,*) in the above example. What is true here is L1(e,*,+),
L'(e,*,+, <), L''(e,*,+, <'), L'''(e,*,+, +', <, <''),... all are
non-trivial *extension* of L2!
>
>> The confusion that you, Jesse, and few others seem to have had
>> (as indicated by your statement below) is that it must be true L1 = L2,
>> in all circumstances!
>>
>> That's not the case!
>
> I swear that here it seems you want to reverse positions. We've all
> claimed that a set of formulas may be used to define theories in a
> whole slew of languages.
You're incorrect because you mixed up informality and precise technical
terminology! A set T of axiom-formulas always defines a unique theory, although
the axioms themselves can be said to be written in infinite number of languages.
But amongst these languages, there's only one language that all the axioms
can be said to be *non-vacuously in*: that language is called _the_ language
of T and is typically denoted by L(T).
And for each formal system T, L(T) is the only valid language that one could
apply the rule of inferences to the axioms (of T of course).
>
> Let's start back at the beginning. Here's what you said.
>
> ,----
> | In summary:
> |
> | A3. Axy(x+y=0)
> |
> | can't be _formally_ proven from the lone axiom x=y.
> `----
>
> How [...] do you intend to defend that?
>
> Let L={+,0} and let T be the theory in L defined by {(Ax)(Ay)(x=y)}.
> Now, tell me slowly why T does not prove (Ax)(Ay)(x+y=0).
Because, as explained many times, L={+,0} is *only* _a_ language that
T = {(Ax)(Ay)(x=y)} is written in. L is not _the_ (unique) language L'(T)
that has *zero* non-logical symbols and that T is *also written in* and that
one could _validly_ apply any Inference rule to the axiom (Ax)(Ay)(x=y),
which is also written in this non-L language.
Do you now understand that you, David, MoeBlee, and others have just had a
misunderstanding on what would constitute as valid application of certain
Inference rules?
--
"To discover the proper approach to mathematical logic,
we must therefore examine the methods of the mathematician."
(Shoenfield, "Mathematical Logic")
> Jesse F. Hughes wrote:
>>
>> What is this theory T1? Above, we defined it as a theory in language
>> L1, so if this is how we define T1, then L(T1) = L1.
>
> Well you see, Jesse, that's your major source of confusion. The sad thing
> is I already explained it to you before but you ignored it.
>
> Let's let L1(e,*,+) be a language. Let's now consider the following formulas:
>
> F1: Ax[x=e]
> F2: Axy[x*y=y*x]
> F3: Axyz[x*(y+z)=(x*y)+(x*z)]
>
> Of course all F1, F2, F3 formulas are written in L1. Note, however, L1 is
> *not the only language* the 2 formulas F1 and F2 would be written in!
>
> There are infinite number of languages, besides L1, F1 and F2 would be
> written in: L(e,*), L'(e,*,+, <), L''(e,*,+, <'), L'''(e,*,+, +', <, <''),...
> But amongst all of them stands out _the_ language L(e,*) where each
> of the non-logical symbols would be in some axioms of the axiom-set
> (which is just a formal system), say, T1 = {F1, F2}. You could give
> L(e,*) a name like the-minimum-language-of-T1 if you'd like, but standard
> text books would name it the-language-of-T1, symbolized as L(T1). And in
> this case we could also just give it another alias L2 df= L(T1) = L(e,*).
Your claim about what standard text books say is nonsense. I invite
you once again to look over the following three quotes and let me know
if these guys are non-standard.
**********************************************************************
"We consider a language to be completely specified when its symbols
and formulas are specified. This makes a language a purely
syntactical object. Of course, most of our languages will have a
meaning (or several meanings); but the meaning is not considered to
be part of the language. We shall designate the language of a formal
system F by L(F)."
"The next part of a formal system consists of its /axioms/. Our
only requirement on these is that each axiom shall be a formula of
the language of the formal system." [p. 4 in my copy of Shoenfield]
"We consider a first order language L. By a theory T in L we mean a
set of sentences of L." [Keisler's contribution to Barwise's
handbook]
"A /theory/ can now be defined as a certain ordered pair, consisting
of two things [duh!]: (a) a class of non-logical constants, and (b)
a class of non-logical axioms which contain no non-logical constants
other than those in the class mentioned in (a). Thus, two theories
T and T' are identical if and only if they are identical in their
non-logical constants and their non-logical axioms." [Robert Rogers
writes in "Mathematical Logic and Formalized Theories"]
**********************************************************************
[NOTE: I've put little stars around the quotations, because Nam seems
to always overlook these quotes. I'm hoping this time he will see
them and respond.]
How come *none* of them claim that the language of a theory is the set
of all non-logical symbols appearing in the axiom? On the contrary,
they explicitly say that a theory is an arbitrary set of formulas of a
*given* language. Thus, it makes perfect sense to say that your set
T1 of axioms defines a theory of the language L1.
> Do you now understand what L2, L(T1), and L(e,*) are the very same
> language?
Yes, sure.
> The point I've been defending is then, in this case of the above
> T1 = {F1, F2}, the Inference rules such as the Expansion and Universal
> Instantiation rules would operate *only* on T1's theorems that are written
> in L2 = L(T1) = L(e,*). For example, from T1's theorem F1, you can't say
> (F1 \/ Ax[x < x]) is a T1's theorem, because although both F1 and
> Ax[x < x] are formulas written in, e.g., the language L'(e,*,+, <) or
> L'''(e,*,+, +', <, <'') above, only F1 is in *the language of the theory*
> T1, namely L2 = L(T1) = L(e,*).
Name *one* author who clearly agrees with you.
Note: I agree that the consequence of any rule of inference must be a
formula in the language of the theory. No one has said otherwise.
The point of (endless, repetitive) contention is your claim that a
given set of axioms defines a theory in one language only.
Let T1 be the set {F1, F2} and let L={e,*,+, +', <, <''}. If we
consider T1 as a theory in L (which we certainly can do), then
T1 |- F1 \/ Ax[x < x]
(Note: In Rogers' terminology, T1 is not literally a theory, but
<L,T1> is. This is probably the most unambiguous definition.)
If we consider T1 as a theory in L2, then F1 \/ Ax[x < x] is not a wff
in the theory T1, so T1 doesn't prove it.
>
>>
>> Now, if you mean that T1 is the *set* of axioms (and not the theory in
>> L1), then L(T1) is not thus far defined.
>
> You got to make it clear in your head that T1's theorem-formulas can
> be said to be written in infinite number of languages. But that
> doesn't diminish the fact that L(T1) - i.e. the (unique) language of
> T1 can be perfectly defined. I've both defined and given an example
> right above!
What you call L(T1) is a special language for the set of axioms T1,
yes. And any *theory* comes with a unique language, by definition.
But a set of axioms does not, by itself, define a theory. We first
choose the language of the theory and then the set of axioms.
[...]
> And for each formal system T, L(T) is the only valid language that one could
> apply the rule of inferences to the axioms (of T of course).
Again, show me a single author that says this.
>> Let's start back at the beginning. Here's what you said.
>>
>> ,----
>> | In summary:
>> |
>> | A3. Axy(x+y=0)
>> |
>> | can't be _formally_ proven from the lone axiom x=y.
>> `----
>>
>> How [...] do you intend to defend that?
>>
>> Let L={+,0} and let T be the theory in L defined by {(Ax)(Ay)(x=y)}.
>> Now, tell me slowly why T does not prove (Ax)(Ay)(x+y=0).
>
> Because, as explained many times, L={+,0} is *only* _a_ language that
> T = {(Ax)(Ay)(x=y)} is written in. L is not _the_ (unique) language L'(T)
> that has *zero* non-logical symbols and that T is *also written in* and that
> one could _validly_ apply any Inference rule to the axiom (Ax)(Ay)(x=y),
> which is also written in this non-L language.
>
> Do you now understand that you, David, MoeBlee, and others have just had a
> misunderstanding on what would constitute as valid application of certain
> Inference rules?
No. I see that you have a strange personal interpretation of the
definition of theory. I've seen no other author use this definition.
I've given three quotations showing a different definition. I see no
advantages to your definition.
I see no misunderstanding on my part.
--
Jesse F. Hughes
"Sigh. Back to figuring out how to solve the factoring problem and
ending the world as we know it." -- James S. Harris
Why?
> I invite
> you once again to look over the following three quotes and let me know
> if these guys are non-standard.
Nothing I've said would contradict these "guys". You've just mixed up
between what I said and what they said, as I'll demonstrate below.
>
> **********************************************************************
> "We consider a language to be completely specified when its symbols
> and formulas are specified. This makes a language a purely
> syntactical object. Of course, most of our languages will have a
> meaning (or several meanings); but the meaning is not considered to
> be part of the language. We shall designate the language of a formal
> system F by L(F)."
>
> "The next part of a formal system consists of its /axioms/. Our
> only requirement on these is that each axiom shall be a formula of
> the language of the formal system." [p. 4 in my copy of Shoenfield]
>
>
> "We consider a first order language L. By a theory T in L we mean a
> set of sentences of L." [Keisler's contribution to Barwise's
> handbook]
>
> "A /theory/ can now be defined as a certain ordered pair, consisting
> of two things [duh!]: (a) a class of non-logical constants, and (b)
> a class of non-logical axioms which contain no non-logical constants
> other than those in the class mentioned in (a). Thus, two theories
> T and T' are identical if and only if they are identical in their
> non-logical constants and their non-logical axioms." [Robert Rogers
> writes in "Mathematical Logic and Formalized Theories"]
> **********************************************************************
>
> How come *none* of them claim that the language of a theory is the set
> of all non-logical symbols appearing in the axiom?
They actually do. You either didn't read the quotes carefully, or didn't
read more relevant parts (besides the quotes) they also wrote, or didn't
do enough reasoning based on them, or all of the above.
For example, from the quotes above:
- "a formal system consists of its /axioms/"
- "each axiom shall be a formula of the language of the formal system".
and from Shoenfield's page 14:
- " A first-order-language is thus completely determined by its nonlogical
symbols"
you couldn't logically conclude that "the language of a theory is the set
of all non-logical symbols appearing in the axiom[s]"? Or that L(e,*) is
the language of the theory T1 = {F1, F2} above?
> On the contrary,
> they explicitly say that a theory is an arbitrary set of formulas of a
> *given* language.
But where in all that do they explicitly oppose the facts that the language
of a theory is still uniquely definable, and that in this example of T1
above it's precisely L(e,*)?
> Thus, it makes perfect sense to say that your set
> T1 of axioms defines a theory of the language L1.
Again, you were just confused the fact T1 is written (vacuously) in L1
and the fact the language of T1 is L2, as in "L2, L(T1), and L(e,*)
are the very same language" and to which you already agreed to that,
as in "Yes, sure".
Didn't I also explain below the following:
>> You got to make it clear in your head that T1's theorem-formulas can
>> be said to be written in infinite number of languages. But that
>> doesn't diminish the fact that L(T1) - i.e. the (unique) language of
>> T1 can be perfectly defined. I've both defined and given an example
>> right above!
?
>> Do you now understand what L2, L(T1), and L(e,*) are the very same
>> language?
>
> Yes, sure.
>
>> The point I've been defending is then, in this case of the above
>> T1 = {F1, F2}, the Inference rules such as the Expansion and Universal
>> Instantiation rules would operate *only* on T1's theorems that are written
>> in L2 = L(T1) = L(e,*). For example, from T1's theorem F1, you can't say
>> (F1 \/ Ax[x < x]) is a T1's theorem, because although both F1 and
>> Ax[x < x] are formulas written in, e.g., the language L'(e,*,+, <) or
>> L'''(e,*,+, +', <, <'') above, only F1 is in *the language of the theory*
>> T1, namely L2 = L(T1) = L(e,*).
>
> Name *one* author who clearly agrees with you.
I can't! None of them wrote in their books "I will clearly agree with
Nam and disagree with Jesse"!
So why don't you _explain_ *with your own reasons* why what I said
above is incorrect.
For instance, why don't you explain whether or not (F1 \/ Ax[x < x]) being
a theorem of T1 = {F1, F2} would violate the consequence closure property
of FOL.
>
> Note: I agree that the consequence of any rule of inference must be a
> formula in the language of the theory. No one has said otherwise.
But you did. Before you agreed L2 = L(T1) = L(e,*) is _the_ language
of T1 but now you claim below (F1 \/ Ax[x < x]) is a theorem in T1
even though this formula is *not* written in L2!
> The point of (endless, repetitive) contention is your claim that a
> given set of axioms defines a theory in one language only.
The point of contention is, *in your own words*, "the consequence of
any rule of inference must be a formula in the language of the theory".
What I've always said is a theory T - an axiom set - yields/defines a
unique L(T) you've agreed to refer to as "_the_ language of the theory
[T]" where "the consequence of any rule of inference must be a formula
in".
What you've believed in, in technical terminology, is _any_ non-trivial
extension of L(T) would be such _the_ language L(T). Which is incorrect.
Dou you understand that?
>
> Let T1 be the set {F1, F2} and let L={e,*,+, +', <, <''}. If we
> consider T1 as a theory in L (which we certainly can do), then
>
> T1 |- F1 \/ Ax[x < x]
>
> (Note: In Rogers' terminology, T1 is not literally a theory, but
> <L,T1> is. This is probably the most unambiguous definition.)
>
> If we consider T1 as a theory in L2, then F1 \/ Ax[x < x] is not a wff
> in the theory T1, so T1 doesn't prove it.
>>> Now, if you mean that T1 is the *set* of axioms (and not the theory in
>>> L1), then L(T1) is not thus far defined.
>> You got to make it clear in your head that T1's theorem-formulas can
>> be said to be written in infinite number of languages. But that
>> doesn't diminish the fact that L(T1) - i.e. the (unique) language of
>> T1 can be perfectly defined. I've both defined and given an example
>> right above!
>
> What you call L(T1) is a special language for the set of axioms T1,
> yes. And any *theory* comes with a unique language, by definition.
That's right. And *that unique language* is the one where, in your own
words, "the consequence of any rule of inference must be a formula in".
> But a set of axioms does not, by itself, define a theory.
You got all mixed up. Axioms are formulas defined in a language.
But an axiom-set defines a theory!
> We first
> choose the language of the theory and then the set of axioms.
That's only a manner of speaking, at informal level!
Mathematics and mathematical logic are timeless or time-agnostic:
you choose the language of the theory and the set of axioms
at the same time, if "time" were even a relevant concept here at all!
>
> I see no misunderstanding on my part.
Think again!
The sentence actually reads
"The next part of a formal system consists of its /axioms/."
It's very hard to understand what's going on here. On the one
hand, it's hard to believe you don't see that your misquotation
says something very different from the actual text. On the
other hand it's also hard to believe that you're intentionally
misquoting the text, given that the _actual_ text is right there
a few lines up where anyone can see it.
But your complaint about _Jesse_ not having read carefully
is hilarious.
>- "each axiom shall be a formula of the language of the formal system".
>
>and from Shoenfield's page 14:
>
>- " A first-order-language is thus completely determined by its nonlogical
> symbols"
>
>you couldn't logically conclude that "the language of a theory is the set
>of all non-logical symbols appearing in the axiom[s]"?
We _might_ be able to conclude that from your _misquotation_
of the text. But we certainly cannot conclude this from what the
text actually says - "a formal system consists of" and "The next
part of a formal system consists of" say very different things.
>[...]
>
>>
>> I see no misunderstanding on my part.
Assuming, although it's hard to believe, that you actually
don't see what you're misunderstanding here, one big thing
you seem to be misunderstanding is that "Part of X is Y"
does not imply "X is Y".
>Think again!
David C. Ullrich
"Understanding Godel isn't about following his formal proof.
That would make a mockery of everything Godel was up to."
(John Jones, "My talk about Godel to the post-grads."
in sci.logic.)
1. Potential.
2. Actual
Of course not. Contrary to your claim, Shoenfield does not say "a
formal system consists of its axioms". He says that *part* of a
formal system consists of its axioms. Keisler clearly states that a
theory is defined in a given language, not that the language is
defined by a set of axioms. Rogers says that for two theories to be
equal, both the set of axioms and set of non-logical symbols must be
equal. Why would he say this if the set of axioms determines the set
of non-logical symbols?
>> On the contrary,
>> they explicitly say that a theory is an arbitrary set of formulas of a
>> *given* language.
>
> But where in all that do they explicitly oppose the facts that the language
> of a theory is still uniquely definable, and that in this example of T1
> above it's precisely L(e,*)?
They explicitly oppose this claim in each and every case by saying
that we choose the language *first* and then a set of axioms is any
set of formulas in that language.
>> Thus, it makes perfect sense to say that your set
>> T1 of axioms defines a theory of the language L1.
>
> Again, you were just confused the fact T1 is written (vacuously) in L1
> and the fact the language of T1 is L2, as in "L2, L(T1), and L(e,*)
> are the very same language" and to which you already agreed to that,
> as in "Yes, sure".
Of course L2, L(T1) and L(e,*) are the same language, given your
definition of L(T1) as the minimal language of the set T1. I agree
with that. I never agreed that L(T1) is the only possible language
for a theory involving the set T1 of axioms.
> Didn't I also explain below the following:
>
>>> You got to make it clear in your head that T1's theorem-formulas can
>>> be said to be written in infinite number of languages. But that
>>> doesn't diminish the fact that L(T1) - i.e. the (unique) language of
>>> T1 can be perfectly defined. I've both defined and given an example
>>> right above!
>
> ?
You "explained" it, but it's false.
A given theory has a unique language, yes, but it is not determined by
the set of axioms.
>>> Do you now understand what L2, L(T1), and L(e,*) are the very same
>>> language?
>>
>> Yes, sure.
Right. You defined L(T1) as a certain set and I agreed that set was
equal to L2 and L(e,*). I did not agree that this set is the only
possible language for a theory defined by T1.
[...]
> I can't! None of them wrote in their books "I will clearly agree with
> Nam and disagree with Jesse"!
>
> So why don't you _explain_ *with your own reasons* why what I said
> above is incorrect.
>
> For instance, why don't you explain whether or not (F1 \/ Ax[x < x]) being
> a theorem of T1 = {F1, F2} would violate the consequence closure property
> of FOL.
It does not violate any closure property.
Let L = {*,e,<} and consider the set T1 as a theory in L. (In Roger's
terms, consider the theory <L, T1>).
Then T1 |- (F1 \/ Ax[x < x]) -- or, better,
<L,T1> |- (F1 \/ Ax[x < x]).
What closure property was violated.
>> Note: I agree that the consequence of any rule of inference must be a
>> formula in the language of the theory. No one has said otherwise.
>
> But you did. Before you agreed L2 = L(T1) = L(e,*) is _the_ language
> of T1 but now you claim below (F1 \/ Ax[x < x]) is a theorem in T1
> even though this formula is *not* written in L2!
You misunderstood what I was agreeing to. Certainly, we can define a
theory consisting of the pair <L2,T1>. This theory would not prove
that formula, since it would not be a wff in this theory.
>> The point of (endless, repetitive) contention is your claim that a
>> given set of axioms defines a theory in one language only.
>
> The point of contention is, *in your own words*, "the consequence of
> any rule of inference must be a formula in the language of the
> theory".
We agree on this claim.
> What I've always said is a theory T - an axiom set - yields/defines a
> unique L(T) you've agreed to refer to as "_the_ language of the theory
> [T]" where "the consequence of any rule of inference must be a formula
> in".
I did not and do not agree to that.
I see no point in continuing. I thought you were avoiding the
quotations because it was clear to the casual reader that they show
you are wrong. But, even though this fact is clear, you will twist
the words of Shoenfield to pretend otherwise while ignoring the other
two authors.
This argument has gone far enough. I will summarize my position once
more.
In every presentation of logical theory that I've seen thus far, one
fixes a language L and a theory T in L is any set of formulas of L.
Obvious, if T is a set of formulas in L, then there is another
language L' such that T is also a set of formulas in L'. Thus, the
language of T is determined only by context: by the stipulation of L
at the beginning.
There is *no* requirement that every non-logical symbol of a theory's
language occurs in the set T. Not a single author I've found makes
this claim.
Rogers actually has the clearest notation in this regard. He defines
a theory as an ordered pair <L,T> so that we do not mistake the set T
for the theory T in L. A theory is *not* a set of axioms, but a set
of axioms interpreted in some given language (subject to the condition
that the axioms are formulas of the given language).
--
Jesse F. Hughes
"As you can see, I am unanimous in my opinion."
-- Anthony A. Aiya-Oba (Poeter/Philosopher)
More significantly, he explicitly says that we first define the
language and then the axioms, with *no* requirement other than that
the axioms are formulas in the language.
This is an explicit refutation of your claim that the axioms of a
theory define the language of the theory.
--
Jesse F. Hughes
"Marriage.. ..is the union of two persons of different sex for
life-long reciprocal possession of their sexual faculties."
-- Immanuel Kant, who died an unmarried virgin
Do you always learn _technical_ materials by _literally_ sticking to the
author's English-word-by-English-word?
>
> More significantly, he explicitly says that we first define the
> language and then the axioms, with *no* requirement other than that
> the axioms are formulas in the language.
I already mentioned to you that's just a manner of speaking (i.e.
writting style). He could have easily defined *fist* a theory as
a set axioms, *then* an axiom as just a formula, and then a formula
as a senctence written in a mathematical language L, and then *finally*,
a language L as consisting of symbols (logical or otherwise.
(This style of definition, which is an antithesis to your "first"
insistence,
is wildely used in software language definitions!)
Why do find it hard to understand that mathematical logics is
time-independent? Or let me rephrase the question: why do you refuse
to acknowledge time-indepenccy in FOL reasoning?
> This is an explicit refutation of your claim that the axioms of a
> theory define the language of the theory.
Let me give you a point-blank example so you'd understand you've
been wrong.
Withou letting you know what language or non logical symbols I've
stipulated in my mind. Now I'm giving you the following 2 *literal*
strings:
A1: Ax(x=e)
A2: Axy(x*y=y*x)
Now I'm giving you some instructions:
- 'A' is the logical symbol for the Univseral quantifiers
- '=' is the logical binary identity predicate symbol in FOL
- 'x','y' are just individual variable symbols.
Now a point-blank question: from all these can you *determine/define*
a language L, with the siganture that 'e' is an individual constant symbol
and '*' is a binary function one?
If your answer is "Yes", why did you say the incorrect statement:
"This is an explicit refutation of [Nam's] claim that the axioms of
a theory define the language of the theory"?
If your answer is "No", why don't you go and read Shoenfield (pg. 14)
about grouping terms using parenteheis *and* do some inteferences
from there. (For the record I already mentioned this page 14 in the
thread before; seems like to didn't pay attention to that).
> [Bla bla bla]
Please, asshole, shut up!
Are you suggesting now we should "descend" into debating which quotes
should be longer or shorter from post to post?
One of the key issues here is, e.g., from the 2 formulas:
> A1: Ax(x=e)
> A2: Axy(x*y=y*x)
could you determine a language L where rules of inference can be
applied, *without knowing _first_ what the stipulate nonlogical
symbols be*!
Why don't you answer that and put forward your own reasons,
instead of going round-abound on the styles of witting of
some authors or posters.
Per a fixed language L in which *all the theorems* are written in
(again note that it doesn't matter whether or not you'd stipulate
L "first"), then there can't be "extra" nonlogical symbols, beyond
the union of the symbols found in *all the theorems* of T.
If one allows, as you've incorrectly tried, the *fixed set* of
formula-strings T1 = {F1,F2} to have a theorem where there's
a *newer* symbol than that of L2(T) = {'e','*'}, then one *would
never have a _fixed set_ for all the theorems of T*, a blatant
violation of the inference consequent closure of FOL. In fact,
one would allow uncountably number of non-logical symbols that way.
The only way to prevent this run-away proliferation of nonlogical
symbols is to use, for a T, the language with *minimal* signature.
Do you understand it now?
To borrow one of the phrases of a poster of the past, Herbert Newman
is smoking broccoli, and fumes puffing out of his eyes.
> "Jesse F. Hughes" <je...@phiwumbda.org> wrote in message
> news:87tz46c...@phiwumbda.org...
>> "Jesse F. Hughes" <je...@phiwumbda.org> writes:
>>>
>>> Of course not. Contrary to your claim, Shoenfield does not say "a
>>> formal system consists of its axioms". He says that *part* of a
>>> formal system consists of its axioms.
>
> Do you always learn _technical_ materials by _literally_ sticking to the
> author's English-word-by-English-word?
Yes, when I want to learn what the author means, then I start by
reading his words.
>>
>> More significantly, he explicitly says that we first define the
>> language and then the axioms, with *no* requirement other than that
>> the axioms are formulas in the language.
>
> I already mentioned to you that's just a manner of speaking (i.e.
> writting style). He could have easily defined *fist* a theory as a
> set axioms, *then* an axiom as just a formula, and then a formula as
> a senctence written in a mathematical language L, and then
> *finally*, a language L as consisting of symbols (logical or
> otherwise. (This style of definition, which is an antithesis to
> your "first" insistence, is wildely used in software language
> definitions!)
Oh, I certainly acknowledge that if the author had used a different
definition, then things would be different. And, indeed, one *could*
define the language for a theory as you propose, but, as it happens,
that's not how *any* logician *does* define the language for a theory.
In any case, I'm pretty goddamned tired of this dull conversation.
The fact is that you're simply wrong. Every logician I know of
defines a formal theory by first specifying the language and then
specifying any set of formulas in that language as the theory.
I'm not going around in any more circles with you. It's clear to
everyone here that the quotations I've cited are contrary to what you
say. In fact, even LWalker has stopped defending you, and that's
saying something.
--
"...[W]hatever gifts I have, they are mine. And I do fully intend on NOT
doing more research, NOT teaching, and NOT doing any number of things
that other people may feel they have a right to tell me I should do, as
when you had the chance with me, you crapped out." --James S. Harris
No, of course not. There is no "run-away proliferation". You specify
the language and the axioms and then consequence is well-defined. No
one suggests that you get to go back and change your choice
thereafter.
But have it your way. I'm done with this pointless argument. You
won't admit your mistake and there's nothing to be gained by going on
and on like this.
--
"Memoirists like Frey and Augusten Burroughs belong to the long list of
those who should never have stopped using drugs. The drugs might have
made Frey more interesting, or they might have killed him. Either way,
American literature would have benefited." --John Dolan, www.exile.ru
More like you couldn't answer (among others) the point-blank
question I had for you:
>> from all these can you *determine/define* a language L, with the
>> siganture that 'e' is an individual constant symbol and '*' is
>> a binary function one?
> It's clear to
> everyone here that the quotations I've cited are contrary to what you
> say.
If I were you I would concern more on the technical essence behind
the quotations, than just the quotations themselves.
> In fact, even LWalker has stopped defending you, and that's
> saying something.
Lol. I'm not letting anybody here know my view whether or not
anybody involved in this thread is a crank. But iirc you believed
he is. Then why a crank's stopping defending anybody become
a central piece of *your* _method of reasoning_?
I *first* specified 'S' as a binary predicate symbol and *then* the
axiom Axyz[((xSy) /\ (xSz)) -> (y=z)] /\ Axy[x=y].
According to *you*, I'm a dead-meat now, so to speak, and can't change
my mind to have the axiom Axy[Sx=y] (where 'S' as a binary function
symbol) because some authors on FOL would "forbid" me to do it!
I didn't know FOL would be that dictatorial! Or, perhaps you want
to reflect on Shoendfield's "defined symbols" on page 6.
Of course I meant "(where 'S' is a unary function symbol)".
Most of the times Nam comes across as someone who
is perverse enough and arrogant enough to be a crank, but
just a tad shy of being stupid enough. Occasionally he gives
off some troll signals. Or maybe he's just a doctor.
Come to think of it, though, it doesn't really matter which one it is.
Marshall
>> I *first* specified 'S' as a binary predicate symbol and *then*
>> [state] the axiom Axyz[((xSy) /\ (xSz)) -> (y=z)] /\ Axy[x=y].
Great. :-)
>> According to *you*, I'm a dead-meat now, so to speak, and can't change
>> my mind to have the axiom Axy[Sx=y] (where 'S' as a unary function
>> symbol) [instead.]
>>
Exactly. Reason: "Axy[Sx=y]" would not be a wff then (and hence certainly
could/would not be an axiom).
On the other hand if you would consider a DIFFERENT formal system where
(i.e. in the language of which) 'S' is a unary predicate, then you
certainly could state/use the axiom Axy[Sx=y] _there_.
Herb
Comment added:
> On Sat, 2 May 2009 17:41:59 -0600 Nam D. Nguyen wrote:
>
>> I *first* specified 'S' as a binary predicate symbol and *then*
>> [state] the axiom Axyz[((xSy) /\ (xSz)) -> (y=z)] /\ Axy[x=y].
>
> Great. :-)
>
>> According to *you*, I'm a dead-meat now, so to speak, and can't change
>> my mind to have the axiom Axy[Sx=y] [instead].
>>
> Exactly. Reason: "Axy[Sx=y]" would not be a wff then (and hence certainly
> could/would not be an axiom _in the context of this system_).
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
> On the other hand, if you would consider a DIFFERENT formal system where
> Jesse F. Hughes wrote:
>>
>> I'm not going around in any more circles with you.
>
> More like you couldn't answer (among others) the point-blank
> question I had for you:
Yes, of course. It should be clear to everyone here that you are my
intellectual superior. Kudos!
--
"There are known knowns. There are things we know that we know. There
are known unknowns. That is to say there are things that we now know
we don't know. But there are also unknown unknowns. There are things
we don't know we don't know." -- Donald Rumsfield, Epistemologist
You missed the point of my example.
In the first axiom:
(1) Axyz[((xSy) /\ (xSz)) -> (y=z)] /\ Axy[x=y]]
there's a component:
(2) Axyz[((xSy) /\ (xSz)) -> (y=z)]
which is, as you already know, the definition of a *function* which
*is in turn just a binary relation*. The point is as far as FOL proof
is concerned, you couldn't even stipulate a binary predicate symbol
from a special binary predicate one which would stand for an unary
function, (and vice versa) - *without at least an axiom*!
If you meant + is an unary function then there must be an axiom
equivalent to (2) to signify this is a special 2-ary predicate symbol,
and then apply symbol re-definition (Shoenfield) to make it an unary
function one.
If you meant + is a predicate symbol, you'd need some other axioms
(like Axy[x+y] or Exy[x+y]) that doesn't involve equality symbol '='
to make sure that you're not talking about an unary function symbol,
disguised as a vanilla predicate symbol.
Either way you'd need some axioms. And as I've explained before,
once you got syntactical axioms, you could infer/define a language L
whose nonlogical symbols is collectively the union of those in the axioms.
Do you have any proof to the contrary, if you still believe what
I've said here is incorrect?
For what it's worth, it's beyond my caring whether or not I have more
technical knowledge on something over somebody. As one with mortal
knowledge, there are something I do know and there are always some I don't.
Can you just answer my technical (and rather simple) questions though?
> Jesse F. Hughes wrote:
>> Nam Nguyen <namduc...@shaw.ca> writes:
>>
>>> Jesse F. Hughes wrote:
>>>> I'm not going around in any more circles with you.
>>> More like you couldn't answer (among others) the point-blank
>>> question I had for you:
>>
>> Yes, of course. It should be clear to everyone here that you are my
>> intellectual superior. Kudos!
>
> For what it's worth, it's beyond my caring whether or not I have more
> technical knowledge on something over somebody. As one with mortal
> knowledge, there are something I do know and there are always some I don't.
>
> Can you just answer my technical (and rather simple) questions
> though?
Sure.
> Let me give you a point-blank example so you'd understand you've
> been wrong.
> Withou letting you know what language or non logical symbols I've
> stipulated in my mind. Now I'm giving you the following 2 *literal*
> strings:
> A1: Ax(x=e)
> A2: Axy(x*y=y*x)
> Now I'm giving you some instructions:
> - 'A' is the logical symbol for the Univseral quantifiers
> - '=' is the logical binary identity predicate symbol in FOL
> - 'x','y' are just individual variable symbols.
> Now a point-blank question: from all these can you *determine/define*
> a language L, with the siganture that 'e' is an individual constant symbol
> and '*' is a binary function one?
Yes, you *can* define such a language, and indeed this is a natural
choice of language for the set of axioms you suggest. But this is not
the only possible language for a theory involving the set {A1,A2} as
axioms.
Indeed, as we've seen, the entire approach you suggest here is
backwards from the general convention. We start by defining the
language L, so that we thereby specify the set of formulas. A theory
in L is thus any set of formulas of L. That's what every author I've
quoted has explicitly said.
> If your answer is "Yes", why did you say the incorrect statement:
> "This is an explicit refutation of [Nam's] claim that the axioms of
> a theory define the language of the theory"?
Given a set of formulas as above, we certainly can, if we wish, choose
to interpret these formulas as a theory in the minimal language they
define. But the axioms of a theory do not define the language of the
theory in the conventional approach. Rather, the axioms are
interpreted in the pre-specified language. How hard is that to
understand?
> If your answer is "No", why don't you go and read Shoenfield (pg. 14)
> about grouping terms using parenteheis *and* do some inteferences
> from there. (For the record I already mentioned this page 14 in the
> thread before; seems like to didn't pay attention to that).
I have no idea what you think I'll learn from p.14, but I'm glad you
mention this section on first-order theories. Let's read on, shall
we? From p. 22.
A /first-order theory/, or simply a /theory/, is a formal system
T such that
i) the language of T is a first-order language;
ii) the axioms of T are the logical axioms of L(T) and certain
further axioms, called the /nonlogical axioms/;
iii) the rules of T are the expansion rule, the contraction rule,
the associative rule, the cut rule and the E-introduction rule.
In order to specify a theory, we have only to specify its
nonlogical symbols and its nonlogical axioms; everything else is
given by the definition of a theory. Note also that the logical
axioms and the rules are determined as soon as the language is
chosen; they are independent of the nonlogical axioms.
Now, notice this: you specify *both* the symbols and the axioms. It
is simply, plainly obvious that in Shoenfield's presentation, the
nonlogical axioms do *not* determine the language. Otherwise, we
should specify a theory by specifying the nonlogical axioms alone.
I hope that I answered your questions sufficiently and now I'd prefer
to let this tedious conversation drop. It's evident we're getting
nowhere and it's also evident to me that you're sorely mistaken and
either unable or unwilling to admit it. I don't see any reason to
continue.
--
Jesse F. Hughes
"Had you told it like it was, it wouldn't be like it is."
-- Albert King
> [...] Either way you'd need some axioms. [...]
Sorry, but your claims amount to utter nonsense.
Herb
Loosely speaking, a language is just a subset of the set of all finite
strings over an alphabet.
Hence the "minimal language" that contains F1 and F2 contains *only*
F1 and F2, doesn't it?
And if it contains more, why does it not contain Ax[xx*=***x***] --
or does it?
Guffaw. No, I'm "suggesting" that when you omit a few key
words from a sentence you change the meaning.
See, if some text said "One should not jump to the
conclusion that black is white" and you claimed that
the text said "black is white" you'd be lying.
>One of the key issues here is, e.g., from the 2 formulas:
>
>> A1: Ax(x=e)
>> A2: Axy(x*y=y*x)
>
>could you determine a language L where rules of inference can be
>applied, *without knowing _first_ what the stipulate nonlogical
>symbols be*!
Another key issue is whether you're willing to intentionally
distort a quotation in an attempt to show it supports what
you've been saying. Yet another key issue is whether you
think the rest of us are so blind that we won't be able to
see that that's what you're doing even when an accurate
quote is given.
>Why don't you answer that and put forward your own reasons,
>instead of going round-abound on the styles of witting of
>some authors or posters.
>
David C. Ullrich
>[...]
>I didn't know FOL
Evidently not.
No fair complaining that you didn't say that, by the way -
you've used exactly the same technique in quoting texts,
distorting the meaning of a sentence by omitting part of it.
>what
>I've said here is incorrect
You finally got it! Congratulations.
Surely, Nam would agree that the quote above
fairly represents his position. Perhaps he would
even be offended by the mere suggestion that he might
complain. I can easily imagine Nam responding,
"Are you suggesting now we should 'descend' into
debating which quotes should be longer or shorter
from post to post?"
Jim Burns
Glad that we're in agreement. But remember your "Yes" here contradicts
what you said earlier:
>>> This is an explicit refutation of your [Nam's] claim that the axioms
>>> of a theory define the language of the theory"?
And yet a moment later, right below, you contradicted your "Yes" above,
again:
> But the axioms of a theory do not define the language of the
> theory in the conventional approach.
It doesn't matter how many quotes you've cited, as long as you flip-flop
from one post to another (on a key issue) it's hard to know what you're
really arguing about.
> Rather, the axioms are interpreted in the pre-specified language.
According to Shoenfield, languages, proofs, and even formal systems
are *purely syntactical*. So I really don't know what you meant by
"_interpreted_ in the pre-specified language".
> How hard is that to understand?
Very hard: "_interpreted_ in the pre-specified language" coupled with your
flip-flopping above makes it very difficult to understand your arguments
against what I've said about the key issue(s).
>
>> If your answer is "No", why don't you go and read Shoenfield (pg. 14)
>> about grouping terms using parenteheis *and* do some inteferences
>> from there. (For the record I already mentioned this page 14 in the
>> thread before; seems like to didn't pay attention to that).
>
> I have no idea what you think I'll learn from p.14, but I'm glad you
> mention this section on first-order theories. Let's read on, shall
> we?
We'll see if we should "read on".
[some quotations]
> It is simply, plainly obvious that in Shoenfield's presentation, the
> nonlogical axioms do *not* determine the language.
Here you go again; you contradict with your "Yes" statement above:
> Yes, you *can* define such a language, and indeed this is a natural
> choice of language for the set of [non-logical] axioms you suggest.
How does "a natural choice of language" rhyme with "do *not*
determine the language"?
You really should stop quoting authors' works to defend your
arguments, when you keep contradicting yourself!
***
Listen. It isn't really that hard to understand why you can't prove,
say, Axy(x+y=0) from the theory T = {Axy(x=y)} (the lone-axiom theory,
so to speak). I've explained to you more than one way, but there's
another simpler way.
Consider the 2 statements:
(a) There's only one building material in that house.
(b) The building material in that house is steel.
Can you conclude (b) from (a)? Of course not. Logically that's a logical
fallacy of over generalization (there might be a name for the fallacy).
Now consider the following:
(a') Axy[x=y]
(b') Ax[S(x)] ('S' would stand for, say, 'Steel'.)
(c') Ex[S(x)]
If from the theory T = {(a')} you could infer (b') then you'd commit
the same logical fallacy as exemplified by (a) and (b) above. To make
it work you need to extent T into T' = {(a'),(c')} and now (b') is
provable in T'.
Incidentally, in the theory T'' = {(c')}, neither could you prove
(b'). This is another kind over-generalization, i.e. the quantity
kind: from a few you can't conclude all! The other kind above is like
a quantity kind: from a single property you can't conclude another
property.
And "no", Shoenfield didn't *directly* state that. But if you reflect
a few quotations I had and do some diligent analysis you'd see it
for yourself.
Do you clearly see now that you and others had a misunderstanding on
the issue?
Sure. If one doesn't do a discussion *in good faith* - as you don't here;
and if one deliberately cuts the quote short just to be "smart" - as you do
here, then of course things would be read completely of of context. Is that
a surprise to you?
The point is do don't have a proof I *deliberately* cut any quote short
just to confuse my opponents. Obviously by definition quotes would be shorter
than the whole text book where they're quoted from; and quotes of quotes
would be shorter than before. But given a certain *genuine* context that
the way it would be (but people could always google the previous context
if necessary).
For the record, *I did inform you* why in certain genuine context I had
to cut some quotes shorter than before:
I wrote *to you*:
>>> You don't understand the point of debate here. I cut my own quoting of
>>> Shoenfield hoping it'd be shorter so Jesse would abandon the crazy idea
>>> that the number of non-logical symbols of the language of the finitely
>>> axiomatizable G "depends on context"! But my full quote of Shoenfield's
>>> writing is:
>>> [...]
So, really, if your intention here is just attacking like "hilarious", or if
you don't have any technical contributions in good faith to the discussion,
why don't you stop being so "smart" with your 1-phrase quotes and get lost!
Like you had any technical explanation why!
>
>
> Herb
I meant "The other kind above is like a quality kind:"
>David C. Ullrich wrote:
>> On Sat, 02 May 2009 19:11:30 -0600, Nam Nguyen <namduc...@shaw.ca>
>> wrote:
>>
>>> what I've said here is incorrect.
>>
>> You finally got it! Congratulations.
>
>Sure. If one doesn't do a discussion *in good faith* - as you don't here;
>and if one deliberately cuts the quote short just to be "smart" - as you do
>here, then of course things would be read completely of of context. Is that
>a surprise to you?
The idea that you changed "The second part of A is B" to "A is B"
in good faith is hilarious.
>The point is do don't have a proof I *deliberately* cut any quote short
>just to confuse my opponents. Obviously by definition quotes would be shorter
>than the whole text book where they're quoted from; and quotes of quotes
>would be shorter than before. But given a certain *genuine* context that
>the way it would be (but people could always google the previous context
>if necessary).
>
>For the record, *I did inform you* why in certain genuine context I had
>to cut some quotes shorter than before:
>I wrote *to you*:
>
> >>> You don't understand the point of debate here. I cut my own quoting of
> >>> Shoenfield hoping it'd be shorter so Jesse would abandon the crazy idea
> >>> that the number of non-logical symbols of the language of the finitely
> >>> axiomatizable G "depends on context"! But my full quote of Shoenfield's
> >>> writing is:
> >>> [...]
>
>So, really, if your intention here is just attacking like "hilarious", or if
>you don't have any technical contributions in good faith to the discussion,
>why don't you stop being so "smart" with your 1-phrase quotes and get lost!
David C. Ullrich
>> Yes, you *can* define such a language, and indeed this is a natural
>> choice of language for the set of axioms you suggest.
>
> Glad that we're in agreement. But remember your "Yes" here contradicts
> what you said earlier:
As I've said, I'm done with this conversation. But I should point out
that the following two claims are *not* contradictory:
(1) You *can* define a language in this way.
(2) It is *not* the conventional method to do so.
In the meantime, thanks much for the suggestions in how to interpret
plain written English regarding technical definitions. I'm sure I can
learn a lot from your kind tutelage.
--
"Now for once I might actually have an audience that realizes that
[my proof of Fermat's Last Theorem is correct], because you see,
they'll finally know what's in it for them--cold, hard cash."
--James Harris embarks on a new mathematical strategy.
> you can't prove,
> say, Axy(x+y=0) from the theory T = {Axy(x=y)}
In a language that has '+' as a 2-place operation symbol and '0' as a
0-place operation symbol, from the sole non-logical axiom
Axy x=y
by natural deduction we derive
Axy x+y=0
just as I had posted such a proof.
Nothing you've said refutes that simple fact.
/
Also, you've still not responded to the fact that I showed you an
exact textbook (cf. Hinman) definition of the notion of a proof in a
language, contrary to your claim that there is no such notion in
mathematical logic. And I've reminded you of your lack of response on
that point a few times. I wonder why you continue to ignore the
matter.
MoeBlee
P.S. In your other exchanges, you've yet again misread plain English:
To say that one may define a language from a set of axioms (i.e., to
say "yes" that one may so define a language) does not contradict that
one may also define a language simply by specifying the symbols and
arities of those symbols and that that is ordinary.
A first order language is determined by (thus definable by) its
symbols and their arities. One may take either route to defining a
language: (1) one takes the symbols and arities to be those determined
by some set of formulas in which those symbols occur or (2) one
simiply stipulates certain symbols and arities. And the second route
is common and is as described by Shoenfield and other authors.
For no good reason, you are just arbitrarily, and contrary even to the
textbook of your primary reference, ruling that (2) is disallowed.
Otherwise, there is no basis to object to stipulating that a certain
language has '+' and '0' as, respectively, a 2-place operation symbol
and 0-place operation symbol, then defining a theory in said language
to be the set of logical consequences of the sole non-logical axiom
"Axy x=y", and then showing a deduction of the formula "Axy x+y=0" of
said langauge, as said deduction then does provide that "Axy x+y=0" is
in the aforesaid theory.
MoeBlee
I've been always talking about FOL proof *in a theory*, *not in a language*.
OK. Do you remember earlier in the thread I mentioned that one could
stipulate a million languages if one would like, but here we're talking about
proof in the theory T = {Axy(x=y)} where L(T) has *zero* nonlogical
symbols.
That means we're *not talking about* "a language that has '+' ... 'o'". OK?
>
> Axy x=y
>
> by natural deduction we derive
>
> Axy x+y=0
>
> just as I had posted such a proof.
Do you mean the proof where you *invalidly used* the Universal
Instantiation rule in the theory T above where L(T) doesn't have
'+', '0'? If your answer is "Yes", I already demonstrated examples
(the latest being about the impossible provability of (b') Ax[S(x)]
in the theory T = Axy(x=y) due to over generalization); why don't you
refute my reasoning in those specific examples, if you don't agree
with them. If your answer is "No", you're not talking about FOL proof
as I've been talking about; and I'm not interested in such non-FOL proof
"in a language"
>
> Nothing you've said refutes that simple fact.
You're *not* talking about a FOL-theory-proof fact; so it doesn't matter to
me what that "simple" "fact" be. If you and other can't refute the simple
example I've just had about impossibility of proving (b') Ax[S(x)] in the
theory T = Axy(x=y), then nothing you say in this context would be "simple fact"
(they're rather "complex illusion and misunderstanding of what FOL syntactical
proof is about)
>
> /
>
> Also, you've still not responded to the fact that I showed you an
> exact textbook (cf. Hinman) definition of the notion of a proof in a
> language, contrary to your claim that there is no such notion in
> mathematical logic. And I've reminded you of your lack of response on
> that point a few times. I wonder why you continue to ignore the
> matter.
I've answered that one way or another; you just didn't listen carefully,
as well as ignored my reasons/examples. Basically, you weren't talking
about FOL syntactical proof *in a theory*.
But I am.
This is what you actually said in (1):
> Yes, you *can* define such a language, and indeed this is a natural
> choice of language for the set of [non-logical] axioms you suggest.
To me "indeed this is a _natural choice_ of language for the set of axioms"
very much contradicts with "It is *not* the _conventional method_ to do so".
Don't you think so?
>
> In the meantime, thanks much for the suggestions in how to interpret
> plain written English regarding technical definitions.
I think you know that English language is a natural language, which is
very much different from formal mathematical languages used in FOL reasoning.
> I'm sure I can learn a lot from your kind tutelage.
For what it's worth I don't have any desire to be a tutor here. All I've
been doing is *learning* from various conversations here. Most of my
disappointment in the conversations is that *genuine* appreciation
of rigidity of syntactical proofs in FOL is very low. To the point
that there are those who'd consider themselves as non-crank would offer
a kind of arguments typically offered by a crank.
I already stated early in the thread that one is free to specify/stipulate
a million languages if one cares to so so. You seem to have *distorted*
my "you can't here! What I said:
>> Listen. It isn't really that hard to understand why you can't prove,
>> say, Axy(x+y=0) from the theory T = {Axy(x=y)} (the lone-axiom theory,
>> so to speak). I've explained to you more than one way, but there's
>> another simpler way.
So, for the millionth time, MoeBlee, I'm not talking about defining
languages! What I simply stated is basically you can't validly apply
rules of inference to a formula that's not expressed in the L(T)
whose signatures are in the axioms of T.
If you'd like to spend 100 years defining a trillion extensions of
L(T), I wouldn't give a hood but neither would I say there's any
wrong with that.
Do recall I said basically rules of inference operate on formulas
that are theorems of a specified theory, not on any (extended) languages!
>
> A first order language is determined by (thus definable by) its
> symbols and their arities. One may take either route to defining a
> language: (1) one takes the symbols and arities to be those determined
> by some set of formulas in which those symbols occur or (2) one
> simiply stipulates certain symbols and arities. And the second route
> is common and is as described by Shoenfield and other authors.
>
> For no good reason, you are just arbitrarily, and contrary even to the
> textbook of your primary reference, ruling that (2) is disallowed.
Of course *your memory is short here*. In an early response *to you* I
said that one would be free in stipulating *million different formal
languages* of one cares to do so:
>> It's not that difficult actually. I could spend years talking about million
>> different formal languages - some might be syntactically isomorphic. Yet,
>> if I don't have any axioms when talking about _formal proof_ all those
>> million languages are irrelevant. Right? (And the debate here is about proof
>> of some formula!)
> Otherwise, there is no basis to object to stipulating that a certain
> language has '+' and '0' as, respectively, a 2-place operation symbol
> and 0-place operation symbol, then defining a theory in said language
> to be the set of logical consequences of the sole non-logical axiom
> "Axy x=y",
So far you've mentioned all the theorems of T = {Axy[x=y]} written in the
language L(T) that has *zero* nonlogical symbols. OK, that's fine.
> and then showing a deduction of the formula "Axy x+y=0" of
> said langauge, as said deduction then does provide that "Axy x+y=0" is
> in the aforesaid theory.
How on Earth would a theorem of T {Axy[x=y]} has a nonlogical symbol
while the language of the theory T has zero nonlogical symbol? I'd
guess you'd "instantiate" that nonlogical symbol through Universal
Instantiation you mentioned before.
But didn't I *already* refute through 2 or 3 examples? Violation of FOL
closure property, over generalization, remember?
But *I* gave my proof in the context I just described, yet you've been
claiming that my proof is incorrect.
So if, in the context *I* specified exactly, you now grant that my
proof of "Axy x+y=0" is correct, then good!
> > Axy x=y
>
> > by natural deduction we derive
>
> > Axy x+y=0
>
> > just as I had posted such a proof.
>
> Do you mean the proof where you *invalidly used* the Universal
> Instantiation rule in the theory T above where L(T) doesn't have
> '+', '0'?
No, for the MILLIONTH TIME, I am in the context that '+' and '0' ARE
symbols of the language. You just QUOTED me saying that '+' and ')'
are symbols of the language. And I said that '+' and '0' are symbols
of the language the VERY FIRST TIME (a few weeks ago now) I posted the
proof that you claimed incorrect.
For the Million+1th time now: I am giving the proof in a language in
which '+' and '0' ARE symbols. I've said it all along, over and over,
that my proof is correct in "any language" such '+' and '0' are
symbols of the stated arities.
> > Also, you've still not responded to the fact that I showed you an
> > exact textbook (cf. Hinman) definition of the notion of a proof in a
> > language, contrary to your claim that there is no such notion in
> > mathematical logic. And I've reminded you of your lack of response on
> > that point a few times. I wonder why you continue to ignore the
> > matter.
>
> I've answered that one way or another; you just didn't listen carefully,
No, I read your posts. You did not respond to my cite of Hinman saying
"proof in L" and giving an EXACT defintion of that notion, which is a
notion YOU claimed not to exist in mathematical logic - not "in
mathematical logic" was your own exact claim.
> as well as ignored my reasons/examples. Basically, you weren't talking
> about FOL syntactical proof *in a theory*.
>
> But I am.
So what? *I* was EXACTLY SPECIFIC as to my context ORIGINALLY but YOU
said that my proof was not correct.
And you said that there is no notion of "proof in a language" in
mathematical logic (no matter how you NOW qualify your statement).
But you were plainly incorrect. I showed you exactly where such a
notion is even FORMALLY given. Moreover, the notion is tacitly in play
when an author says such things as "here we consider some fixed
language L"; moreover, the notion is needed to define 'proof' in full
rigor as Hinman does. A proof is in a language (it can even be in more
than one language as long as the languages don't conflict as to the
symbols), since every line (or node, whatever, and putting aside
quibbles about temporary constants, etc.) in the proof must be a
formula - but to say 'is a formula' is to say 'is a formula of a
LANGUAGE', so every line in a proof must be a formula of at least one
language. So a proof is a proof in some language (or even set of
languages, if we like).
So, again, if you now grant that my proof is correct given the context
I originally mentioned (and have been reiterating over and over
again), then good!
It couldn't be more clear: I mentioned my context EXACTLY. Then I gave
a proof in that context. Then you claimed my proof was incorrect. So I
hope now that you do recognize that IN THE CONTEXT I GAVE, my proof is
correct after all.
MoeBlee
NO! Because he didn't say the natural choice is to pick a set of
axioms and then define a language from those axioms. Rather, he said
that GIVEN that we are defining a language from the set of axioms you
gave, then the language you've chosen is the natural choice.
Again, one can define a language by inferring the signature of the
language from some set of suitable formulas. And one can ALSO define a
language by stipulating the signature of the language without
reference to any particular set of formulas. And the second route is
the more common route, and it is the route that Shoenfield describes.
And given use of the second route, which I EXPLICITLY stated when I
EXPLICITLY stated that the language I'm working with has '+' and '0',
my proof is perfectly correct. Yet you disputed that my proof is
correct, even though I EXPLICITLY stated (from the first, a couple of
weeks ago, and repeated ever since) that the language has '+' and '0'.
Will you please show the good sense now just to admit you made a
mistake? It's not so bad to admit, you know.
MoeBlee
> Again, one can define a language by inferring the signature of the
> language from some set of suitable formulas. And one can ALSO define
> a language by stipulating the signature of the language without
> reference to any particular set of formulas. And the second route is
> the more common route, and it is the route that Shoenfield
> describes.
It is also the route that Keisler and Rogers take. So far, we have
seen no published logician who agrees with Nam's convention that the
language must be inferred from the axioms.
--
Jesse F. Hughes
"[I]t's the damndest thing. There's something wrong with every last
one of you, and I *never* thought that was a possibility. But now I
feel it's the only reasonable conclusion." --JSH sees some sorta light
Actually, I was trying to avoid this thread ever since the Google
thousand-post split -- as I already mentioned to Hughes back in
the LV subthread. But as the Nam Nguyen debate continues, it has
become its own welldefined subthread in Google, and so now I
return to post here.
My own opinion of the Nam Nguyen debate at this point? Well:
-- Standard theory supports defining the language first, and then
the axioms.
-- Nguyen supports defining the axioms first and then the language,
and therefore, Nguyen is wrong _according to standard theory_.
(Notice that I have nothing against saying, for example, that a
so-called "crank" who claims that the negation of Cantor's theorem
is provable _in ZFC_ is wrong _about ZFC_. But I consider neither
this hypothetical "crank" nor Nguyen to be absolutely wrong, but
just wrong about the _standard theory_.)
-- I don't know whose side Shoenfield supports, but I'd wager that
Shoenfield supports the standard theory _only because most books
support the standard theory_.
-- But none of this means that there's anything wrong with the way
that Nguyen does it. I believe that defining the axioms first and
then the language can be just as valid as vice versa, even if only
the latter is considered standard.
-- The standard theorists cannot take credit for pushing me out of
the thread, since it was the thousand-post Google problem and not
the standard theorists who convinced me to stop posting in this
thread for a few days.
Good, then I don't wish to distort you.
So, since I can stipulate a language with '+' and '0' as symbols of
the appropriate arities, then I can prove "Axy x+y=0" from "Axy x=y"
as I have given the details several times now.
So, if you don't disagree that I can stipulate such a language, then
it is inexplicable (aside from your mistake about "closure" that you
make later in your proof) why you deny that my proof was correct.
>What I said:
>
> >> Listen. It isn't really that hard to understand why you can't prove,
> >> say, Axy(x+y=0) from the theory T = {Axy(x=y)} (the lone-axiom theory,
> >> so to speak). I've explained to you more than one way, but there's
> >> another simpler way.
But I CAN derive "Axy x+y=0" from the lone non-logical axiom "Axy
x=y".
I SHOWED you exactly how.
AGAIN: I stipulate a language to include '+' and '0', at the
appropriate arities, as symbols. Then I show a sequence of formulas -
each a formula of my stipulated language - such that each formula is
either "Axy x=y" or follows from an inference rule applied to previous
lines and such that the last entry in the sequence is "Axy x+y = 0".
> So, for the millionth time, MoeBlee, I'm not talking about defining
> languages! What I simply stated is basically you can't validly apply
> rules of inference to a formula that's not expressed in the L(T)
> whose signatures are in the axioms of T.
No, it is NOT required that the symbols of the language all occur in
the non-logical axioms of the theory.
Yes, of course, IF the language has only non-logical symbols that
occur in some set of non-logical axioms, then a derivation in that
language can have only those non-logical symbols. I don't think anyone
disagrees with that point, Nam. So IF the language does not have '+'
and '0' as symbols, then, of course, one cannot derive "Axy x+y=0" as
a theorem of a theory whose formulas are all formulas of the language
(that does not have '+' and '0' as symbols). I don't think anyone
disagrees with that, Nam.
But also we can stipulate a language irrespective of having first
stipulated a set of non-logical axioms (as I understand, you say now
that you agree with this). And in THAT situation - say, in which we
stipulate '+' and '0' as non-logical symbols at the appropriate
arities - we can go on to stiplulate "Axy x=y" as a sole non-logical
axiom and then prove "Axy x+y=0". And THAT is the situation I said my
proof pertained to, from the very first proof in which I gave my proof
and I as I reiterated that over and over in subsequent posts.
> If you'd like to spend 100 years defining a trillion extensions of
> L(T), I wouldn't give a hood but neither would I say there's any
> wrong with that.
>
> Do recall I said basically rules of inference operate on formulas
> that are theorems of a specified theory, not on any (extended) languages!
Whatever you mean by that, the fact is that the notion of 'proof' is
ordinarily defined in mathematical logic in a way that once we have a
language, we have certain sequences of formulas of that language that
are sequences that are proofs from some given (possibly empty) set of
formulas of that language. And my proof of "Axy x+y=0" from the set of
formulas {"Axy x=y"} is pefectly a proof (let's not quibble about
LOGICAL axioms vs. natural deduction) given that I stipulated (as I
did, over and over) that the language has '+' and '0' at the
appropriate arities.
> > A first order language is determined by (thus definable by) its
> > symbols and their arities. One may take either route to defining a
> > language: (1) one takes the symbols and arities to be those determined
> > by some set of formulas in which those symbols occur or (2) one
> > simiply stipulates certain symbols and arities. And the second route
> > is common and is as described by Shoenfield and other authors.
>
> > For no good reason, you are just arbitrarily, and contrary even to the
> > textbook of your primary reference, ruling that (2) is disallowed.
>
> Of course *your memory is short here*. In an early response *to you* I
> said that one would be free in stipulating *million different formal
> languages* of one cares to do so:
Then why are your arguing with Jesse about it?!
> >> It's not that difficult actually. I could spend years talking about million
> >> different formal languages - some might be syntactically isomorphic. Yet,
> >> if I don't have any axioms when talking about _formal proof_ all those
> >> million languages are irrelevant. Right? (And the debate here is about proof
> >> of some formula!)
>
> > Otherwise, there is no basis to object to stipulating that a certain
> > language has '+' and '0' as, respectively, a 2-place operation symbol
> > and 0-place operation symbol, then defining a theory in said language
> > to be the set of logical consequences of the sole non-logical axiom
> > "Axy x=y",
>
> So far you've mentioned all the theorems of T = {Axy[x=y]} written in the
> language L(T) that has *zero* nonlogical symbols. OK, that's fine.
NO! That's exactly what I am NOT saying.
The theorems are all the sentences, in the language (which has '+' and
'0'), that are provable from "Axy x=y".
And "Axy x+y=0" is a sentence, in the language (which has '+' and
'0"), that is provable from "Axy x=y".
PLEASE, this is utterly SIMPLE!
> > and then showing a deduction of the formula "Axy x+y=0" of
> > said langauge, as said deduction then does provide that "Axy x+y=0" is
> > in the aforesaid theory.
>
> How on Earth would a theorem of T {Axy[x=y]} has a nonlogical symbol
> while the language of the theory T has zero nonlogical symbol?
Because the LANGUAGE of the theory T DOES have '+' and '0' just as I
STIPULATED:
This is MY context, just as I specified from the beginning a couple of
weeks ago. So, for a moment, please put aside YOUR theory T and
consider MY theory, just as I've said all along:
The language has, by stipulation (which you agreed is okay to do), the
non-logical symbols '+' and '0'.
Then, the theory is the set of all sentences, in said language, that
are entailed by "Axy x=y".
And "Axy x+y='0" is a sentence, in said language, that is entailed by
"Axy x=y".
It is utterly simple, just two points:
(1) "Axy x+y=0" is a sentence of the language, just as I stipulated
the language.
(2) Any model for the language in which "Axy x=y" is true is a model
in which "Axy x+y=0" is true. So "Axy x+y=0" is entailed by "Axy x=y".
And there is a proof of "Axy x+y=0" from the set of formulas {"Axy
x=y"} by the completeness theorem or simply by observing that there is
a sequence of formulas such that all formulas in the sequence are
either "Axy x=y" or derived by an inference rule from previous entries
in the sequence and such that the last formula in the sequence is "Axy
x+y=0".
It's that SIMPLE!
> I'd
> guess you'd "instantiate" that nonlogical symbol through Universal
> Instantiation you mentioned before.
>
> But didn't I *already* refute through 2 or 3 examples? Violation of FOL
> closure property, over generalization, remember?
No! Because '+' and '0' ARE in the language.
MoeBlee
It is the route taken by just about any textbook in the subject I've
seen.
But, if I am not mistaken, now Nam is saying that he recoginzes that
that route is legitimate.
MoeBlee
> On May 2, 12:38 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> "Nam D. Nguyen" <namducngu...@shaw.ca> writes:
>> > I already mentioned to you that's just a manner of speaking (i.e.
>> > writting style). He could have easily defined *fist* a theory as a
>> > set axioms, *then* an axiom as just a formula, and then a formula as
>> > a senctence written in a mathematical language L, and then
>> > *finally*, a language L as consisting of symbols (logical or
>> > otherwise. (This style of definition, which is an antithesis to
>> > your "first" insistence, is wildely used in software language
>> > definitions!)
>> I'm not going around in any more circles with you. It's clear to
>> everyone here that the quotations I've cited are contrary to what you
>> say. In fact, even LWalker has stopped defending you, and that's
>> saying something.
>
> Actually, I was trying to avoid this thread ever since the Google
> thousand-post split -- as I already mentioned to Hughes back in
> the LV subthread.
Quite right, though I forgot this fact.
> My own opinion of the Nam Nguyen debate at this point? Well:
>
> -- Standard theory supports defining the language first, and then
> the axioms.
> -- Nguyen supports defining the axioms first and then the language,
> and therefore, Nguyen is wrong _according to standard theory_.
He is wrong insofar as he claims that this is the predominant
convention, yes.
> -- I don't know whose side Shoenfield supports, but I'd wager that
> Shoenfield supports the standard theory _only because most books
> support the standard theory_.
The quotations I've supplied should leave no doubt. Regarding formal
systems in general, he writes:
"We consider a language to be completely specified when its symbols
and formulas are specified. This makes a language a purely
syntactical object. Of course, most of our languages will have a
meaning (or several meanings); but the meaning is not considered to
be part of the language. We shall designate the language of a formal
system F by L(F)."
"The next part of a formal system consists of its /axioms/. Our
only requirement on these is that each axiom shall be a formula of
the language of the formal system." [p. 4 in my copy of Shoenfield]
Regarding first-order theories in particular, he writes:
A /first-order theory/, or simply a /theory/, is a formal system
T such that
i) the language of T is a first-order language;
ii) the axioms of T are the logical axioms of L(T) and certain
further axioms, called the /nonlogical axioms/;
iii) the rules of T are the expansion rule, the contraction rule,
the associative rule, the cut rule and the E-introduction rule.
In order to specify a theory, we have only to specify its
nonlogical symbols and its nonlogical axioms; everything else is
given by the definition of a theory. Note also that the logical
axioms and the rules are determined as soon as the language is
chosen; they are independent of the nonlogical axioms.
As we can see (putting the two definitions together), the language
L(T) is the language of the formal system T and there is no
requirement that each non-logical symbol of L(T) appears in the axioms
of T. On the contrary, there is only one relevant requirement: that
every axiom of T be a formula in L(T). Shoenfield is quite explicit
on this point.
> -- But none of this means that there's anything wrong with the way
> that Nguyen does it. I believe that defining the axioms first and
> then the language can be just as valid as vice versa, even if only
> the latter is considered standard.
I never said that Nam's proposal is "wrong". I've only said that it
is not the conventional presentation. *He's* the one who's claimed
that his proposal is the only sensible definition of theory, as far as
I can tell.
> -- The standard theorists cannot take credit for pushing me out of
> the thread, since it was the thousand-post Google problem and not
> the standard theorists who convinced me to stop posting in this
> thread for a few days.
I'm sure I never took credit for that. I only drew the (mistaken)
conclusion that since you had fallen silent, we may infer that you
disagree with Nam. After all, you've said that you will not publicly
claim Nam is wrong when others are already doing so.
But thanks for the clarification. Seems to me that you agree with me
wholeheartedly.
--
"This sucks," said a Pennsylvania State University student [...] " Why
can't the college let me do what I want to do with my computer? The
school computer security guys are being way more annoying than the
spyware was." -- A student pines for his disabled spyware
> -- Standard theory supports defining the language first, and then
> the axioms.
> -- Nguyen supports defining the axioms first and then the language,
> and therefore, Nguyen is wrong _according to standard theory_.
Let's be clear. In ordinary mathematical logic, it is NOT disallowed
to define a language by inferring a signature from a given set of
sequenes of symbols such that each sequence forms a formula of some
language or another and there is no conflict with the symbols (as, if
I am not mistaken, unique readability will determine the symbol kind
and arity just from the formula itself).
As to Nam on the particular point of first stipulating a language, he
has recently been saying he does not disallow this, so I don't opine
on your call that he's wrong on this particular point.
> (Notice that I have nothing against saying, for example, that a
> so-called "crank" who claims that the negation of Cantor's theorem
> is provable _in ZFC_ is wrong _about ZFC_. But I consider neither
> this hypothetical "crank" nor Nguyen to be absolutely wrong, but
> just wrong about the _standard theory_.)
But Nam purports to be speaking on BEHALF of ordinary mathematical
logic. Nam is saying that WE are incorrect about ordinary mathematical
logic while HE is correct about ordinary mathematical logic (as it is
conveyed in such textbooks as Shoenfield's).
> -- I don't know whose side Shoenfield supports, but I'd wager that
> Shoenfield supports the standard theory _only because most books
> support the standard theory_.
> -- But none of this means that there's anything wrong with the way
> that Nguyen does it.
What is wrong is Nam's claim that his evaluation is in accord with
ordinary mathematical logic and that, for example, my proof of "Axy x
+y=0" is not in accord with ordinary mathematical logic.
> I believe that defining the axioms first and
> then the language can be just as valid as vice versa, even if only
> the latter is considered standard.
NO! I've posted over and over and over that ordinary mathematical
logic does NOT disallow extracting a language from some already given
set of formulas.
But, if you ACTUALLY STUDIED the mathematical logic involved here,
you'd see that the route of first stipulating a language is much more
straightforward, not nearly as convoluted, as extracing from a given
set of formulas.
Moreover, the raw notion of a language stipulated by giving a
signature would seem to need to be already in place before one could
THEN speak about some set of formulas from which to extract a
signature for a language, since the notion of 'formula' itself is in
regards to the previously defined notion of a language which in turn
reverts to the notion of symbols of certain kinds and arities.
MoeBlee
>> So, for the millionth time, MoeBlee, I'm not talking about defining
>> languages! What I simply stated is basically you can't validly apply
>> rules of inference to a formula that's not expressed in the L(T)
>> whose signatures are in the axioms of T.
[...]
> But also we can stipulate a language irrespective of having first
> stipulated a set of non-logical axioms (as I understand, you say now
> that you agree with this). And in THAT situation - say, in which we
> stipulate '+' and '0' as non-logical symbols at the appropriate
> arities - we can go on to stiplulate "Axy x=y" as a sole non-logical
> axiom and then prove "Axy x+y=0". And THAT is the situation I said my
> proof pertained to, from the very first proof in which I gave my proof
> and I as I reiterated that over and over in subsequent posts.
Careful! I don't think he agrees.
I think he's saying that we can define millions of different languages
for T, but rules of inference must only apply to the minimal language
L(T). Read again the excerpt he wrote above.
--
Jesse F. Hughes
"[M]eta-goedelisation as the essence of the globalised dictatorship by
denial of sense." -- Ludovico Van makes some sort of point.
Take a look at:
http://biblioteca.universia.net/irARecurso.do?page=http%3A%2F%2Fprojecteuclid.org%2Feuclid.jsl%2F1183733109&id=37468802
and you will find the answer to all your inquires.
Jhonas
But I didn't opine as to his view of rules of inference. I meant only
that he seems to agree that a language can be defined before
specifiying any particular theory that uses that language. (And IFhe
says that is not something he agrees with, then I leave for him to say
for himself what EXACTLY he means).
As to rules of inference, that matter is subsumed in other of my
remarks. But to put the matter directly here: In ordinary context of
mathematical logic, the rules of inference generalize over formulas of
the language - and it is my very point that where '+' and '0' are in
the language, the rules of inference allow instantiations to formulas
that have those symbols EVEN THOUGH those symbols do not occur in any
of the non-logical axioms for some particular axiomatization of some
particular theory.
As we surely agree, there is no ordinary convention that the rules of
inference pertain only to formulas with only symbols mentioned in some
non-logical set of axioms. If Nam disputes that, then he's just wrong.
MoeBlee
I don't believe I've ever seen the first method, which just seems
completely backassward.
> lwa...@lausd.net writes: [bla bla bla]
>
> [bla bla bla]
>
Still eager to "debate" with cranks?
Herb
> I don't believe I've ever seen the first method, which just seems
> completely backassward.
But my point is not to claim that it is used in any particular place,
but rather that it is not disallowed. That is, if I am not mistaken,
given that the logical symbols are fixed, unique readability should
allow us to infer what are the kinds and arities of any non-logical
symbols that occur in a set of sequences of symbols such that said
sequences don't clash as to kind and arity of symbols in them and then
that said sequences are formulas in any language that includes the
just mentioned non-logical symbols.
For example, if the set of formulas is:
{"Ax x=0", "Axy +xy=+yx"}
then we can infer that '0' is a 0-place operation symbol and '+' is a
2-place operation symbol and then define that language that has '0', a
0-place operation symbol, and '+', a 2-place operation symbol, as the
only non-logical symbols.
MoeBlee
> Moreover, the raw notion of a language stipulated by
> giving a signature would seem to need to be already
> in place before one could THEN speak about some set
> of formulas from which to extract a signature for a
> language, since the notion of 'formula' itself is in
> regards to the previously defined notion of a
> language which in turn reverts to the notion of
> symbols of certain kinds and arities.
I have a question about this "axioms first, language after"
procedure. If one defines one's system in this fashion,
how would one go about showing that the axioms and other
formulas can be unambiguously parsed?
If one defines one's system "language first, axioms after"
then, of course, one has a clear description of the
syntax to work with. The other way, I suppose you
have to draw analogies with well-known systems. This
is why we assumed '0' was a constant (or 0-ary function?)
and '+' was a 2-ary function.
However, if I recall correctly, Nam claimed at one point
that "x + y = 0" was not well formed in his system,
to the surprise, it seemed, of everyone except Nam.
It probably wasn't Nam's intent there, but his rejoinder
served as perfect illustration of why, for reasons
of clarity and unambiguity, one might avoid defining
a system "axioms first, language after".
Jim Burns
If I'm not mistaken, given certain conditions that I mentioned, we are
assured of unambiguous parsing by the unique readability theorems. A
few technical details might need to be massaged, but I don't imagine
any huge obstacles. See my post today to Chris Menzel in this regard.
> If one defines one's system "language first, axioms after"
> then, of course, one has a clear description of the
> syntax to work with. The other way, I suppose you
> have to draw analogies with well-known systems. This
> is why we assumed '0' was a constant (or 0-ary function?)
> and '+' was a 2-ary function.
I don't think we need analogies.
My remarks here are to be understood in context of first order
predicate languages:
I am supposing that we given what the logical symbols are (the
quantifier, connectives, and individual variables) are of any first
order language (i.e., that all first order languages share the exact
same quantifiers, connectives, and individual variables). So, with the
logical symbols given, each language is uniquely determined by its
signature (its non-logical symbols and their kind (predicate symbol or
operation symbol) and their arities). Then if we have a set of
sequences, then there is the set of entries of sequences that are not
logical symbols. If each of the members of that set is used only as a
certain kind of symbol at a certain arity, then, by unique
readability, its kind and arity is determined. Then we take the
signature of our language to be those non-logical symbols that are
entries in at least one sequence in our set of sequences.
Note: It is not required that the definition of our language by the
above method be EFFECTIVE (i.e., that there is an algorithm to
determine the kind and arity of each non-logical symbol), but rather
only that the kind and arity is DETERMINED (even if we may not be able
to calculate that determination). On the other hand, for EFFECTIVIZED
languages, of course, yes, we do require that it is calculable what
kind and arity each non-logical symbol is.
MoeBlee
As a reminder, and as a fairly obscure point, in the
particular case of proving "x+y=0" from "x=y", all
that is necessary, assuming the usual meaning of "=",
is that "x+y" and "0" be terms.
Marshall
On April 16 (!) I wrote (quote):
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
First of all we have to consider the syntactic part of the calculus [i.e.
system].
To make a long story short:
variables: x, y, z, x', y', z', ...
arbitrary names: a, b, c, a', b', c', ...
constants: 0.
[Def. of terms:]
| Any arbitrary names or constant is a term.
| If t and s are terms, then (t + s) is a term.
etc. etc.
Rule: A-Elim:
AvPhi(v)
--------
Phi(t)
where v is a variable and t a (any) term.
This justifies the following step in a proof:
:
AxAy(x = y)
Ay((a + b) = y)
:
Moreover it allows for the move:
:
Ay((a + b) = y)
(a + b) = 0
:
etc. etc.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that in this system (of natural deduction due to Gentzen/Lemmon) there
are no free variables, but "abitrary names" ("parameters").
Herb
P.S. It seems to me that Nam is a complete moron.
> If I'm not mistaken, given certain conditions that I mentioned, we are
> assured of unambiguous parsing by the unique readability theorems.
Looking at this in more detail I see that we do need to impose some
extra conditions I didn't mention.
For example, suppose we are given that 'x' is a variable (which will
be the case since we are given the logical symbols as invariant over
all first order languages), then consider:
Fgx
That could be read as 'F' being 1-place and 'g' being 1-place. Or it
could be read as 'F' being 2-place and 'g' being 0-place.
So a couple of possible remedies might be to require that we have a
"master list" of the arities of all possible predicate symbols. Then,
we need to prove that the arity of any operation symbol in a formula
is determined by the arities of the predicate symbols.
Another solution might be to forgo Polish notation for terms and use
parentheses. In that case
Fgx would read as 'F' being 2-place and 'g' being 0-place
while
Fg(x) would read as 'F' being 1-place and 'g' being 1-place.
MoeBlee
I'm still trying to find out a way to settle the long
Nam Nguyen debate here.
Back before the thousand-post Google split, Marshall
mentioned a computer program called "Prover9." But later
on, MoeBlee mentioned Prover9 in another thread -- I
forget whether that thread is also an offshoot of the
Google split thread as well. MoeBlee's reference to
Prover9 reminded me of Marshall's use of the program.
Now IIRC, Marshall said that he inputted a single axiom
Ax (x=y) (or whatever the correct Prover9 syntax is) and
the theorem to be proved, Ax (x+y=0). Then the output
was a proof of the theorem Ax (x+y=0) in the theory
whose single axiom was "Ax (x=y)".
So here are some questions that I have about this. Note
that I only expect Marshall, MoeBlee, or anyone else who
has access to Prover9 to answer these questions.
1. The cornerstone of the standard theorists' argument
is that one must state a language L first, then state a
set of axioms in the language L. But when, if ever, does
one input the language L into _Prover9_? How does
_Prover9_ know to prove statements mentioning nonlogical
symbols not mentioned in the axioms?
2. Along this same line of thought, suppose I were to
input "Ax (x=y)" as the lone axiom again, but ask it to
prove Ax (x...y=0) instead? Notice that I asked about
Ax (x...y=0) before, but this time I specifically ask
about Ax (x...y=0) in the context of _Prover9_. I want
to know what _Prover9_ would output if asked to prove
the statement Ax (x...y=0).
3. And if Prover9 would prove Ax (x+y=0) but not
Ax (x...y=0), what's the difference between the former
and the latter, from Prover9's perspective? Perhaps
Prover9 won't accept statements with ellipses as
wellformed formulas -- which implies that there really
is a language L built into the program, and L is
determined by Prover9's _syntax_.
Of course, I lack access to Prover9 for the exact same
reason that I lack access to Shoenfield -- I doubt
that I could afford either one.
But the main target of Marshall and MoeBlee's argument
is _Nguyen_, not I. Even if I had Prover9 and could
see the proof of "Ax (x+y=0)," that still wouldn't
convince _Nguyen_ of anything. And surely _Nguyen_
would be able to afford Prover9, since I can't see
Prover9 being more expensive than Shoenfield, which
Nguyen evidently can afford and does own.
And so, I wonder whether Prover9 will be able to
settle the Nguyen debate once and for all.
> MoeBlee mentioned Prover9 in another thread
No, someone mentioned it to me.
> 1. The cornerstone of the standard theorists' argument
> is that one must state a language L first, then state a
> set of axioms in the language L.
NO! I've told you about four times already that the argument does not
depend on such a stipulation! Are you not even bothering to read?
Please just reread the posts so that I don't have to explain this YET
AGAIN.
Hint: Change the word 'must' in your above sentence to 'may'.
> And so, I wonder whether Prover9 will be able to
> settle the Nguyen debate once and for all.
What has ALREADY settled the debate is just looking at any number of
textbooks in mathematical logic, including Shoenfield (which is at
least one textbook that it seems Nam himself endorses as
authoritative).
If you wish to UNDERSTAND mathematical logic, then I'm afraid you'll
need to actually read a textbook, whether by purchase or by borrowing
one from a library, notwithstanding that that is so anathema to you.
MoeBlee
No, it is not. What the hell is wrong with your reading comprehension?
OK, then. I'll read the post of Chris Menzel from nearly 24
hours ago:
Menzel yesterday:
"I don't believe I've ever seen the first method [Nguyen's
method], which just seems completely backassward."
> Hint: Change the word 'must' in your above sentence to 'may'.
I disagree. I stand by the word "must" as being more
representative of the opinion of at least one standard
theorist, Menzel. The language L _must_ be defined first,
because anything else is completely "back@$$ward."
The following is why I disagree with Menzel.
Let me come up with a theory of geometry. Since Menzel
insists that we define the language first, the language
will consist of the words "point," "line," "plane,"
"between," "contains," and "congruent" -- in other words
the language of Euclid-Hilbert geometry -- plus one
additional word, "thingamajig."
Now that we have our language, only now may we define
our axioms, according to Menzel at least. So let me
state the axioms as being all of, and only, the axioms
of Euclid-Hilbert geometry. So in particular, no axiom
mentions this new word, "thingamajig."
Now we consider the theory itself, the set of statements
that are provable in this theory. Now surely none of
these proved statements can contain the new word
"thingamajig," can they? Indeed, we don't even know
whether a thingamajig can even exist or not! In fact, I
can't see how there can even be any wellformed statement
that mentions the word "thingamajig." Thus, the theory
seems to prove nothing substantive about thinagamajigs!
Primitives are undefined, but the axioms which mention
the primitive characterize the primitive. The words
"point" and "line" are undefined, so we can't really
know what a point is and what a line is. But then we
have the axiom:
"Two distinct points A and B always completely determine
a straight line a."
So whatever a "point" is, and whatever a "line" is, the
latter contains two of the former. Now try saying
something similar regarding "thingamajigs."
Notice that the primitive "between" is said by Hilbert
to only describe points, "congruent" only describes
segments and angles, and "contains" only describes
points, lines, and planes. None of them can be used to
describe "thingamajigs." Thus:
"Every thingamajig is congruent to itself."
is not a wellformed statement.
Since no theorem mentions the word "thingamajig," we
wonder how "thingamajig" can even be considered part of
the language of the theory. But we already _defined_
the language to contain the word "thingamajig," and so
it's too late to change the language. We can't go back
and say that "thingamajig" isn't in the language, since
doing so would be "back@$$wards" according to Menzel.
This is why I disagree with Menzel. If a theory can't
prove anything substantive about a word, then we have
no business including that word in the language.
According to Chris Menzel, not doing so "just seems
completely backassward."
So maybe it would be more accurate to say:
The cornerstone of the the standard theorist Chris
Menzel's argument is that one either states a language
L first, then state a set of axioms in the language L,
or do an alternate that seems completely back@$$ward.
(1) He didn't say that it is IMPOSSIBLE. And he didn't object to my
response to him on that point (though, of course, he may have
objections that he hasn't posted). (2) Chris is not the only one in
that argument. At least one other player on that stage was me, and I
was excruiating clear to allow that one may determine a language from
a set of axioms (allowing for certain techical details to be ironed
out).
Moreover, my main point is that the argument against Nam does not
DEPEND (as I wrote in my previous post) on any view that one MUST
define a language first and not determine a language from a set of
axioms. Rather the argument only depends on allowing that one MAY
define a language first. And since, ORDINARILY, and even as Shoenfield
described, we do define a language first, just as the sequences of
definitions of such things as 'language' in mathematical logic
actually runs, PERFORCE we MAY define a language first, whether or
not, and regardless of any opinion Chris or I or anyone has about the
business of extracting a language from a set of axioms.
GOT IT NOW?
> > Hint: Change the word 'must' in your above sentence to 'may'.
>
> I disagree. I stand by the word "must" as being more
> representative of the opinion of at least one standard
> theorist, Menzel. The language L _must_ be defined first,
> because anything else is completely "back@$$ward."
I don't speak for Menzel, but as his post stands, I take "backassward"
as refering to HEURISTICS. He did not, at least in that remark,
completely RULE OUT that one may take a backassward approach if one
chooses to do so. (Of course, only Chris can say, and it is possible
that he might have meant RULING OUT, even in context of my defense of
NOT ruling out.)
Moreover, Chris is just one poster and does not in himself constitute
a consensus of the people arguing with Nam, in particular, as I stated
over and over, MY view does NOT rule out determining a language from a
set of axioms (as long as some technical details are ironed out).
> The following is why I disagree with Menzel.
>
> Let me come up with a theory of geometry. Since Menzel
> insists that we define the language first,
I don't see that he TRULY "INSISTED".
I can say, "I've never heard of a person first TYPING a letter then
writing it out in pencil on a piece of scrap paper. That seems
backassward to me." But that doesn't entail that I rule out that it is
possible to do.
> the language
> will consist of the words "point," "line," "plane,"
> "between," "contains," and "congruent" -- in other words
> the language of Euclid-Hilbert geometry -- plus one
> additional word, "thingamajig."
>
> Now that we have our language, only now may we define
> our axioms, according to Menzel at least. So let me
> state the axioms as being all of, and only, the axioms
> of Euclid-Hilbert geometry. So in particular, no axiom
> mentions this new word, "thingamajig."
>
> Now we consider the theory itself, the set of statements
> that are provable in this theory. Now surely none of
> these proved statements can contain the new word
> "thingamajig," can they?
YES THEY CAN! This has been explained over and over and over. Please
just read the posts!
> Primitives are undefined, but the axioms which mention
> the primitive characterize the primitive. The words
> "point" and "line" are undefined, so we can't really
> know what a point is and what a line is. But then we
> have the axiom:
>
> "Two distinct points A and B always completely determine
> a straight line a."
>
> So whatever a "point" is, and whatever a "line" is, the
> latter contains two of the former. Now try saying
> something similar regarding "thingamajigs."
WHATEVER a thingamajig is, for example, this is a theorem of your
theory:
Ax(x is a thingamajig -> x is a thingamajig)
That theorem is a member of the theory you've described. It is a
formula in the language of the theory and is derivable from the empty
set of non-logical axioms, so PERFORCE, it is derivable from the set
of non-logical axioms of your theory.
PLEASE inform yourself with a good book! Or even just read the
previous posts!
> Since no theorem mentions the word "thingamajig,"
No, the predicate symbol 'thingamjig' (or as 'thingamajig' is regarded
as a nickname for a predicate symbol, if we are to be so pedantic)
ocurs in INFINITELY many theorems in your theory!
> we
> wonder how "thingamajig" can even be considered part of
> the language of the theory.
NO, we DON'T wonder any such thing. It's part of the language because
we (or you, whatever) DEFINED the language to be one such that
'thingamjig' is of the language.
> But we already _defined_
> the language to contain the word "thingamajig," and so
> it's too late to change the language. We can't go back
> and say that "thingamajig" isn't in the language,
Right.
> since
> doing so would be "back@$$wards" according to Menzel.
That wasn't even Chris's point about backasswardness! You've
TRANSPLANTED his point, which was about a DIFFERENT matter!
> This is why I disagree with Menzel. If a theory can't
> prove anything substantive about a word, then we have
> no business including that word in the language.
Then that's your PERSONAL OPINION about how it SHOULD be. But in fact
that is NOT how it is in ordinary mathematical logic. Sure, you're
entitled (barely though, since you're such an ignoramus on the
subject) to advocate that we define things differently in mathematical
logic. But that was not what was at stake in our conversation with
Nam. Rather, we were talking about how things are in fact presently
defined in ordinary mathematical logic.
MoeBlee
No, that is NOT the "cornerstone" of the argument. See my previous
post.
MoeBlee
Pretty clearly it isn't (properly done).
> And he didn't object to my response to him on that point (though, of
> course, he may have objections that he hasn't posted).
Nope.
>> > Hint: Change the word 'must' in your above sentence to 'may'.
>>
>> I disagree. I stand by the word "must" as being more representative
>> of the opinion of at least one standard theorist, Menzel. The
>> language L _must_ be defined first, because anything else is
>> completely "back@$$ward."
>
> I don't speak for Menzel, but as his post stands, I take "backassward"
> as refering to HEURISTICS.
Better, perhaps: presentation.
No. Chriz Menzel is simply passing comment, not making an argument.
Your attempts to characterize the arguments in this subthread are
bizarrely mistaken. Try reading it again without assuming that one
side must be composed of "standard theorist" zealots trying to supress
anything non-standard.
> Pretty clearly it isn't (properly done).
> Nope.
> Better, perhaps: presentation.
Thanks. I'm glad I didn't misunderstand you.
MoeBlee
If by "system" you meant a logic framework system, then
that's not what I had meant. (I always talk in the context
of FOL= system). Otoh, if you meant "formal system" then
of course "x+y=0" is not well-formed in the L(T) that
has zero nonlogical symbol (where T = {Axy[x=y]}.
I think in fact this L(T) is call the language of FOL;
and "x+y=0" isn't a wff in this language. Hence it's
not provable in this T.
> It probably wasn't Nam's intent there,
It's my intent all right to say to MoeBlee, Jesse, and others
that "x+y=0" is simply *not provable in this T*, in accordance
to *syntactical* provability *in FOL=*.
> but his rejoinder
> served as perfect illustration of why, for reasons
> of clarity and unambiguity, one might avoid defining
> a system "axioms first, language after".
Two issues.
First, it's far from being a "perfect illustration of why, for reasons
of clarity and unambiguity". Many times people do think of operations,
models first before even specifying any (non-logical) symbol at all,
to *symbolize* the operations, models. The more complex a targeted
domain of abstraction is, the more difficult one would find to come up
with a balanced number of nonlogical symbols, representing the concepts
in the domain. For instance, we might know well enough many biological
processes and relations such as DNA replication, heredity, protein synthesis,
... But that doesn't mean it's that readily available to our mind what kind
of nonlogical symbols or how many of them we must have to cohesively
formalize/symbolize these biological concepts.
Secondly, all this "axioms first, language after" that I'm purported
to try to "enforce" in FOL reasoning is a) untrue and b) quite irrelevant.
My opponent just exaggerated it to the point of ridiculousness (such
as "backassward"!).
It's untrue because *many times* in the thread I already said one is
*free to stipulate* as many languages as one could, meaning that even one
doesn't contemplate on creating any formal system at all (hence no axioms
would ever need to be written) one could perfectly stipulate a million
language if one would like. I don't understand why people couldn't come
to grasp such a simple and repeatedly-said notion!
It's irrelevant because the central issue here is actually not about
whether or not any human stipulate language or axioms - first or last!
The is issue here is whether or not certain "peculiar" Rules, such as
A-Instantiation or Expansion, would *permit* an *introduction* of
nonlogical symbols - beyond those found in the axioms of a theory
(i.e. beyond the minimum set of nonlogical symbols for this axiom-set
theory). If those rules permit that (which I've been defending that
they don't!), then not only the language that we all would agree to
stipulate, but countably infinite nonlogical symbols would be *validly*
_introduced_ into a language - whether or not we'd care to desire or
stipulate. Otoh, if those rules don't permit (which my opponents have
been defending that they do!), then it's immaterial whether or not
any stipulate anything language first or last, the Rules would tersely
look at the *underlying* axioms to discern the minimal language from
there and any symbol appearing in the hypothesis or conclusion would
be in that language L(T= {axioms}). No "foreign" symbols would be permitted.
Period.
All of course within the context of formal (i.e. syntactical or symbolical)
proofs in good old FOL=, which doesn't require a new concept such as proof
*in a language" as the other poster has tried to introduced into the debate.
I meant "*uncountably* infinite"
Correct. Naturally, a FOL language *can be* defined well in advanced of
any theory - theory which may or may *not* use any non-logical symbol
at all in that language!
>
> As to rules of inference, that matter is subsumed in other of my
> remarks.
It's my "right" as a poster that I stay confined within the context
of syntactical/symbolical proof in axiom-set systems of FOL=, when
talking about valid application of rules of inference. (Recall that
very early in the debate, I mentioned *to you*:
> Of course. (And I usually assume FOL=).
and, iirc, you acknowledged that.
So, MoeBlee, for what it's worth, I'm carrying my defending in this
debate in the manner of one-issue-one-logic-framework-at-a-time.
Any thing else like "proof-in-a-language" or "equational logic"
is irrelevant and I'd only engage in a new thread (or sub-thread),
if I have time or interest.
> But to put the matter directly here: In ordinary context of
> mathematical logic,
If by "ordinary context of mathematical logic" you mean the context
of FOL= syntactical proofs *in formal systems*, then I already gave
examples explaining what you said below is invalid.
> the rules of inference generalize over formulas of
> the language - and it is my very point that where '+' and '0' are in
> the language, the rules of inference allow instantiations to formulas
> that have those symbols EVEN THOUGH those symbols do not occur in any
> of the non-logical axioms for some particular axiomatization of some
> particular theory.
Again, as far as FOL= syntactical proofs *in a formal system* T is concerned,
Rules of inference can *not* allow such generalization ("instantiation",
"expansion", or the like) without committing to the error of over-generalization,
from specific hypothesis/information to general conclusion, as I gave in one
example before.
>
> As we surely agree, there is no ordinary convention that the rules of
> inference pertain only to formulas with only symbols mentioned in some
> non-logical set of axioms. If Nam disputes that, then he's just wrong.
In so far as you and others have not been able to refute my specific examples
at all (other than saying something like "Shoenfield, Roger, etc... didn't
say that", or invoking off-the-topic non-FOL= logic frameworks) then
I'm correct and you and other opponents of mine are *not*.
Also you (MoeBlee) should have realized that as far as FOL= *proof in a theory*
is concerned, *rules of inference don't "pertain" to just _any_ formula*!
Specifically, rules of inference pertain *only* to formulas that are
*theorems*. But since theorems are defined from axioms, it isn't much
an exaggeration to say rules of inference pertains to *axioms*. [And that's
not just (in your words) "ordinary convention" but it's the very heart of the
definition of proofs - in FOL=].
So you and others are not *just* disputing with me: you're disputing the
very fundamental notion of syntactical proofs in FOL=.
> Nam Nguyen wrote:
> > MoeBlee wrote:
> >>
> >> As we surely agree, there is no ordinary convention that the rules of
> >> inference pertain only to formulas with only symbols mentioned in some
> >> non-logical set of axioms. If Nam disputes that, then he's just wrong.
> > In so far as you and others have not been able to refute my specific
> > examples
> > at all (other than saying something like "Shoenfield, Roger, etc... didn't
> > say that", or invoking off-the-topic non-FOL= logic frameworks) then
> > I'm correct and you and other opponents of mine are *not*.
>
> Also you (MoeBlee) should have realized that as far as FOL= *proof in a theory*
> is concerned, *rules of inference don't "pertain" to just _any_ formula*!
They pertain to any formula in the language being considered;
the choice of language is not always made explicit, but simply saying
you are using FOL= as a framework is not enough; to be precise,
the language has to be made explicit as well.
> Specifically, rules of inference pertain *only* to formulas that are
> *theorems*. But since theorems are defined from axioms, it isn't much
> an exaggeration to say rules of inference pertains to *axioms*. [And that's
> not just (in your words) "ordinary convention" but it's the very heart of the
> definition of proofs - in FOL=].
>
> So you and others are not *just* disputing with me: you're disputing the
> very fundamental notion of syntactical proofs in FOL=.
Absolutely not, and you have already seen examples.
Perhaps the best example comes when there are *no* (non-logical) axioms at all.
Logic text books are full of examples asking students to show that
certain statements are theorems of FOL=, with *no* axioms.
(the language is implicitly or explicitly assumed to be such that
the formla in question is well formed). e.g., if "wotsit" is a
1-place predicate, then
(all x. not wotsit(x)) -> not (some y wotsit(y))
is provable in whatever system of FOL you want, from no
non-logical axioms.
You seem to be saying that without non-logical axioms, *nothing*
is provable in FOL= -- that's just no so.
< ==
> "To discover the proper approach to mathematical logic,
> we must therefore examine the methods of the mathematician."
> (Shoenfield, "Mathematical Logic")
--
Alan Smaill
Like I explained before, to any *theorem*-formulas, *not just* any formulas
you considered. For instance, let L = L(T = {Ax[Steel(x)]} then
Ex[Steel(x)] is "pertained" by rule(s) of inference. On the other hand, e.g.,
as much as you'd like to "consider" F = Ex[Wood(s)] as *any formula*,
F is simply *not* pertained by the rule(s) as a theorem of this T.
You're simply wrong here.
> the choice of language is not always made explicit, but simply saying
> you are using FOL= as a framework is not enough; to be precise,
> the language has to be made explicit as well.
>
>> Specifically, rules of inference pertain *only* to formulas that are
>> *theorems*. But since theorems are defined from axioms, it isn't much
>> an exaggeration to say rules of inference pertains to *axioms*. [And that's
>> not just (in your words) "ordinary convention" but it's the very heart of the
>> definition of proofs - in FOL=].
>>
>> So you and others are not *just* disputing with me: you're disputing the
>> very fundamental notion of syntactical proofs in FOL=.
>
> Absolutely not, and you have already seen examples.
What (countered) examples? What you incorrectly stated above, or your
incorrect example below?
>
> Perhaps the best example comes when there are *no* (non-logical) axioms at all.
> Logic text books are full of examples asking students to show that
> certain statements are theorems of FOL=, with *no* axioms.
> (the language is implicitly or explicitly assumed to be such that
> the formla in question is well formed). e.g., if "wotsit" is a
> 1-place predicate, then
>
> (all x. not wotsit(x)) -> not (some y wotsit(y))
>
> is provable in whatever system of FOL you want, from no
> non-logical axioms.
Is "wotsit" a logical symbol *to you*? I'm sure the answer would be "No".
Just that alone, your example is incorrect.
>
> You seem to be saying that without non-logical axioms, *nothing*
> is provable in FOL= -- that's just no so.
Let L1 = L(T1 = {Axy[x=y]}). From L1, you could have another theory
T2 = {Exy[~(x=y)]}. From T1, you could prove Exy[x=y]; and from T2
prove (Exy[~(x=y)] \/ Axy[x=y]). And in any theory if you could prove
one theorems you could prove *infinite* number of theorems.
Hope *your misunderstanding* would go away now.
--
Not that Alan can't answer for himself, but I can't make any sense of
the preceding paragraph. In standard first-order logic, rules of
inference apply (i.e., pertain) to every formula of the language. For
instance, the rule of Modus Ponens is that, for *any* formulas A and B,
given A and (A -> B), you may infer B. Are you denying this? If so,
you're simply wrong here.
Sometimes propositional logic is presented as a Hilbert-style
axiomatic system, in which all the theorems are tautologies,
and with two rules of inference, Modus Ponens and Universal
Substitution. Modus Ponens, as you say, is a valid inferential
rule for any formulas A and (A -> B), but Universal Substitution
(where any wff may be substituted for a variable at every occurance
of that variable in a wff) is only a valid inference rule when applied
to tautologies, i.e. only when applied to theorems of the calculus.
I think that Nam is thinking of some sort of similar substitution
rule above, where Wood(x) is substituted for Steel(x). Or something.
Some inference rules are valid only relative to some particular
deductive system. At first-order, any validity (phi -> psi) can
be pressed into service as an inference rule applicable to any
formula of the form of phi, and in fact this happens quite a bit,
though somewhat disguised in the various implementations of FOL.
This sort of deduction is a very natural thing to do; I think
it's the basic intuition behind some "natural deduction" systems
which have no axioms at all, just inference rules.
--
hz
With due respect, no. Rules of inference are specific for theorems of
of a formal system. If we use the rules for something else (which I suppose
we could) then we're *not* talking about syntactical proofs in FOL (as
I've cautioned before). Let me review with you what Shoenfield stated:
"We need the third part of a formal system which will enable us to conclude
theorems from the axioms. This is provided by the *rules of inference*,
which we often call simply *rules*. Each rule of inference states that
under certain conditions, one formula, called the *conclusion* of the
rule, can be *inferred* from certain formulas, called the *hypotheses*
of the rule.
How should we define the *theorems* of a formal system F? Obviously they
should satisfy the two laws:
i) the axioms of F are theorems of F;
ii) if all the hypotheses of a rule of F are theorems of F, then the
conclusion of the rule is a theorem of F.
Moreover, we want a formula to be a theorem of F only if it follows
from these laws that it is a theorem. We can therefore define a theorem
of F to be a formula of F which can be seen to be a theorem on the basis
of laws (i) and (ii)."
From his passage, we could see clearly if we talk about rules of inference
in the context of FOL proofs in a formal system (in which is, again, the
context of my argument), then the rules can't be applied to just any formula.
If any formula that is applicable to be "pertained" by a rule of inference
(whether as a hypothesis or a conclusion) *it must be at least an axiom*:
which means it can't be just any formula, as you've alluded to above.
[Note in law (ii) the phrase "rule of F": he clearly meant the rule that's
being applied on the hypotheses of F, which clearly doesn't mean *any* formula.
In addition, we could easily see from his passage that rules of inference
can't be applied to *any* formula without violating the definition of
syntactical proof in FOL. For example, let L = L(T = {Ax[Sx=e]}. Now,
by Expansion Rule, we'd have:
(1) Ax[Sx=e] \/ ~(Ex[Sx=e])
By the essence of what you've alluded above (and Allan, et al, said before),
if we just stipulate an extension of L which is, say, L' = L(e,e',S), then
we could have this theorem:
(1') Ax[Sx=e] \/ ~(Ex[Sx=e'])
then given the very same condition - same hypothesis - Ax[Sx=e], we could
derive 2 *different conclusions*, a clear violation of what Shoenfield stated
above:
"under certain conditions, _one formula_, called the *conclusion* of
the rule, can be *inferred* from ... the *hypotheses* of _the_ rule."
***
In addition, as I've alluded to in previous posts, if we permit the
existence a nonlogical symbol *foreign* to the underlying (T = {Ax[Sx=e]},
such as say "e'", then we'd open a floodgate to the entire existences
of all the elements of say a (non-empty) Grothendieck universe (whose size
would probably be more that just uncountable), to be in theorems of T!
One could demonstrate that I'm wrong here; but from what I've gathered,
that's not what FOL or FOL's syntactical proof is about.
So, one is far from proving I'm wrong here using your argument.
Neither can I.
> > In standard first-order logic, rules of
> > inference apply (i.e., pertain) to every formula of the language. For
> > instance, the rule of Modus Ponens is that, for *any* formulas A and B,
> > given A and (A -> B), you may infer B. Are you denying this? If so,
> > you're simply wrong here.
>
> With due respect, no. Rules of inference are specific for theorems of
> of a formal system.
well, they pertain to formulas of a formal system, if that's what you
mean -- I suspect that's not what you mean, but it's what the rest of
the logical world means.
> If we use the rules for something else (which I suppose
> we could) then we're *not* talking about syntactical proofs in FOL (as
> I've cautioned before). Let me review with you what Shoenfield stated:
>
> "We need the third part of a formal system which will enable us to conclude
> theorems from the axioms. This is provided by the *rules of inference*,
> which we often call simply *rules*. Each rule of inference states that
> under certain conditions, one formula, called the *conclusion* of the
> rule, can be *inferred* from certain formulas, called the *hypotheses*
> of the rule.
>
> How should we define the *theorems* of a formal system F? Obviously they
> should satisfy the two laws:
>
> i) the axioms of F are theorems of F;
> ii) if all the hypotheses of a rule of F are theorems of F, then the
> conclusion of the rule is a theorem of F.
>
> Moreover, we want a formula to be a theorem of F only if it follows
> from these laws that it is a theorem. We can therefore define a theorem
> of F to be a formula of F which can be seen to be a theorem on the basis
> of laws (i) and (ii)."
Fine, good.
> From his passage, we could see clearly if we talk about rules of inference
> in the context of FOL proofs in a formal system (in which is, again, the
> context of my argument),
you talked about "frameworks" in the previous post, not formal systems.
Which do you mean?
> then the rules can't be applied to just any formula.
Why on earth not?
Of course, not any old sequence of characters is a formula,
but the rules simply do apply to whatever formulas are being considered.
There is absolutely nothing in your quote from Shoenfield that
says otherwise -- and in his earlier description of what constitutes
a formal system, he makes it explicit that a *choice* of what constitute
the formulas of the formal system is onvolved. Simply saying that
FOL= is being used is not enough to pin down the formal system;
to be precise, a definition of the choice of syntax -- the lexicon --
is also needed.
> If any formula that is applicable to be "pertained" by a rule of inference
> (whether as a hypothesis or a conclusion) *it must be at least an axiom*:
Where on earth do you get that from?
The vocabulary of "pertaining" comes from you, btw.
Let's take Peano arithmetic, which I hope you agree is a theory
in FOL=. You can see the axioms at:
http://en.wikipedia.org/wiki/Peano_arithmetic
We had better be able to prove that 2 + 3 = 3 + 2;
in the official syntax, that is:
s(s(0)) + s(s(s(0))) = s(s(s(0))) + s(s(0)))
But *none* of s(s(0)), s(s(s(0))), s(s(0)) + s(s(s(0))),
s(s(s(0))) + s(s(0))) or the formula in question appear in the axioms.
So, according to you, this axiomatisation can't prove this statement --
is that right?
> In addition, we could easily see from his passage that rules of inference
> can't be applied to *any* formula without violating the definition of
> syntactical proof in FOL. For example, let L = L(T = {Ax[Sx=e]}. Now,
> by Expansion Rule, we'd have:
>
> (1) Ax[Sx=e] \/ ~(Ex[Sx=e])
>
> By the essence of what you've alluded above (and Allan, et al, said before),
> if we just stipulate an extension of L which is, say, L' = L(e,e',S), then
> we could have this theorem:
>
> (1') Ax[Sx=e] \/ ~(Ex[Sx=e'])
not by using just the the rules of FOL from no axioms we wouldn't.
How do you propose to prove this?
> In addition, as I've alluded to in previous posts, if we permit the
> existence a nonlogical symbol *foreign* to the underlying (T = {Ax[Sx=e]},
> such as say "e'", then we'd open a floodgate to the entire existences
> of all the elements of say a (non-empty) Grothendieck universe (whose size
> would probably be more that just uncountable), to be in theorems of T!
Here you confuse the syntax of the language with the domain that is
being described. Following Shoenfield himself -- in the parts you
didn't cite -- he says exactly what is involved in specifying a
language.
> --
> "To discover the proper approach to mathematical logic,
> we must therefore examine the methods of the mathematician."
> (Shoenfield, "Mathematical Logic")
--
Alan Smaill
With due respect, no. You are completely confused.
No. Here is the source of your confusion. All Shoenfield is doing is
using the two laws above to *define* the notion of a theorem of system
F. Roughly, a theorem is either an axiom or something that you can
prove by means of the rules from previously established theorems. You
are thus confusing the definition of "theorem", which requires that you
restrict the rules of F to theorems if you want to generate *further
theorems*, with the (imaginary) stipulation that you must restrict the
rules of F to theorems generally in all contexts.
> [Note in law (ii) the phrase "rule of F": he clearly meant the rule
> that's being applied on the hypotheses of F, which clearly doesn't
> mean *any* formula.
No, it is talking, just as it says, about the hypotheses of a RULE of F,
which can be any formulas. Note that the claim is a conditional: IF all
the hypotheses of a rule of F are theorems of F, then the conclusion is
a theorem. This conditional does not say that you cannot apply the rule
to non-theorems; it simply says that you must apply it only to theorems
of F in order for a conclusion of the rule to count as a *theorem of F*.
In fact, of course, you *must* be able to apply the rules of F to any
formulas of the language of F, for this is the only way that you can
prove anything from a first-order theory like PA whose axioms are not
theorems of F.
> In addition, we could easily see from his passage that rules of inference
> can't be applied to *any* formula without violating the definition of
> syntactical proof in FOL. For example, let L = L(T = {Ax[Sx=e]}.
I guess this means that L is a language containing only the 1-place
function symbol S and the constant e. And that T is a first-order
theory whose sole non-logical axiom is Ax[Sx=e].
> Now, by Expansion Rule, we'd have:
>
> (1) Ax[Sx=e] \/ ~(Ex[Sx=e])
Yes, that would be a theorem of the theory.
> By the essence of what you've alluded above (and Allan, et al, said
> before), if we just stipulate an extension of L which is, say, L' =
> L(e,e',S), then we could have this theorem:
>
> (1') Ax[Sx=e] \/ ~(Ex[Sx=e'])
Sure.
> then given the very same condition - same hypothesis - Ax[Sx=e], we could
> derive 2 *different conclusions*,
But we could already have done that above. Add any bunch of superfluous
conjuncts to (1) above.
> a clear violation of what Shoenfield stated above:
> "under certain conditions, _one formula_, called the *conclusion* of
> the rule, can be *inferred* from ... the *hypotheses* of _the_ rule."
You are misreading this terribly. In any given *application* of a rule
there can of course only be one conclusion for any given set of
hypotheses. However, it is perfectly possible in a *further*
application of the same rule to the same hypotheses to generate a
different conclusion. Doesn't the rule you call Expansion above permit
exactly that? One can infer (1) and also, e.g.,
(1*) Ax[Sx=e] \/ (Ex[Sx=e])
> In addition, as I've alluded to in previous posts, if we permit the
> existence a nonlogical symbol *foreign* to the underlying (T =
> {Ax[Sx=e]}, such as say "e'", then we'd open a floodgate to the entire
> existences of all the elements of say a (non-empty) Grothendieck
> universe (whose size would probably be more that just uncountable), to
> be in theorems of T! One could demonstrate that I'm wrong here; but
> from what I've gathered, that's not what FOL or FOL's syntactical
> proof is about.
Hope the above helps.
> Hope the above helps.
Hint:
"...arguing with the crank is useless, because he will invariably dismiss
all evidence or arguments which contradict his unconventional belief."
Source:
http://en.wikipedia.org/wiki/Crank_(person)
Herb
> It's my "right" as a poster that I stay confined within the context
> of syntactical/symbolical proof in axiom-set systems of FOL=, when
> talking about valid application of rules of inference.
I've already agreed - from the beginning - that if '+' and '0' are not
in the language, then Axy x+y=0 is not derivable in such a system.
But I also described ANOTHER, DIFFERENT context, which is one where
'+' and '0' ARE in the language of the system. And in that context, as
I desribed it, Axy x+y=0 IS derivable. Yet you keep denying that.
The language has '+' and '0' at appropriate arities; the rules are
natural deduction; and the sole non-logical axiom is Axy x=y. So, Axy x
+y=0 is then derivable in this system. That you have some OTHER system
in which '+' and '0' are not symbols is irrelevent to the fact that,
in the system I just described, Axy x+y=0 is derivable.
It's that simple.
> Any thing else like "proof-in-a-language" or "equational logic"
> is irrelevant
(1) Proof in a language is relevant to the context *I* described but
that you argued about. (2) Aside from that, you claimed 'proof in a
language' is not a notion that is not found in mathematical logic. But
I showed you that it is. I don't see why you can't just admit that you
spoke incorrectly on that matter.
> If by "ordinary context of mathematical logic" you mean the context
> of FOL= syntactical proofs *in formal systems*, then I already gave
> examples explaining what you said below is invalid.
No you haven't. There is no "example' that can possibly change the
fact that I showed a proof such that each formula is in the language I
defined and only natural deduction was used on formulas in that
language and the proof is of "Axy x+y=0" from the sole assumption "Axy
x=y".
> > the rules of inference generalize over formulas of
> > the language - and it is my very point that where '+' and '0' are in
> > the language, the rules of inference allow instantiations to formulas
> > that have those symbols EVEN THOUGH those symbols do not occur in any
> > of the non-logical axioms for some particular axiomatization of some
> > particular theory.
>
> Again, as far as FOL= syntactical proofs *in a formal system* T is concerned,
> Rules of inference can *not* allow such generalization ("instantiation",
> "expansion", or the like) without committing to the error of over-generalization,
> from specific hypothesis/information to general conclusion, as I gave in one
> example before.
There is no "over-generalization" in any step I took. I simply applied
universal generalization from one formula in the language to another
formula in the language.
ASK ANY LOGICIAN, Nam.
MoeBlee
> Also you (MoeBlee) should have realized that as far as FOL= *proof in a theory*
> is concerned, *rules of inference don't "pertain" to just _any_ formula*!
I never said they do.
Indeed, every deduction is a deduction in a language. Every formula in
the deduction must be formula of the language. If the deduction is in
a theory, then every formula must be in the language of the theory.
Nothing I've ever said has contradicted that.
Again, I stated a language that has '+' and '0' of certain arities,
then I stated the theory to be the set of all sentences in said
language that are entailed by Axy x=y. And Axy x+y=0 is a formula in
the language of the theory and Axy x+y=0 is entailed by Axy x=y. That
is, every model (for the language) that makes Axy x=y true is a model
(for the language) that makes Axy x+y=0 true. Moreover, there is a
derivation, using only formulas of the language, of Axy x+y=0 from Axy
x=y.
And again, I'm not talking about YOUR situation in which '+' and '0'
are not in the language.
It's that simple.
> Specifically, rules of inference pertain *only* to formulas that are
> *theorems*. But since theorems are defined from axioms, it isn't much
> an exaggeration to say rules of inference pertains to *axioms*. [And that's
> not just (in your words) "ordinary convention" but it's the very heart of the
> definition of proofs - in FOL=].
What in the world? Rules of inference pertain to formulas in the
language. A formula doesn't have to be a theorem for a rule to apply
to it.
P and P->Q might not be theorems, but the rule of modus ponens still
applies to them.
Maybe what you have in mind is the fact that in a proof each line is
either an axiom (assumption) or the result of a rule applied to
previous lines, so every line is a theorem of the axioms (or
assumptions). That's fine. Except it doesn't apply to NATURAL
DEDUCTION, where, for example we may put P on a line as an assumption,
then reason to get Q on a line, then conclude P->Q.
MoeBlee
Typo. I meant you claimed it is not a notion found in mathematical
logic.
MoeBlee
No I'm not. I've said many times the context of my argument has been FOL
syntactical proof w.r.t. an (axiom-set) formal system, in particular
the formal system in the language that has *zero* non-logical symbols.
Why is that a confusion on my part, as to what is being debated here?
Didn't I just say above:
>> If we use the rules for something else (which I suppose we could) then
>> we're *not* talking about syntactical proofs in FOL (as I've cautioned
>> before).
>
>> [Note in law (ii) the phrase "rule of F": he clearly meant the rule
>> that's being applied on the hypotheses of F, which clearly doesn't
>> mean *any* formula.
>
> No, it is talking, just as it says, about the hypotheses of a RULE of F,
> which can be any formulas. Note that the claim is a conditional: IF all
> the hypotheses of a rule of F are theorems of F, then the conclusion is
> a theorem. This conditional does not say that you cannot apply the rule
> to non-theorems; it simply says that you must apply it only to theorems
> of F in order for a conclusion of the rule to count as a *theorem of F*.
But as I've made caveats before, I'm not interested in applying the rules
to "non-theorems"! Remember this all started out with the debate whether
or not Axy[x+y=0] be a _theorem_ of T = {Axy[x=y]} where L(T) has zero
nonlogical symbol. I.e. we've not been debating whether or not Axy[x+y=0]
is a "non theorem"!
>
> In fact, of course, you *must* be able to apply the rules of F to any
> formulas of the language of F, for this is the only way that you can
> prove anything from a first-order theory like PA whose axioms are not
> theorems of F.
You misread my quotation of Shoenfield's book. In that section, F is a formal
system like PA (as in "How should we define the *theorems* of a formal system F").
Then your "prove anything from a first-order theory like PA whose axioms
are not theorems of F" is not parse-able: because in this context PA is F!
(Read: in this context PA's axioms are F's theorems!").
>
>> In addition, we could easily see from his passage that rules of inference
>> can't be applied to *any* formula without violating the definition of
>> syntactical proof in FOL. For example, let L = L(T = {Ax[Sx=e]}.
>
> I guess this means that L is a language containing only the 1-place
> function symbol S and the constant e. And that T is a first-order
> theory whose sole non-logical axiom is Ax[Sx=e].
>
>> Now, by Expansion Rule, we'd have:
>>
>> (1) Ax[Sx=e] \/ ~(Ex[Sx=e])
>
> Yes, that would be a theorem of the theory.
>
>> By the essence of what you've alluded above (and Allan, et al, said
>> before), if we just stipulate an extension of L which is, say, L' =
>> L(e,e',S), then we could have this theorem:
>>
>> (1') Ax[Sx=e] \/ ~(Ex[Sx=e'])
>
> Sure.
>
>> then given the very same condition - same hypothesis - Ax[Sx=e], we could
>> derive 2 *different conclusions*,
>
> But we could already have done that above. Add any bunch of superfluous
> conjuncts to (1) above.
>
>> a clear violation of what Shoenfield stated above:
>
>> "under certain conditions, _one formula_, called the *conclusion* of
>> the rule, can be *inferred* from ... the *hypotheses* of _the_ rule."
>
> You are misreading this terribly.
OK I made one mistake here. That's an incorrect example. The Expansion rule
allows multiple conclusions from one hypothesis (due to the nature of
the logical "or"). The example I should have given instead is that
given the same T above, whatever rule(s) you'd use to prove Ex[Sx=e]
from the lone axiom Ax[Sx=e], you wouldn't be able to prove Ex[Sx=e'],
because e' is not in the signature of L = L(T = {Ax[Sx=e]}.
> In any given *application* of a rule
> there can of course only be one conclusion for any given set of
> hypotheses. However, it is perfectly possible in a *further*
> application of the same rule to the same hypotheses to generate a
> different conclusion. Doesn't the rule you call Expansion above permit
> exactly that? One can infer (1) and also, e.g.,
>
> (1*) Ax[Sx=e] \/ (Ex[Sx=e])
So it's a correctable mistake on my part there.
>
>> In addition, as I've alluded to in previous posts, if we permit the
>> existence a nonlogical symbol *foreign* to the underlying (T =
>> {Ax[Sx=e]}, such as say "e'", then we'd open a floodgate to the entire
>> existences of all the elements of say a (non-empty) Grothendieck
>> universe (whose size would probably be more that just uncountable), to
>> be in theorems of T! One could demonstrate that I'm wrong here; but
>> from what I've gathered, that's not what FOL or FOL's syntactical
>> proof is about.
>
> Hope the above helps.
No. You've pointed out one bad but correctable example. You still have
*not* refuted my key point in this thread about Axy[x+y=0] *not* being
a theorem of the lone axiom system T = {Axy[x=y]}, where L(T) has zero
nonlogical symbols, using the rules of inference, and using the definitions
of theorem proof in FOL.
Do you happen to know that those who were part of "Police Vigilante",
"Commissar", or Inquisitors, would never consider themselves as "criminals"?
In fact it wouldn't be a surprise if some of them would consider themselves
as "Saints"!
In the land of reasoning, the cranks are those whom we should fear less.
What harm could they really bring to the foundations of reasoning?
Those who have a mind of an Inquisitor should be the ones whom we should
fear the most!
OK, so if you agreed with me ,in the context I've specified, Axy[x+y=0]
is not a theorem of T = {Axy[x=y]} then there's no argument between us
then.
As per your context below where you'd claim Axy[x+y=0] is derivable,
I have to go over what you said and reflect more on that. [It's a
fact that right now I'm trying to bring some closure on the issue
in my context.
Again we're basing our arguments in 2 different context, so there's nothing
for us to debate here. (At least not yet).
OK. And the comment he passed that that Nguyen's way of doing
it is back@$$ward.
> Your attempts to characterize the arguments in this subthread are
> bizarrely mistaken. Try reading it again without assuming that one
> side must be composed of "standard theorist" zealots trying to supress
> anything non-standard.
How about this: one side is composed of posters trying to
suppress anything that _Nguyen_ writes. They believe that
_Nguyen_ is wrong. It would be more balanced if some posters
supported Nguyen's axioms-first method and some posters
supported the language-first method, but no -- they all seem
to be against Nguyen.
Nguyen's opponents have made it appear that they are the side
being open-minded to Nguyen's method and that Nguyen needs to
be more open-minded, but really, it's Nguyen's opponents who
need to be more open-minded. Comments such as Menzel's
"back@$$wards" and Newman's calling Nguyen a "crank," and
earlier in this thread, an "@$$hole," make it clear that
their side is the side having trouble accepting Nguyen.
This sounds similar to the earlier comment by MoeBlee about
statements involving "thingamajig" being provable. Both Smaill
and MoeBlee argue that in the theory with no axioms, any
tautology is provable, even those involving symbols in the
language that aren't otherwise defined.
Counterintuitive, yes -- but Smaill and MoeBlee appear to
believe that this is the only way that makes sense.
Once again, I accept that there can be vacuous truths, so that
from the theory whose lone axiom is "Ax (~wotsit(x))," one
can prove "Ax (wotsit(x) -> phi)" for any formula phi (in the
right language, of course). But what I still don't accept is
that one can prove theorems, even if merely tautologies, with
certain symbols if there is no axiom with that symbol. And
even if we do allow tautologies to be proved from the null
axiom theory, then I disagree that it's the _only_ way to do
it -- Nguyen's method makes sense as well.
And of course, "Ax (x+y=0)" isn't even a tautology, so that's
even _worse_ than claiming that only tautologies with the
symbol "+" can be proved if no axiom mentions "+". I'd accept
that the theory can prove "Ax (x+y=x+y)" well before I'd
accept that it can prove "Ax (x+y=0)"!
> You seem to be saying that without non-logical axioms, *nothing*
> is provable in FOL= -- that's just no[t] so.
I'd be more likely to accept this standard argument if the
standard theorists didn't riducule Ross Finlayson when he
mentions the null axiom theory in his posts.
So far, what I've seen is that if RF (or any so-called
"crank") is the one proposing the null axiom theory, then
nothing can be proved from it, but if the standard theorists
are the ones proposing the null axiom theory, then suddenly
it can prove infinitely many statements.
Lately, Newman has been calling everyone who disagrees with him a
"crank" or an even less complimentary word. He has devoted most
of his recent posts to telling these so-called "cranks" to shut
up, and warning his allies of the futility of even arguing with
us "cranks" (essentially telling them to shut up as well).
Of course, Newman is considering anyone who disagrees with him to
have an "unconventional" belief. Anyone who fails to accept
Newman as being infallible on set theory and mathematics will
receive this same treatment.
> Those who have a mind of an Inquisitor should be the ones whom we should
> fear the most!
I couldn't agree more!
> Lately, Newman has been calling everyone who disagrees with him a
> "crank" or an even less complimentary word.
No, he hasn't.
Look, I don't like his endless, repetitive postings accusing folks of
being cranks. They're dull and annoying. But he does not call
everyone who disagrees with him cranks. He really has reserved that
term for certain characteristics, which he mentions in his posts.
Indeed, in most of these threads, Herb hasn't really entered into the
conversation at all, so no disagreement *could* take place.
--
"The Hammer is not force. It is absolute power. The Hammer is from Idea Space.
That's the real world. Here is the magical realm.
You are creatures in that realm, who do not quite understand.
But it doesn't matter. There is a story to be told..." James S. Harris, poet.
> This sounds similar to the earlier comment by MoeBlee about
> statements involving "thingamajig" being provable. Both Smaill
> and MoeBlee argue that in the theory with no axioms, any
> tautology is provable, even those involving symbols in the
> language that aren't otherwise defined.
>
> Counterintuitive, yes -- but Smaill and MoeBlee appear to
> believe that this is the only way that makes sense.
Not counterintuitive in the least.
If my language includes + and 0 and my set of axioms is
{(Ax)(Ay)(x = y)}, it is utterly obvious and natural that
(Ax)(Ay) x + y = 0 is a theorem. Why would you possibly think
otherwise? The axiom says that every pair of elements of my domain
are equal and the language stipulates that x + y and 0 are elements of
my domain (for every interpretation of x and y).
> Once again, I accept that there can be vacuous truths, so that
> from the theory whose lone axiom is "Ax (~wotsit(x))," one
> can prove "Ax (wotsit(x) -> phi)" for any formula phi (in the
> right language, of course). But what I still don't accept is
> that one can prove theorems, even if merely tautologies, with
> certain symbols if there is no axiom with that symbol.
You don't accept it simply because there's a slew of folks saying Nam
is wrong and you want Nam to be right.
> And even if we do allow tautologies to be proved from the null axiom
> theory, then I disagree that it's the _only_ way to do it --
> Nguyen's method makes sense as well.
Nam's suggested convention is perfectly sensible and no one has said
otherwise. All we've claimed is that it is not the convention adopted
by most logicians. (Indeed, I've *never* seen any text define the
language of a theory the way he suggests.)
--
Jesse F. Hughes
" ... And I'm Michele Norris."
-- Quincy P. Hughes
Furthermore, the very reason that he wants Nam to be right
is *because* there is a slew of folks saying he's wrong.
Marshall
Alas, I fear you are. Be that as it may:
> ...You've pointed out one bad but correctable example. You still have
> *not* refuted my key point in this thread about Axy[x+y=0] *not* being
> a theorem of the lone axiom system T = {Axy[x=y]}, where L(T) has zero
> nonlogical symbols, using the rules of inference, and using the
> definitions of theorem proof in FOL.
Well, I should hope I didn't refute that. It is obviously true that
"Axy[x+y=0]" is not a theorem of T if the language L(T) of T is
stipulated to contain no non-logical symbols. For on that assumption
(and assuming "+" is a non-logical symbol) "Axy[x+y=0]" is not even a
sentence of L(T).
Surely no one disagreed with you on *that* point.
Only half-right. It's because there's a slew of folks saying
that Nam is wrong _and_ there's a slew of folks saying that
Ross Finlayson is wrong as well!
RF once came up with a "null axiom theory" -- i.e., a theory
with no axioms at all. The standard theorists then told RF
that such a theory was pointless, because without axioms
there could be no theorems.
Now, not only can theorems about "+" such as Ax (Ay (x+y=0))
be proved in theories with no axioms mentioning "+,"
suddenly theorems can be proved without axioms at all. RF
can't prove theorems without axioms in his null axiom
theory, but the standard theorists can.
So now, I ask of the standard theorists, can theorems be
proved in the null axiom theory, a theory without any axioms
at all?
If no, then Nguyen is right.
If yes, then RF is right.
The standard theorists would have it so that _both_ Nguyen
and RF are wrong. I'm sorry, but the standard theorists
can't have it both ways. Either the null axiom theory has
theorems and RF is right, or it has no theorems and Nguyen
is right.
I'll accept that either Nguyen or RF is _wrong_, as soon
as the standard theorists accept that one is _right_.
> Furthermore, the very reason that he wants Nam to be right
> is *because* there is a slew of folks saying he's wrong.
And the very reason that the standard theorists want Nguyen
to be wrong is because there is a slew of folks saying he's
wrong, and the very reason that the standard theorists want
RF to be wrong is because there is a slew of folks saying
he's wrong as well. The standard theorists always seem to
stick together.
Standard logic dictates that exactly one of Nguyen and RF
is right, and exactly one of them is wrong. I'll let the
standard theorists decide which is which.
(Whichever one is wrong might be right using a different
type of logic, such as one in which language must be
defined before the theory. But exactly one of them is
right using standard logic only.)
That depends on exactly what the "null axiom theory" is supposed to be;
RF was not terribly clear on the point as I recall. If, by the null
axiom theory, RF means a theory that lacks even logical axioms, then of
course nothing whatever be proved. However, if RF only means a theory
with no *non-logical* axioms (e.g.,, the pure predicate calculus), then
the theory has infinitely many theorems.
> Now, not only can theorems about "+" such as Ax (Ay (x+y=0)) be proved
> in theories with no axioms mentioning "+,"
If, and only if, "+" is in the languages of the theories in question.
> suddenly theorems can be proved without axioms at all.
If, and only if, "without axioms" means "without non-logical axioms".
> RF can't prove theorems without axioms in his null axiom theory, but
> the standard theorists can.
Ross can too if, again, the null axiom theory simply means that his
theory has no non-logical axioms.
> So now, I ask of the standard theorists, can theorems be proved in the
> null axiom theory, a theory without any axioms at all?
As noted.
Well then there's no disagreement between you and me on that point, which
is:
From the lone-axiom formal system T = Axy[x=y] one can *not* prove Axy[x+y=0],
using the FOL syntactical proof machinery which includes rules of inference.
***
But I'm not sure if it's true that "no one" disagreed with me - at least at
the beginning of this (sub) thread.
> But I'm not sure if it's true that "no one" disagreed with me
> - at least at the beginning of this (sub) thread.
You have just been hacked by the sci.gang: you had said some quite
interesting things in your first couple of posts...
-LV
> in most of these threads, Herb hasn't really entered into the
> conversation at all, so no disagreement *could* take place.
Right. You know, time is precious.
Herb