Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Topic: Matheology § 224
Replies: 84   Last Post: Apr 20, 2013 4:43 PM

 Messages: [ Previous | Next ]
 fom Posts: 1,968 Registered: 12/4/12
Re: Matheology § 224
Posted: Apr 12, 2013 8:59 PM

On 4/12/2013 8:45 AM, Nam Nguyen wrote:
> On 12/04/2013 3:29 AM, Alan Smaill wrote:
>> Nam Nguyen <namducnguyen@shaw.ca> writes:
>>

>>> But what is "meta-logic of the meta-language", in the context of FOL
>>> structure? Or is that at best just intuition and at worst just a
>>> buzzword?

>>
>> You tell us that it is possible to reason about language structures.
>> What logic are you using to do that -- or is that at best just intuition?

>
> I've used FOL ( _First Order Logic_ ) definitions that one should be
> familiar with.
>

Nam,

all of these things.

I was once flamed by someone years ago who kept talking
proper classical mathematics, so I had been unaware of
the jargon that developed in other fields. I do not
know these things as others do. I had to learn the
hard way.

I am sure Alan or Frederick can make corrections

There is logic in the sense of what transformation
rules and rules of detachment are employed in
formulating a proof using a deductive calculus.

Then there is the logic employed when explaining
and analyzing the grammatical structure of proofs
and the related linguistic forms.

Aristotelian logic employs certain natural language
constructions and defines the well-formedness of
admissible statements through analysis. But, this
form of logic had not been sufficient for complex
sentences.

Ultimately, a different form of logic based on the
compositionality of language elements -- nested
functions for terms, subformulas for wffs -- had
been developed. It requires prior definition of
the simplest language elements by statements of
use:

'(' shall indicate the start of scope for a formula

')' shall indicate the end of scope for a formula

etc.

One cannot define much without using variables intended
to represent "object language" elements.

"Define a proposition as a well-formed formula
from an object language"

"Let A_1, A_2, ... represent propositions"

ranging over syntactic elements from my "object
language")

"Every propostional variable is assumed to contain
the scope delimiters for the well-formed formula
it represents."

"If A_1 and A_2 represent propositions, then
(A_1 -> A_2) represents a propostion."

"If A_1 represents a proposition, then
-(A_1) represents a propostion."

On the basis of these defined well-formed expressions,
one uses the form of these expression to formulate
deduction rules like the rule of detachment,
modus ponens:

"If given (A_1 -> A_2) and (A_1) deduce (A_2)"

All of these things are done outside of any discussion
of the theory generated by the Peano axioms or
Zermelo-Fraenkel set theory as the deductive closure
of their axioms.

In *the paradigm* of *first-order logic*, these are
stipulations concerning the use of syntactic elements
of the language.

In order for this to have any semantic import, one
must interpret the symbols. This is the model theory
that assigns structures to formally defined deductive
languages.

But, semantic import means that the syntactic elements
of the definite, intended object language, itself,
must now be explained.

"0 is a term"

"If t is a term, St is a term"

Notice that I now need meta-linguistic term variables.
Even without such a variable, I would have to stipulate
an infinite schema of "... is a term" which is not a
part of statements in the object language that are
applied to objects such as numbers or sets.

So, not using a term variable "t", one would still
have

"0 is a term"
"S0 is a term"
"SS0 is a term"
"SSS0 is a term"

and so on.

Moreover, in this simple explanation, I did not even
attempt to talk about quantifiers. I am not trying
to define a language here, only explain the difference
between metalanguage and object language.

The point is, that to describe a formally defined
language, one must have a language in which the
description is given.

It becomes even worse with the model theory. What
is so important about Tarski's paper is that he used
the relationship between metalanguage and object
language to describe a means of assigning truth
valuations to the well-formed elements of the
language.

It would be more correct to say that Tarski clearly
delineated the need for a metalanguage/object language
distinction.

Suppose one begins to reason about the truth or falsity
of statements in the object language without actually
performing deductions involving the statements of that
language as they purport to refer to the objects from
the domain of discourse. Then, one is reasoning in the
metalanguage. Natural deduction in the metalanguage
is what constitutes metalogic.

The paradigm of first-order logic inherits certain
features from a subject called universal algebra.
Algebras have their syntax given by a signature.

For example:

==========================================

We take the consequences of the
following as the basic theory.

It's signature is given by

<<M, |M|>, <c, 2>, <e, 2>>

with models interpreted coherently
according to

M=V()

in the extended signature

<<M, |M|>, <c, 2>, <e, 2>, <EQ, 2>, <=, 2>, <V, 0>, <null, 0>, <set, 1>,
<S, 1>, <P, 1>>

==========================================

comes from something I did.

The first ordered pair indicates the symbol referring
to the domain and its cardinality (in principle).

The remaining ordered pairs indicated predicate symbols,
function symbols, or constant symbols with the arities
to which relations defined in the structure must correspond.

It is at this point, if necessary, that whatever
stipulations concerning the interpretation of those
symbols is given. All of my symbols are defined symbols,

==========================================

AxAy(xcy <-> (Az(ycz -> xcz) /\ Ez(xcz /\ -ycz)))

AxAy(xey <-> (Az(ycz -> xez) /\ Ez(xez /\ -ycz)))

AxAy(xEQy <-> (Az(xcz <-> ycz) /\ Az(zcx <-> zcy) /\ Az(xez <-> yez) /\
Az(zex <-> zey)))

AxAy(x=y <-> Az(xez <-> yez))

Ax(x=V() <-> Ay(-(ycx <-> y=x)))

Ax(set(x) <-> Ey(xcy))

Ax(x=null() <-> Ay(-(xcy <-> x=y)))

AxAy(x=P(y) <-> (Ez(ycz) /\ Az(zex <-> (zcy \/ z=y))))

AxAy(x=S(y) <-> (Ez(ycz) /\ Az(zex <-> (zey \/ z=y))))

==========================================

With the first two definitions technically being
axioms because the symbols may not be eliminated
through substitution. That is why the signature
is formally introduced initially as

<<M, |M|>, <c, 2>, <e, 2>>

Obviously, I cannot specify an infinite domain.
And, the circular definitions constrain the
interpretation of the primitive relations,
so any set model of the sentences must be a
partial model since the defining relations
cannot be represented as elements of any class
to which the language symbols refer.

On the other hand, this would be the point at
which you begin specifying the model of
constructive objects that you wish to serve

Your use of a "this" operator occurs at this
point since it is how you are defining your
domain. It is a metalinguistic usage.

If you try to use it in a proof concerning the
theory of the natural numbers written in
the object language, then you have to explain
it in the signature and your theory is no
longer a standard theory.

Date Subject Author
4/12/13 Alan Smaill
4/12/13 namducnguyen
4/12/13 Frederick Williams
4/12/13 fom
4/13/13 namducnguyen
4/13/13 fom
4/13/13 namducnguyen
4/13/13 fom
4/13/13 namducnguyen
4/13/13 Peter Percival
4/13/13 namducnguyen
4/13/13 Peter Percival
4/13/13 namducnguyen
4/13/13 Peter Percival
4/13/13 namducnguyen
4/13/13 Jesse F. Hughes
4/14/13 namducnguyen
4/14/13 namducnguyen
4/14/13 namducnguyen
4/14/13 Peter Percival
4/14/13 fom
4/14/13 namducnguyen
4/14/13 fom
4/14/13 namducnguyen
4/14/13 namducnguyen
4/14/13 fom
4/14/13 namducnguyen
4/14/13 namducnguyen
4/14/13 namducnguyen
4/14/13 Jesse F. Hughes
4/14/13 namducnguyen
4/14/13 Jesse F. Hughes
4/14/13 namducnguyen
4/16/13 namducnguyen
4/16/13 namducnguyen
4/16/13 Jesse F. Hughes
4/16/13 namducnguyen
4/16/13 fom
4/17/13 namducnguyen
4/17/13 fom
4/17/13 namducnguyen
4/17/13 Jesse F. Hughes
4/17/13 Jesse F. Hughes
4/17/13 namducnguyen
4/20/13 namducnguyen
4/17/13 Frederick Williams
4/17/13 Frederick Williams
4/17/13 fom
4/17/13 Frederick Williams
4/17/13 fom
4/17/13 fom
4/18/13 namducnguyen
4/18/13 Frederick Williams
4/18/13 namducnguyen
4/19/13 Frederick Williams
4/19/13 namducnguyen
4/20/13 Frederick Williams
4/19/13 Frederick Williams
4/19/13 namducnguyen
4/20/13 Frederick Williams
4/14/13 Jesse F. Hughes
4/14/13 namducnguyen
4/14/13 namducnguyen
4/14/13 Jesse F. Hughes
4/14/13 namducnguyen
4/14/13 Peter Percival
4/15/13 Peter Percival
4/14/13 namducnguyen
4/14/13 namducnguyen
4/13/13 Frederick Williams
4/13/13 Peter Percival
4/13/13 Peter Percival
4/13/13 namducnguyen
4/15/13 Peter Percival
4/13/13 fom
4/13/13 namducnguyen
4/13/13 Peter Percival
4/13/13 namducnguyen
4/13/13 Frederick Williams
4/14/13 Frederick Williams
4/14/13 namducnguyen
4/13/13 Peter Percival
4/13/13 namducnguyen
4/13/13 namducnguyen