On 4/12/2013 8:45 AM, Nam Nguyen wrote: > On 12/04/2013 3:29 AM, Alan Smaill wrote: >> Nam Nguyen <firstname.lastname@example.org> 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. >
I told you before. The textbooks are very bad about all of these things.
I was once flamed by someone years ago who kept talking about "object languages". My background had been in 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 to what follows. I am very bad about these things.
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
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"
(These are already meta-linguistic variables 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.
We take the consequences of the following as the basic theory.
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 as your domain.
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.