David Corfield relevance logic

The variable sharing principle says that no formula of the form ABA \to B can be proven in a relevance logic if AA and BB do not have at least one propositional variable (sometimes called a proposition letter) in common and that no inference can be shown valid if the premises and conclusion do not share at least one propositional variable.

What if we considered propositions as types with elements? Then it’s not shared propositional letter, but some dependency via variables.

Strict implication

C.I. Lewis’s strict implication, becomes the inhabitance of boxA(w)B(w)\box A(w) \to B(w). Or w:Wf(w):[A(w),B(w)]w: W \vdash f(w): [A(w), B(w)].

Linear logic

Splitting of ‘and’,‘or’ as positive and negative. How close to intensional conjunction, etc.?

Product types can be presented both positively and negatively. The two definitions are equivalent in ordinary type theory, but distinct in linear logic. The same is true of binary sum types if we allow sequents with multiple conclusions.

Last revised on May 5, 2021 at 12:57:00. See the history of this page for a list of all contributions to it.