Deductive Reasoning using TIL

Transparent Intensional Logic (TIL) is a highly expressive logical system apt for the logical analysis of natural language. It operates with a single procedural semantics for all kinds of logical-semantic context, whether extensional, intensional or hyper-intensional, while adhering to the compositionality principle throughout. The reason why we vote for a rich procedural semantics is this. A coarse-grained analysis of assumptions yields paradoxes and puzzles, while an expressive formal system such as TIL makes it possible to build an inference machine that neither over-infers (which yields paradoxes) nor under-infers (which leads to the lack of knowledge). From the formal point of view, TIL is a hyperintensional, partial, typed lambda calculus. By way of examples we illustrate how TIL deals with particular 'puzzles' in a smooth way while adhering to Leibniz's law of substitution of identicals and to the principle of compositionality.