Proofs in Different Theories

On this page we look at proving things in different theories, such as,

In many areas, such as set theory, we use a logic over the theory.

When proving things we usually use Intuitionistic logic (see page here). Although there is also a connection between set theory and boolean logic which can be seen nicely in Venn diagrams.

logic over set

Logic and Type Theory

'It is useful to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing subobjects.' see ncatlab
proof in type theory In type theory, types can represent both the structure and the logic within type theory.

Logic and Category Theory

See topos theory

 

 

 

 

 

 

 

 

 

 

 


metadata block
see also:

Computation and Algebra

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.