| element relation |
| typing relation |
| equality |
| entailment / sequent |
| true / top |
| false / bottom |
| implication |
| logical equivalence |
| negation |
| negation of equality / apartness |
| negation of element relation |
| negation of negation |
| existential quantification |
| universal quantification |
| logical conjunction |
| logical disjunction |
| |
symbol | in type theory (propositions as types) |
| function type (implication) |
| product type (conjunction) |
| sum type (disjunction) |
| empty type (false) |
| unit type (true) |
| identity type (equality) |
| equivalence of types (logical equivalence) |
| dependent sum type (existential quantifier) |
| dependent product type (universal quantifier) |
| |
symbol | in linear logic |
| linear implication |
| multiplicative conjunction |
| additive disjunction |
| additive conjunction |
| multiplicative disjunction |
| exponential conjunction |
| exponential disjunction |