natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
strong axioms
further
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.
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).
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.
Last revised on November 2, 2014 at 20:08:57. See the history of this page for a list of all contributions to it.