# Talk:Metatheorem

## Placeholder

I'm going to work on this based on Dan's notes, with the idea that I'll fix it based on whatever total consensus arises with all interested parties. — Rob (and his talk) 17:12, 20 October 2006 (EDT)

## I agree, Tom

The point about totality checking being *more* conservative than the fixed search strategy of logic programming is a good one - the need for factoring lemmas being the perfect example here - so I think that change is good. Does the article seem reasonable otherwise, because I'm not certain the approach is even the right one here. — Rob (and his talk) 19:16, 9 March 2007 (EST)

- I think it's a hard subject but this is a reasonable take on it and a good start, yes. — Tom 7 14:01, 12 March 2007 (EDT)

## Why "meta" ?

To an outsider, all the "meta"-theorem stuff seems like unnecessary baggage. Normally, I would think a meta-theorem is a theorem about theorems. Here's what I think the answer to my question is: In the olden days, one implemented XYZ logic in Twelf and wrote a theorem that XYZ theorems were valid. But now, we use Twelf to directly encode our theorems about object languages. The "meta" is not really appropriate any more. I suppose for historical reasons people are used to "metatheorem", but it might make more sense just to dispense with "meta" and just talk about theorems. Or if not, then a better explanation of "meta" is needed than "for historical reasons" Boyland 01:35, 13 March 2007 (EDT)

- You're right that this needs to be explained more clearly. The point of the "meta" is to distinguish between

- a
*theorem*in an encoded deductive system, and - a
*metatheorem*about an encoded deductive system.

- For example, if I encoded a logic with a judgement
`A true`, then`(all [a:prop] impl a a) true`might be a theorem in the encoded logic (if I can come up with an LF term of that type), whereas cut elimination for the logic is a metatheorem about it. Drl 10:14, 13 March 2007 (EDT)- To answer another point (we edit-conflicted each other making the same first point), I don't see this as an issue of "historical resasons" at all, this is the way I understand the research community working now - the two-year-old workshop on doing this sort of thing is called the Worshop on Mechanizing Metatheory. People still think of Prolog as a "theorem prover" for Horn clauses (see the Wikipedia page on Prolog), and those kinds of theorems are the same kinds of "theorems" (
`plus 3 4 7`,`of (lam [x] E x) (arrow unit unit)`) that are discussed on this page - they are nothing like ∀∃-statement metatheorems. Dan/John/others, where do you think this article could explain this better? — Rob (and his talk) 10:30, 13 March 2007 (EDT)

- To answer another point (we edit-conflicted each other making the same first point), I don't see this as an issue of "historical resasons" at all, this is the way I understand the research community working now - the two-year-old workshop on doing this sort of thing is called the Worshop on Mechanizing Metatheory. People still think of Prolog as a "theorem prover" for Horn clauses (see the Wikipedia page on Prolog), and those kinds of theorems are the same kinds of "theorems" (

- Reading the current article, I'm okay with the explanation of "theorem", but the transition to the Totality assertion section should rehash the discussion at the top about "metatheorem" being a statement about an object language and contrast it with theorem (I missed the definition of "metatheorem" at the top on the first read). Also, when I used the word "theorem" this way, Frank objected that he likes to reserve "theorem" for a judgement defining truth in a logic (so not all derivable object-language judgements are "theorems"). Not sure if we want to use the word that way or not. Drl 12:39, 13 March 2007 (EDT)
- I'll work on the first point - as for the second point, perhaps I could add in to the example something with a logic - just , and say "we could reserve 'theorem' for this kind of statement, but to avoid saying 'derivable object-language judgment' too many times we often blur the distinction by referring to both as theorems. — Rob (and his talk) 08:41, 14 March 2007 (EDT)

- Reading the current article, I'm okay with the explanation of "theorem", but the transition to the Totality assertion section should rehash the discussion at the top about "metatheorem" being a statement about an object language and contrast it with theorem (I missed the definition of "metatheorem" at the top on the first read). Also, when I used the word "theorem" this way, Frank objected that he likes to reserve "theorem" for a judgement defining truth in a logic (so not all derivable object-language judgements are "theorems"). Not sure if we want to use the word that way or not. Drl 12:39, 13 March 2007 (EDT)