Une antinomie, qui vient du grec ancien « ἀντινομία » (« antinomía ») signifiant une « contradiction entre les lois », est un type de contradiction logique, dans lequel des déclarations mutuellement contradictoires sont tout aussi bien fondées et prouvées (dans le cas des systèmes formels). Elle ne doit pas être confondue avec l'antonymie (symétrie d'opposition entre deux termes contraires).
Les antinomies, dans ce contexte, sont des cas particuliers de paradoxes, provoquant immédiatement une contradiction fatale dans la structure logique où elles apparaissent.
Communément, il y a une distinction entre les antinomies sémantique et les antinomies logiques. Les antinomies logiques sont les antinomies qui découlent de seules raisons logiques formelles. Les antinomies sémantiques sont des antinomies qui découlent de la sémantique des termes utilisés. Elles sont aussi appelées antinomies linguistiques ou grammaticales.
La caractéristique commune des antinomies logiques est, entre autres, perçue par Alfred Tarski et Bertrand Russell dans le « rapport à soi » ou la « relation inverse ».
Parmi les exemples de ce type d'antinomie se trouvent :
le paradoxe de Russell (antinomie de l'ensemble de tous les ensembles qui n'appartiennent pas à eux-mêmes, 1901/1903),
(liée au paradoxe du barbier),
les paradoxes de Cantor (1897 et 1899, antinomie du plus grand cardinal),
le paradoxe de Burali-Forti (antinomie de l'ensemble des ordinaux, 1897).
Pour surmonter les antinomies logiques connus, la théorie de type a été introduite par Bertrand Russell. Elle est critiquée car bien qu'elle évite le paradoxe de Rusell, elle ne surmonte pas le paradoxe d'Épiménide (l'antinomie du menteur) et celui de Grellings.
Des exemples d'antinomies sémantiques sont :
le paradoxe du menteur,
le paradoxe de Grelling-Nelson.
Une des façons de résoudre les antinomies sémantiques est d'interdire l'auto-référence (cf. métalangage).
Des paradoxes comme ceux de Berry ou de Richard peuvent être considérés comme relevant des deux types à la fois.