[FOM] Concerning definition of formulas
John McCarthy
jmc at cs.Stanford.EDU
Wed Oct 3 15:53:00 EDT 2007
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
More information about the FOM
mailing list