Contents

# Contents

## Idea

In formal logic one speaks of a “fragment” of a theory when referring to just part of it. Specifically, when rules of type formation or some of the inference rules are omitted, one says that one retains a “fragment” of the original theory.

This terminology is jargon and has not been formalized. What exactly counts as a fragment of a theory and what not differs a bit from author to author.

## Examples

### First-order logic in type theory

In type theory first order logic of propositions is contained via “propositions as types” essentially as the sub-theory dealing with types of type Prop, hence with bracket types or what in homotopy type theory are called (-1)-types.

Some authors speak of the “first-order fragment” of type theory when referring to this restriction (e.g. Bezem-Hendriks-Nivelle 02, Hendriks 13).

### Multiplicative conjunction in linear logic

By default linear logic has a wealth of conjunctions. Discarding or ignoring all of them except the multiplicative conjunction yield the fragment of multiplicative linear logic.

## References

• Marc Bezem, Dimitri Hendriks, Hans de Nivelle, Automated Proof Construction in Type Theory using Resolution, 2002 (pdf)

• Dimitri Hendriks, Metamathematics in Coq, 2013 (pdf)

Last revised on November 2, 2014 at 20:08:57. See the history of this page for a list of all contributions to it.