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

1. a theorem in an encoded deductive system, and
2. 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)

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)