Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
How would you define the usual jargon “fragment” in logic?
There ought to be a simple formal definition, I suppose, such as “Given a language L and a theory T in that language, then a fragment of T is… “
I thought it usually connoted a restriction on a logic (not on a theory per se) where some of the rules of type formation or some of the inference rules are omitted. For example, in multiplicative linear logic, one drops the contraction and weakening rules.
If one really wanted to be formal, one could formalize the idea that a fragment of a logic or deductive system is a subset of the structural rules and a subset of the logical rule pairs (organized into pairs of introduction/elimination rules). Mind you, this is just off the top of my head. I’ve only heard the term used informally.
My thoughts agree with Todd’s.
So given theory T and theory T+AxiomA. Is one a fragment of the other?
for what it’s worth, in my experience in proof theory the term “fragment” is used when one system contains a subset of the logical connectives/judgments of another system, but not necessarily when it just contains a subset of the inference rules. So, MLL is considered a fragment of MALL and MELL, but intuitionistic logic is not considered to be a fragment of classical logic, even though the inference rules of the sequent calculus LJ are a restriction/subset of those of LK.
I think the informal content of “L1 is a fragment of L2” is roughly the same as “L2 is a conservative extension of L1”.
but intuitionistic logic is not considered to be a fragment of classical logic
Thanks. What then is a good word for how intuitionistic logic is obtained from classical logic by removing axioms? Is there anything one says?
I think the usual word is “restriction”. For example, from Wikipedia, “intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not admitted as axioms”.
I see. Hm, that’s a rather unfortunate use of terminology, then.
Just checking on Wikipedia. Actually their statement is worse even, they write
Semantically, intuitionistic logic is a restriction of classical logic
This seems really bad terminology to the extent of being wrong. I would understand if one said that IL as a theory is “a restriction” of CL, in that it contains fewer symbols in its specification. But there seems no good way to regard the richer semantics of IL as a “restriction” of the semantics of CL.
I’m not sure what the wikipedia editor had in mind by “semantically”. (Actually, for the morbidly curious like me, it seems that at some point somebody switched “syntactically” to “semantically”… :-)
But the problem of course is that both “fragment” and “restriction” are potentially negative-sounding words, which is why it is sometimes best to avoid them unless a very clear sense is meant. (E.g., “LJ is a restriction of LK where the right-hand-side of a sequent is not allowed to contain more than one formula”, “MLL is the fragment of linear logic containing just the multiplicative connectives tensor and par”.)
Googling for “propositional fragment” and “first-order fragment” produces quite a few hits.
There is a thesis “Metamathematics in Coq” (pdf) which speaks of the “first-order fragment” in Coq. (That’s maybe a comment more relevant to the other thread.)
it seems that at some point somebody switched “syntactically” to “semantically”… :
Ah, interesting! Thanks for checking this. Maybe this should be debated in the Wikipedia talk pages by somebody. It really seems wrong at this point, while “syntactically” would seem right.
Googling for “propositional fragment” and “first-order fragment” produces quite a few hits.
Yeah, that’s definitely well-established terminology (see also “Horn fragment”), it’s just when asserting an uncontextualized “language L1 is a fragment of language L2” that things get murkier.
Googling for “propositional fragment” and “first-order fragment” produces quite a few hits.
Yeah, that’s definitely well-established terminology
Oh, okay. See, this is what I was really interested in, coming from our discussion in the thread on the “HoTT FAQ”.
There we were looking for the right word to describe how first order logic sits inside (homotopy-)type theory.
Googling for “propositional fragment” and “first-order fragment” produces quite a few hits.
Yeah, that’s definitely well-established terminology
Oh, okay. See, this is what I was really interested in, coming from our discussion in the thread on the “HoTT FAQ”.
Just to be clear, it’s well-established to speak of the propositional fragment of a first-order logic or dependent type theory (meaning no first-order/dependent quantifiers), or to speak of the first-order fragment of a higher-order logic or type theory (meaning no higher-order quantifiers, or alternatively meaning no higher-order functions). I’m also used to thinking of intuitionistic first-order logic as the fragment of MLTT only allowing quantification over a fixed domain of elements (rather than in terms of a restriction to bracket types), although this is not totally standard, and is not quite the same flavor as the above usages because the elimination rules for existential/dependent sum are different.
The wikipedia page Fragment (logic) is actually not bad, and in particular the stipulation that “the semantics of the formulae in the fragment and in the logic coincide”. What makes this criterion essentially informal, though, is the possibility of giving more than one semantics. For example, because of the existence of double-negation translations, classical logic could reasonably be seen as a negative fragment of intuitionistic logic consisting of the image of this translation—but on the other hand this ignores the fact that there are many double-negation translations, and picking one excludes some of the potential meanings of a classical proposition.
1 to 15 of 15