Transparent Intensional Logic (TIL) is a higher-order, hyperintensional, typed -calculus with a procedural semantics. The terms of the ideography of TIL denote procedures producing mappings rather than the mappings themselves. Mappings are semantically secondary, while the procedures are semantically primary. Procedures are sui generis objects of the ontology of TIL. I first introduce six kinds of TIL procedures. There are two kinds of atomic procedures that supply objects to operate on by molecular procedures, namely Trivialization and variables, and two basic kinds of molecular procedures, (-)Closure and Composition. Closure is the procedure of producing a functional mapping by abstracting over the values of -bound variables. Composition is the procedure of applying a function to its arguments. There is a pair of dual procedures operating on lower-order procedures, namely Trivialisation (0C) and Double Execution (2C). While 0C displays the procedure C as an object to operate on, 2C cancels the displaying effect, as 2C produces what is produced (if anything) by the procedure produced by C. It means that while in 0C the procedure C occurs hyperintensionally rather than in the execution mode, in 2C it occurs extensionally.
Having introduced TIL fundamentals, I address and solve a technical problem arising in the hyperintensional procedural semantics of this system. The problem concerns variable binding. A pair of procedures that are duals of one another work together well in the standard cases. But there are limiting cases where they fail to. One of the procedures, Trivialization, when applied to another procedure, raises the logical type of this procedure and makes it technically feasible to operate on this procedure itself rather than the product it is typed and structured to yield. Any occurrences of variables within the procedure become Trivialization-bound. The other procedure, Double Execution, when applied to another procedure, is typed and structured to, first, obtain the product of this procedure and, second, obtain the product of this product on condition that the latter is itself a procedure. Double Execution lowers the logical type of the procedure it is applied to. It is a feature of Double Execution that its execution produces entities beyond the second procedure. As a result, there are cases where Trivialization-bound occurrences of variables become free occurrences; new variables that are apparently free for substitution can emerge by executing Double Execution. This is something we do not want to happen. These cases undermine our definition of substitution, which in turn jeopardizes the validity of the rules of -conversion, not least -conversion. The technical result I present is a principled, as opposed to ad hoc, definition of substitution, which introduces the restrictions required. I also argue that it is not an option to solve the problem by jettisoning one of the two procedures, as both are indispensable and, thus, must be made to work properly together as duals. The problem I address and solve extends beyond Transparent Intensional Logic. Any logic or programming language with a high degree of expressive power is liable to confront a comparable problem with variable binding.