[FOM] Concerning definition of formulas

[John McCarthy]

Tarski's notion of truth can be used computationally.  Thus we may
have

(\forall exp)(Identity(exp) => True(exp)),

where Identity(exp) is the name of a syntactic computation on the
expression  exp  that tests whether  exp  is a polynomial identity.

> Date: Tue, 02 Oct 2007 21:45:04 +0100
> From: Andy Fugard <a.fugard at ed.ac.uk>

> Can't resist sending this, which seems related to a lot of the discussion:
> 
> ``In fact the notion of truth a la Tarski avoids complete triviality by 
> the use of the magical expression `meta': we presuppose the existence of 
> a meta-world, in which logical operations already make sense; the world 
> of discourse can therefore be interpreted in the meta-world, typically 
> the truth of A becomes meta-A, and we can in turn explain `meta-A' by 
> `meta-meta-A' ... We are facing a transcendental explanation of logic 
> `The rules of logic have been given to us by Tarski, which in turn got 
> them from Mr. Metatarski', something like `Physical particles act this 
> way because they must obey the laws of physics' ''
> 
> from Jean-Yves Girard
> 
> 
> @INPROCEEDINGS{Girard1999,
>    author = {Jean-Yves Girard},
>    title = {On the meaning of logical rules {I}: syntax vs. semantics},
>    booktitle = {Computational Logic},
>    year = {1999},
>    editor = {U. Berger and H. Schwichtenberg},
>    volume = {165},
>    series = {Series F: Computer and Systems Sciences},
>    pages = {215--272},
>    publisher = {Springer Verlag}
> }
> 
> -- 
> Andy Fugard