Re: Model theory, abstract syntax

>At 01:56 PM 7/16/01 -0500, Aaron Swartz wrote:
>>I'm unclear on the difference between model theory and abstract 
>>syntax. Can someone clarify?
>
>I'll take a shot;  I guess the real formal systems folks will put me right...
>
>I think they are clearly different, but related, issues.
>
>- Abstract syntax defines a language (i.e. a set of well formed 
>formulae, or wff) in terms of some set of terminal symbols.  Given a 
>formula, it allows us to say whether or not it is a well formed 
>sentence (instance) of the language.  It also provides us with an 
>annotation for the the structure of a wff that can be used as a 
>reference point for defining semantics for the various allowed 
>forms.  In summary:  abstract syntax is primarily about forms.
>
>- Model theory defines semantics for the various allowed forms, by 
>telling us how they can be interpreted in terms of some universe of 
>discourse.  The elements of the language refer to members of the 
>universe, and statements can be interpreted to be true or false of 
>of such a universe.  An "interpretation" of a formula is an 
>assignment of values from the domain of discourse to symbols in the 
>formula, such that the formula can be said to true or false.  A 
>"model" of a formula is an interpretation for which the formula 
>evaluates to true.  Hence "model theory".
>
>- A third related concept is "proof theory":  a deductive apparatus 
>based on syntactic transformations of wffs that preserves truth.

Pretty much right :-). I tend to think of an abstract syntax as the 
syntax abstracted away from the purely lexical details, and treated 
as a kind of algebra (the term is due to John McCarthy, and this is 
his way of thinking.)  One way to state the relation between abstract 
syntax and model theory (AKA logical semantics, BTW) is that the 
abstract syntax specifies the syntax in just enough detail to make it 
possible to state the interpretation rules of the model theory, but 
no more. So for example, you need to know that a conjunction is a 
conjunction and has, say, a list of conjuncts; and that is really all 
you need to know in order to say that a conjunction is true (in I) 
iff all of its conjuncts are true in I and false otherwise. You don't 
really need to know that the conjunction is written by writing '&&' 
in between each conjunct, or by writing '(and' and then the conjuncts 
and then ')', or whatever; those are the concrete syntax details. You 
can have many different concrete syntaxes for the same abstract 
syntax, but if there is a 'canonical' concrete syntax then that will 
serve just as well. For us, the RDF graph is something like an 
abstract syntax and N-triples is the cononical concrete (lexical) 
syntax, I guess.

Pat

PS. You can do proof theory on the abstract syntax, by the way, and 
the result is often called 'natural deduction', though this term is 
also used for concrete proof theories. The overarching idea is that 
for each kind of statement (universal quantifications, conjunctions, 
whatever) there are two rules of inference, one which introduces it 
(ie has a conclusion of that form) and one which eliminates it (ie 
uses an antecendent of that form).

---------------------------------------------------------------------
(650)859 6569 w
(650)494 3973 h (until September)
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Monday, 23 July 2001 20:27:25 UTC