The Type-Theoretic DPLL (TT-DPLL) algorithm is an approach to determining the habitability of a type in the classically typed lambda calculus. It is derived from the regular DPLL algorithm used for propositional satisfiability solving. It reinterprets DPLL's operations in terms of type construction and context manipulation, leveraging the Curry-Howard correspondence where propositions are types and proofs are terms. The goal is to figure out if there is any possible context that allows construction of a term to inhabit a given type.

This algorithm applies to types structured similarly to Conjunctive Normal Form (CNF) formulae: a product (conjunction) of sums (disjunctions) of "literal types." A literal type is either an atomic type (representing a propositional variable) or its negation (e.g., $P \rightarrow \bot$, where $\bot$ is the empty type).

How it Works

The algorithm systematically explores the space of possible assumptions about atomic types to construct a term inhabiting the goal type. It operates through a recursive process:

Input

• A goal type $G_0$ structured as a product of sums of literal types (e.g., $(P \lor \neg Q) \land (R \lor Q) \equiv$ $(P + (Q \rightarrow \bot)) \times (R + Q)$).
• An initial typing context $\Gamma_0$ (usually empty).

Output

• A term $t$ and a context $\Delta$ such that $\Delta \vdash t : G_0$, indicating $G_0$ is inhabited. The typing context $\Delta$ will contain the necessary assumptions (the "satisfying assignment").
• Or, an indication that $G_0$ is uninhabitable (UNSAT), meaning $\Gamma_0 \vdash G_0 \leftrightarrow \bot$, possibly together with a term $t : G_0 \rightarrow \bot$

Process

The core of the algorithm involves constructing a term for the current goal type $G$ within the current context $\Gamma$. This involves propagation (simplifying the type based on context) and decisions (extending the context).

1. Initialization:

   • Set current context $\Gamma = \Gamma_0$.
   • Set current goal type $G = G_0$.
   • Maintain a list/stack of decision points for backtracking. A decision involves assuming a term of type $A$ (adding $a:A$ to $\Gamma$) or its negation (adding $\text{na}: A \rightarrow \bot$ to $\Gamma$).

2. Propagation Phase (Type Simplification & Forced Moves):
   Repeatedly apply the following rules to simplify $G$ or extend $\Gamma$ based on logical consequence, until no more such simplifications can be made:

   • Product Consequence (Conjunct Elimination):
     If $G$ is of the form $T_1 \times T_2 \times \dots \times T_n$:
     For each $T_i$, if $\Gamma \vdash t_i : T_i$ can be readily established (e.g., $T_i$ is in $\Gamma$, or $T_i = \top$ (the unit type), or $T_i$ is an atomic type $A$ and $a:A \in \Gamma$), then $T_i$ is considered satisfied. The goal effectively reduces to the product of the remaining unsatisfied $T_j$.
     If all $T_i$ are satisfied, $G$ becomes $\top$.
   • Sum Consequence (Disjunct Elimination / Unit Propagation Analogue):
     If a component $T_i$ of $G$ (from a product) or $G$ itself is a sum type $S = L_1 + L_2 + \dots + L_k$:
     If for all but one literal type $L_j$ (say $L_m$), its negation is provable in $\Gamma$ (i.e., $\Gamma \vdash proof_{not\_L_j} : L_j \rightarrow \bot$), then to inhabit $S$, one must inhabit $L_m$. The goal to prove $S$ effectively becomes a goal to prove $L_m$.
     • This step uses [[mention:Beta Reduction|beta-reduction]] implicitly: if $L_j = A$ and $na: A \rightarrow \bot \in \Gamma$, attempting to satisfy $S$ via $L_j$ by providing $a':A$ would lead to $na(a'):\bot$.
   • Contextual Derivations & [[mention:Beta Reduction|Beta Reduction]]:
     If $f: A \rightarrow B \in \Gamma$ and $a:A \in \Gamma$, then $f(a):B$ is derivable (after beta-reduction). This new derivation $f(a):B$ can be added to $\Gamma$ (or used on-the-fly) for further propagation. If $B = \bot$, a conflict is found.

3. Check State:

   • Success (SAT): If the current goal $G$ simplifies to $\top$ (all parts of the original $G_0$ are satisfied by $\Gamma$), then $G_0$ is inhabited. Return the current $\Gamma$ (or the relevant parts forming the "assignment") and the constructed term.
   • Conflict (UNSAT sub-branch): If $\Gamma \vdash \bot$ becomes derivable (e.g., $a:A \in \Gamma$ and $na:A \rightarrow \bot \in \Gamma$, leading to $na(a):\bot$), or if the goal $G$ simplifies to $\bot$:
     • A conflict is detected. Backtrack:
       • Revert $\Gamma$ to its state before the most recent un-flipped decision.
       • Flip the decision (e.g., if $a:A$ was assumed, now remove $a:A$ and try assuming $na:A \rightarrow \bot$. Mark this decision point as flipped).
       • If the decision was $na:A \rightarrow \bot$, and it's being flipped, this path is exhausted.
       • If there are no decision points left to flip (all branches from $\Gamma_0$ lead to conflict), then $G_0$ is uninhabitable. Return UNSAT.
     • Continue from step 2 (Propagation Phase) with the new context.

4. Decision Phase (Branching):
   If no propagation rule applies, and the state is not success or conflict:

   • Select an atomic type $A$ that is part of the current goal $G$ for which neither $A$ nor $A \rightarrow \bot$ is "decided" in $\Gamma$ for the current branch.
     • Heuristic (Pure Literal Analogue): If an atomic type $A$ appears "purely positively" in the remaining goal (i.e., not as $A \rightarrow \bot$, or in a way that readily leads to $\bot$ if $A$ is inhabited), one might heuristically prefer to first try assuming $a:A$.
   • Record $A$ and the choice (e.g., assuming $A$) as a new decision point.
   • Branch 1 (Assume $A$ true):
     • Create $\Gamma' = \Gamma, a:A$ (where $a$ is a fresh name for the assumption).
     • Recursively continue the process from Step 2 (Propagation Phase) with context $\Gamma'$ and goal $G$.
   • Branch 2 (If Branch 1 led to conflict and backtracking to this point):
     • The decision to assume $a:A$ is already marked as flipped (or this is the second attempt after $a:A$ failed).
     • Create $\Gamma'' = \Gamma, na:A \rightarrow \bot$ (where $na$ is fresh).
     • Recursively continue the process from Step 2 (Propagation Phase) with context $\Gamma''$ and goal $G$.
   • If both branches from this decision point eventually lead to conflict and backtrack here, then this decision point itself leads to UNSAT. Backtrack further.

Relevance to Classical DPLL

• Propositional Variables $\leftrightarrow$ Atomic Types: $P, Q, \dots$
• Literals $\leftrightarrow$ Literal Types: $P$ or $\neg P \leftrightarrow A$ or $A \rightarrow \bot$.
• Clauses $\leftrightarrow$ Sum Types: $(L_1 \lor L_2) \leftrightarrow L_1' + L_2'$.
• CNF Formula $\leftrightarrow$ Product of Sum Types: $(C_1 \land C_2) \leftrightarrow C_1' \times C_2'$.
• Assignment $\leftrightarrow$ Assumptions in Context $\Gamma$: $\{P=\text{true}, Q=\text{false}\} \leftrightarrow \{p:P, nq:Q \rightarrow \bot\} \subseteq \Gamma$.
• Satisfiability $\leftrightarrow$ Inhabitability: Finding a satisfying assignment $\leftrightarrow$ finding a context $\Gamma$ and term $t$ such that $\Gamma \vdash t:G_0$.
• Unit Propagation $\leftrightarrow$ Sum Consequence / Disjunct Elimination: If a sum type $A+B$ must be inhabited and we know $A \rightarrow \bot$, we must inhabit $B$.
• Boolean Constraint Propagation (BCP): The Propagation Phase aims to achieve a similar effect to BCP, deriving as many consequences as possible from current decisions before making a new one.
• Backtracking: Handled by undoing context additions and trying alternative branches for decisions.

This type-theoretic interpretation provides a constructive view of satisfiability. A "satisfying assignment" corresponds to the set of assumptions needed to construct a proof term for the type representing the formula. The process of [[mention:Beta Reduction|beta-reduction]] is crucial for evaluating the consequences of assumptions, especially when functions (like negations $A \rightarrow \bot$) are applied.
This framework can be naturally extended to more expressive logics by using richer type theories (e.g., Martin-Löf Type Theory for constructive predicate logic).

Paper Link: Here

Summary

Summary generated by Gemini 2.5 Pro Preview 03-25:

Comprehensive overview of the paper "Alloy*: A General-Purpose Higher-Order Relational Constraint Solver":

Core Problem:
The paper addresses the limitation of most constraint solvers, which are primarily restricted to first-order logic. While extremely useful, they struggle with problems inherently requiring higher-order quantification (quantifying over functions or relations), such as program synthesis or finding optimal structures (like a maximum clique in a graph). These tasks often involve patterns like "exists a structure P such that for all inputs I, property S holds" (∃∀). Currently, such problems are typically solved using domain-specific algorithms that embed a first-order solver (like SAT or SMT) within a loop, often implementing strategies like CounterExample-Guided Inductive Synthesis (CEGIS). This approach lacks generality and requires ad-hoc implementations for each new higher-order problem.

Proposed Solution: Alloy*
The paper introduces Alloy*, a novel constraint solver designed to handle higher-order relational logic directly. It extends the existing first-order bounded relational model finder Alloy (and its backend engine Kodkod) to support higher-order quantifiers natively within the Alloy language.

Key Concepts and Mechanisms:

1. Higher-Order Quantification: Alloy* allows higher-order quantifiers (quantifying over relations, which represent sets of tuples or functions in Alloy) to appear anywhere the Alloy syntax permits.
2. Generalized CEGIS: Instead of users implementing CEGIS externally, Alloy* internalizes a general-purpose CEGIS strategy to solve formulas involving the crucial ∃∀ quantifier pattern, which is common in higher-order problems.
3. Formula Decomposition: Alloy* analyzes an input formula (potentially with nested higher-order quantifiers) and decomposes it into a tree of subproblems. Each node in this tree represents either:
   • A first-order formula (solved directly by Kodkod).
   • A disjunction involving at least one higher-order part (solved by trying disjuncts).
   • An ∃∀ higher-order pattern (solved using the internal CEGIS loop).
4. CEGIS Loop in Alloy:* For ∃∀ formulas (∃p ∀e. S(p, e)):
   • Search: Find a candidate instance for p satisfying S(p, e) for some e.
   • Verify: Attempt to find a counterexample e such that S(p, e) fails for the candidate p. This involves solving ∃e. ¬S(p, e).
   • Induce: If a counterexample e_cex is found, add the constraint S(p, e_cex) to the search step and repeat. If no counterexample is found, the candidate p is a valid solution.
5. Leveraging First-Order Solver Features: The framework relies on the underlying first-order solver (Kodkod) supporting features crucial for efficient CEGIS: partial instances (fixing parts of the model), incremental solving (adding constraints without restarting), atom-to-expression conversion (encoding counterexamples as constraints), and skolemization.
6. Optimizations: The authors introduce optimizations like "Quantifier Domain Constraints" (using a when clause to prune the search space in CEGIS) and "Strictly First-Order Increments" (ensuring counterexample constraints are first-order to leverage incremental SAT solving).

Evaluation:
Alloy* was evaluated on two main fronts:

1. Classical Graph Algorithms: Problems like max-clique, max-cut, etc., which have natural higher-order formulations. Alloy* scaled reasonably well, handling graphs up to 50 nodes for most problems within modest time limits, demonstrating feasibility for modeling and bounded verification.
2. Program Synthesis (SyGuS): Alloy* was used to encode and solve a large subset of the Syntax-Guided Synthesis competition benchmarks. It performed competitively, scaling better than the reference synthesizers provided with the competition and even rivaling Sketch (a state-of-the-art synthesizer) on some benchmarks, despite being a general-purpose tool.

Contributions:

• A framework for extending first-order solvers to handle higher-order logic generally.
• A concrete implementation, Alloy*, extending Alloy/Kodkod.
• Demonstration of its feasibility and competitive performance across different domains (graph algorithms, program synthesis) via case studies and benchmarks.
• The identification and implementation of a generalized CEGIS strategy within a constraint solver.
• A publicly released implementation for broader use.

Conclusion:
The paper argues that just as factoring out first-order solving into reusable SAT/SMT solvers advanced the field, factoring out higher-order solving into general-purpose tools like Alloy* could bring similar benefits. It presents Alloy* as the first general-purpose, bounded, sound, and complete (for the given bounds) higher-order relational constraint solver, suggesting that the time is ripe to treat higher-order constraint solving as a reusable component rather than requiring ad-hoc solutions for each problem.

In logic, an assignment (or valuation, interpretation) is a function that maps variables within a given logical formula to values.

For example, in propositional logic, propositional variables are mapped to truth values of true or false.

Assignments can be used to evaluate the truth value of a complex formula. A satisfying assignment is one that makes a formula evaluate to true.

An axiom is a rule of inference with zero premises, meaning it is assumed to be true because it follows from nothing.

For example:

$$\frac{}{\Gamma \vdash \text{True}}\text{true}$$

Read: True can be derived as a constant from any context or even no context.

A boolean is a type with two terms: true and false.

The Brouwer-Heyting-Kolmogorov interpretation (source) is an "interpretation" of intuitionistic logic. It defines truth constructively, meaning a proposition is true only if we can construct a proof of it. It follows that both the law of the excluded middle and double negation elimination are rejected, as the former claims every mathematical proposition or its inverse has a proof, and the latter claims that every consistent (i.e. doesn't lead to a contradiction) mathematical statement holds. Basically, in the BHK interpretation, "proving" things is much more concrete, and therefore, it is harder to do, but more useful.

This way of looking at truth and proof corresponds cleanly with dependent types, since they require the same amount of constructive evidence that the BHK interpretation demands. They naturally model quantified statements and logical implications as types.

This is in contrast to Tarskian semantics, championed by Alfred Tarksi, which defines truth in terms of correspondence with an model. In other words, every proposition is true or false, regardless of our ability to prove it, determined by the "model" (see Theory link) applied to the symbols used. This is the basis of classical logic, which explains why strict dependent types are unintuitive from this perspective.

Implementations of the BHK interpretation include Implicational Intuitionistic Propositional Logic, Intuitionistic Propositional Logic, but most commonly and foundationally, Martin-Lof Type Theory.

The call-with-current-continuation (CWCC) operator, commonly abbreviated as call/cc, is a control flow operator found in some programming languages and type theories. It allows a program to capture its own execution state (the "rest of the computation" or "continuation") at a particular point and resume it later, potentially multiple times or not at all.

In pseudocode, CWCC has the following type.

• call/cc : {A,B : Type} ((A -> B) -> A) -> A
  • Or logically, it is a proof of the following proposition: $\text{call/cc} : \forall A, B. ((A \rightarrow B) \rightarrow A) \rightarrow A$

When call/cc is invoked, it is given a function, let's call it handler_fn. call/cc then calls handler_fn, passing it a special function representing the current continuation, let's call this k.

• handler_fn: A function that takes the current continuation k as its argument.
• k (the continuation): A function that represents the entire rest of the computation from the point call/cc was called. If k is ever called with a value v, the computation immediately jumps back to where call/cc was invoked, and the call/cc expression itself evaluates to v. Any computation that was pending within handler_fn after k was invoked is discarded.

Type Theoretic Perspective

In type theory, particularly in systems aiming to incorporate classical logic via the Curry-Howard Correspondence, call/cc is often introduced with a type equivalent to Peirce's Law:

$\forall A, B. ((A \rightarrow B) \rightarrow A) \rightarrow A$

This type signature is powerful. It essentially states: "For any types $A$ and $B$, if you can produce an $A$ by assuming you have a function that can turn an $A$ into a $B$ (the continuation $k: A \rightarrow B$), then you can produce an $A$."

This allows the derivation of classical logical principles that are not typically provable in intuitionistic systems. The empty type ($\bot$), representing falsehood, plays a crucial role when $B$ is instantiated as $\bot$.

A negation $\neg P$ is typically defined as $P \rightarrow \bot$.

Correspondence to Double Negation Elimination

[[mention:Double Negation Elimination]] (DNE) states that $\neg \neg P \rightarrow P$. In type theory, this is $(((P \rightarrow \bot) \rightarrow \bot) \rightarrow P)$. call/cc allows us to construct a term of this type.

Derivation Sketch:

1. Goal: Construct a term for $(((P \rightarrow \bot) \rightarrow \bot) \rightarrow P)$.
2. Assume: We are given $proof_{\neg\neg P} : ((P \rightarrow \bot) \rightarrow \bot)$.
3. Use call/cc: We instantiate call/cc with type $A=P$ and $B=\bot$. So, call/cc has the type $((P \rightarrow \bot) \rightarrow P) \rightarrow P$.
4. Argument for call/cc: call/cc expects a function of type $(P \rightarrow \bot) \rightarrow P$. Let's call this function g.
   • g takes an argument $k_P : P \rightarrow \bot$. This $k_P$ is the continuation captured by call/cc. If $k_P$ is called with a value of type $P$, the call/cc expression will evaluate to that value, but the context implies $k_P$ leads to $\bot$.
   • Inside g, we have:
     • $proof_{\neg\neg P} : ((P \rightarrow \bot) \rightarrow \bot)$ (our initial assumption)
     • $k_P : P \rightarrow \bot$ (the continuation)
   • We can apply $proof_{\neg\neg P}$ to $k_P$: $proof_{\neg\neg P}(k_P)$ yields a term of type $\bot$.
   • From $\bot$, we can derive any type, including $P$. This is done using the principle of ex falso quodlibet, often embodied by a term like $\text{absurd}_P : \bot \rightarrow P$.
   • So, $\text{absurd}_P(proof_{\neg\neg P}(k_P))$ is a term of type $P$.
   • Thus, $g = \lambda k_P : (P \rightarrow \bot). \text{absurd}_P(proof_{\neg\neg P}(k_P))$. This function $g$ has type $(P \rightarrow \bot) \rightarrow P$.
5. Result: $\text{call/cc}(g)$ is a term of type $P$.

The complete term for DNE is:
$\lambda proof_{\neg\neg P} : ((P \rightarrow \bot) \rightarrow \bot). \text{call/cc}(\lambda k_P : (P \rightarrow \bot). \text{absurd}_P(proof_{\neg\neg P}(k_P)))$

This demonstrates how call/cc provides a constructive path (in terms of term construction) to DNE.

Correspondence to Law of the Excluded Middle

The Law of the Excluded Middle (LEM) states $P \lor \neg P$. In type theory, using sum types ($+$) for disjunction, this is $P + (P \rightarrow \bot)$.

Derivation Sketch:

1. Goal: Construct a term for $X \equiv P + (P \rightarrow \bot)$.
2. Use call/cc: We instantiate call/cc with type $A=X$ and $B=\bot$. So, call/cc has the type $((X \rightarrow \bot) \rightarrow X) \rightarrow X$.
3. Argument for call/cc: call/cc expects a function of type $(X \rightarrow \bot) \rightarrow X$. Let's call this function g.
   • g takes an argument $k_X : X \rightarrow \bot$. This $k_X$ is the continuation. ($k_X$ means "assuming $P \lor \neg P$ leads to contradiction").
   • Inside g, we want to produce $X$. We can try to produce the $\neg P$ part of $X$, which is $P \rightarrow \bot$.
     • To construct $P \rightarrow \bot$, we assume a hypothetical $p_{hypo} : P$.
     • With $p_{hypo}$, we can form $\text{inl}(p_{hypo}) : P + (P \rightarrow \bot)$. This is a term of type $X$.
     • Now apply the continuation $k_X$: $k_X(\text{inl}(p_{hypo}))$ yields a term of type $\bot$.
     • So, the function $\lambda p_{hypo} : P. k_X(\text{inl}(p_{hypo}))$ is a term of type $P \rightarrow \bot$. Let this be $proof_{\neg P}$.
   • Now we can construct the right side of the sum: $\text{inr}(proof_{\neg P}) : P + (P \rightarrow \bot)$. This is a term of type $X$.
   • Thus, $g = \lambda k_X : ((P + (P \rightarrow \bot)) \rightarrow \bot). \text{inr}(\lambda p_{hypo} : P. k_X(\text{inl}(p_{hypo})))$. This function $g$ has type $((P + (P \rightarrow \bot)) \rightarrow \bot) \rightarrow (P + (P \rightarrow \bot))$.
4. Result: $\text{call/cc}(g)$ is a term of type $P + (P \rightarrow \bot)$.

This shows that call/cc (which embodies Peirce's Law) is sufficient to prove LEM.

Role in Classical Type Theories

The call/cc operator is a key ingredient in forming a Classically Typed Lambda Calculus. By adding call/cc to an intuitionistic type theory, one gains the ability to prove classical tautologies like LEM and DNE, making the logic of the type theory classical.

Its inclusion allows for reasoning by contradiction and other classical proof techniques to be directly represented as programs (terms) within the type system.

The CDCL algorithm is a satisfiability solver for propositional formulae.
It is an improvement on the DPLL algorithm that enables more efficient traversal of the search space via learning clauses. This improvement enables CDCL to be the basis of most modern high-performance SAT solvers.

How it Works

Input

• A Propositional Formula in Conjunctive Normal Form

Output

• A Satisfying Assignment or an indication of unsatisfiability.

Process
CDCL refines DPLL by incorporating several key techniques:

1. Decision Making (Branching):

   • Similar to DPLL, if no direct implications (like unit propagation) can be made, the algorithm chooses an unassigned variable (the decision variable) and assigns it a truth value (e.g., True). This is a decision level.
   • Sophisticated heuristics (e.g., VSIDS - Variable State Independent Decaying Sum) are used to select decision variables that are likely to lead to conflicts or solutions quickly.

2. Boolean Constraint Propagation (BCP) (Unit Propagation):

   • After a decision (or learning a new clause), BCP is performed. This is identical to unit propagation in DPLL: if a clause becomes a unit clause (all literals but one are false under the current assignment), the remaining literal must be assigned a value to make the clause true.
   • This process is repeated iteratively until no more unit clauses are found or a conflict is detected.
   • Efficient data structures (e.g., two-watched literals) are crucial for fast BCP.

3. Conflict Analysis and Clause Learning:

   • If BCP leads to a conflict (i.e., a clause becomes false under the current assignment, e.g., (A ∨ B) where A is False and B is False), the algorithm does not simply backtrack to the most recent decision.
   • Instead, it analyzes the implication graph that led to the conflict to identify the assignments responsible.
   • From this analysis, a new clause, called a learned clause (or conflict clause), is generated. This clause is redundant (implied by the original formula) but prunes the search space by preventing the same conflicting assignment combination from being explored again.
   • The learned clause is typically an asserting clause: at some backtrack level, it will become a unit clause, forcing a variable assignment.

4. Non-Chronological Backtracking (Backjumping):

   • When a conflict occurs and a conflict clause is learned, the algorithm backtracks.
   • Instead of backtracking to the immediately preceding decision level (chronological backtracking), CDCL backtracks to the most recent decision level that is actually involved in the conflict, as determined by the conflict analysis. This level is often much earlier in the decision stack, allowing the solver to jump over irrelevant parts of the search space.
   • The learned clause is designed to become unit at the backtrack level, guiding the search.

5. Restarts:

   • Periodically, the solver may discard the current partial assignment and restart the search from the beginning, while keeping the learned clauses.
   • Restarts help to escape "stuck" regions of the search space and can improve overall performance, often guided by restart policies (e.g., Luby sequence).

6. Literal Phase Heuristics:

   • When making a decision, heuristics can also decide which phase (True or False) to assign to the variable first. Some solvers remember the last satisfying phase (phase saving).

The algorithm terminates when one of the following conditions is met:

• Satisfiable: If the decision process leads to an assignment where all original clauses are satisfied, the formula is satisfiable.
• Unsatisfiable: If conflict analysis at decision level 0 (no decisions made, only propagations from original unit clauses or learned clauses) derives an empty clause (a conflict), the formula is unsatisfiable.

Relevance

CDCL algorithms are significantly more powerful than basic DPLL, especially on large, structured industrial instances. The combination of clause learning, non-chronological backtracking, and efficient BCP allows them to navigate vast search spaces effectively. They are the core engine in many SMT solvers and have applications in AI, formal verification, and other areas.

A Classic Dependently Typed Lambda Calculus (CDTLC) refers to a type theory that extends a dependently-typed lambda calculus with some axiom that embodies the Law of the Excluded Middle, such as the call/cc operator. It can be seen either as a classical extension of a dependently typed lambda calculus, or as a dependently typed extension of a classically typed lambda calculus.

When adding classical axioms, DTLC (now CDTLC) becomes equivalent in some sense to first order logic via the Curry-Howard correspondence. Under this equivalence propositions in classical first order logic correspond to types in CDTLC, and classical proofs correspond to terms in CDTLC.

This allows for the formalization of classical mathematics and reasoning within a typed lambda calculus framework, potentially leveraging the computational interpretations of proofs, though the constructive nature of evidence found in intuitionistic systems cannot be expected universally.

The classically typed lambda calculus (CTLC) is the intuitionistically typed lambda calculus together with an operator called call/cc or call-with-current-continuation which enables control flow manipulation and also just happens to correspond to the law of the excluded middle.

Due to the addition of LEM, CTLC directly corresponds to propositional logic via the Curry-Howard Correspondence.

A computable function is a function for which there exists an algorithm or a model of computation (like a turing machine or lambda calculus) that can determine the output for any given valid input in a finite amount of steps.

Conjunctive normal form is a specific constraint on the structure of a logical formula, often specifically referring to a propositional formula.

A formula in CNF is a conjunction of clauses, where each clause is a disjunction of propositional literals.

A context-free grammar is a formal grammar where the classification function is restricted to the set of programs simulatable by a finite state machine and a stack, i.e. a deterministic pushdown automaton.

Continuation-passing style (CPS) or the Continuation-Passing Style Transformation (CPST) is an alternative way to write expressions that allows precise management of what is done with the result of a function evaluation. It essentially adds an extra parameter to each function which the function then calls with whatever it wanted to return originally. The calling function then determines what gets done with the result.

A small example:

Direct Style:

def add(x, y):
  return x + y

result = add(5, 3)
print(result)  # Output: 8

Continuation-Passing Style:

def add_cps(x, y, continuation):
  continuation(x + y)

def print_result(result):
  print(result)

add_cps(5, 3, print_result)  # Output: 8

This transformation can even be done multiple times to the same program. Here's the CPST done twice:

def add_cps(x, y, continuation_inner): # Renamed for clarity
  result = x + y
  continuation_inner(result)

# 2-CPS version of add_cps_original
def add_2cps(x, y, continuation_inner_arg, continuation_outer):
  def intermediate_continuation_for_add_cps(value_from_add_cps):
    continuation_outer(value_from_add_cps)
  add_cps_original(x, y, intermediate_continuation_for_add_cps)

def print_result_cps_cps(value):
  print(value)

def original_intended_continuation_for_add_cps(value):
    print(f"(This was 'continuation_inner_arg' for add_2cps: {value}) - usually not directly called in this setup")

add_2cps(5, 3, original_intended_continuation_for_add_cps, print_result_cps_cps) # Output: 8

This double version doesn't really seem that useful in practice though.

Continuation Passing Style Transformation (the single version) is useful for compilers for certain kinds of optimization, as well as for providing the conceptual basis for continuations and the [[mention: call with current continuation]] operator, leading the way to formalize classical theorems in intuitionistic type theory.

Fun Fact: When modeling a programming language as a category where the types are objects and the morphisms are terms, the CPST corresponds to a specific case of the yoneda embedding.

The Curry-Howard correspondence (also known as the Curry-Howard isomorphism or the proofs-as-programs paradigm) proposes some kind of relation between logical frameworks and type theories.

It establishes a direct correspondence between:

• Propositions and types: A logical proposition corresponds to a type in some type theory.
• Proofs and programs: A proof of a proposition corresponds to a program of the corresponding type.
• Proof simplification and program evaluation: The process of simplifying a proof (cut elimination) corresponds to the process of evaluating a program ($\beta$-reduction).

A data type is a variant of a type, that is used to classify different kinds of data, as opposed to logical statements.

Examples include Boolean, List, and inductively-defined term types such as those representing Lambda Calculus expressions.

The DPLL algorithm is an algorithm for propositional satisfiability solving. It is a backtracking-based search algorithm designed to determine the satisfiability of a propositional formula in conjunctive normal form (CNF).

How it Works

The algorithm systematically explores the space of all possible combinations of truth assignments for each of the variables in the formula. It operates through a recursive/iterative process described as follows:

Input

• A Propositional Formula in Conjunctive Normal Form

Output

• A Satisfying Assignment or an indication of unsatisfiability.

Process

• Initialize an empty list of assignments.
  • Assignments are distinguished as either decision or propagation assignments
• Represent the CNF formula as a set of clauses. Clauses are sets of literals.

  • Literals are variables like $A$ or their negations like $\neg A$.

  • Clauses represent disjunctions (ORs): e.g., $A \lor \neg B \lor C \equiv \{A, \neg B, C\}$.

  • The formula is a conjunction (AND) of these clauses: e.g., $(A \lor \neg B) \land (C \lor B) \equiv \{\{A, \neg B\}, \{C, B\}\}$.

  • The formula data structure must support efficient modifications and allow changes to be rolled back, i.e. by cloning for recursive calls or by maintaining a change log.

  • Simplify & Check UNSAT

    • Removes atoms that are assigned to true, if an atom is the only one left in a clause when set to true it removes the clause as well.
    • Removes atoms in clauses that are assigned to false. Rollback to last decision clause and assign it the other way. If no decisions left to reverse, return UNSAT
    • If all clauses have been removed, return SAT with current assignment.
• Repeatedly do one of the following, whichever one can be done first:
  • Unassigned Atom Elimination: If there is a clause with only one atom that is not already assigned in the assignment:
    • Add to assignment list whatever is needed to make that atom true (and thus the resulting clause true). Simplify & Check UNSAT
  • Non-Conflicting Atom Elimination: If a variable only appears in the form $P$ or only appears as $\neg P$,:
    • Assign the variable to true if the variable appears as $P$ everywhere, false otherwise. Simplify and Check UNSAT
  • Branch:
    • Add an decision assignment to the assignment list. Simplify and Check UNSAT

Relevance

DPLL has been surpassed by CDCL at this point, but it is a good basis for learning about SAT solving algorithms and CDCL builds off of DPLL to some degree, so its a good toy model.

Paper Link: Here

Summary

Summary generated by Gemini 2.5 Pro Preview 05-06:

The document focuses on "Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays" (page 1). It details both the theoretical underpinnings and practical implementation aspects, particularly within the SMT solver Boolector.

I. Theory of Arrays (primarily from Chapter 2)

1. Definition and Axioms (page 11, Section 2.2):

   • The document discusses the extensional theory of arrays, which allows reasoning about array elements and entire arrays (array equality).
   • The signature ΣA includes read, write, and =.
   • read(a,i) returns the value of array a at index i.
   • write(a,i,e) returns a new array, identical to a except at index i where it holds element e.
   • McCarthy's Axioms are fundamental:
     • (A1) Congruence: i = j ⇒ read(a,i) = read(a,j)
     • (A2) Read-over-write (same index): i = j ⇒ read(write(a,i,e),j) = e
     • (A3) Read-over-write (different index): i ≠ j ⇒ read(write(a,i,e),j) = read(a,j)
   • Axiom of Extensionality is crucial for array equality:
     • (A4) a = b ⇔ ∀i(read(a,i) = read(b,i))
     • An alternative form (A4') is given for quantifier-free contexts: a ≠ b ⇔ ∃λ (read(a,λ) ≠ read(b,λ)), meaning unequal arrays must differ at some witness index λ (page 12).
   • The quantifier-free fragment is denoted TA.

2. Decision Procedure DPA (pages 17-33, Sections 2.6, 2.7):

   • A novel decision procedure DPA for the quantifier-free extensional theory of arrays combined with a base theory TB (e.g., bit-vectors) is presented.
   • Preprocessing (page 13, Section 2.4):
     • For each array inequality a ≠ c, a witness constraint based on (A4') is added: a ≠ c → ∃λ. read(a,λ) ≠ read(c,λ).
     • For each write(a,i,e), the constraint read(write(a,i,e),i) = e (from A2) is added. These make the formula equisatisfiable (page 14).
   • Formula Abstraction (page 15, Section 2.5): read operations are replaced by fresh abstraction variables, and array equalities by fresh propositional variables, creating an over-approximation α(π).
   • Abstraction Refinement Loop (page 17, Section 2.6):
     • DPB (decision procedure for the base theory) solves α(π) ∧ ξ (where ξ are refinement lemmas).
     • If a model σ is found, a consistency checker (page 18, Section 2.7) determines if σ corresponds to a valid model in TA.
     • Read Propagation (pages 21, 27): A mapping ρ tracks reads associated with array terms. Reads are propagated:
       • Downwards through writes (Rule D, page 21): If σ(α(i)) ≠ σ(α(j)), read(b,i) is propagated from write(a,j,e) to a.
       • Across array equalities (Rules R, L, page 27): If σ(α(a=c)) is true, reads are propagated between a and c.
       • Upwards from arrays through writes (Rule U, page 27): If σ(α(i)) ≠ σ(α(j)), read(b,i) from a is propagated to write(a,j,e). This respects axiom (A3).
     • Lemma Generation: If an inconsistency (e.g., violation of adapted congruence axiom (A1), see page 22) is found, a lemma based on the propagation path conditions is generated and added to ξ. These lemmas are TA-valid (page 34, Section 2.8).
   • The procedure is proven sound (page 34) and complete (page 39).
   • Complexity: The number of lemmas is bounded by O(n² · 2ⁿ) (page 43).

3. Implementation Details for Arrays in Boolector:

   • Treating Writes as Reads (page 47, Section 2.11.4; page 61): A write(a,i,e) can be implicitly treated as a read on itself for index i, returning e. This avoids the explicit preprocessing step of adding read(write(a,i,e),i)=e.
   • Unconstrained Array Variables (page 75, Section 3.4.2):
     • read(a,i) where a is unconstrained is rewritten to a fresh variable.
     • write(a,i,v) where a and v are unconstrained is rewritten to a fresh array variable.
     • a = t where a is unconstrained is rewritten to a fresh boolean variable.

II. Theory of Bit-Vectors (primarily from Chapter 3 and Appendix A)

1. General Handling:

   • Boolector primarily uses term rewriting and bit-blasting for bit-vectors (page 62).
   • The BTOR format supports bit-vector variables, constants (decimal, hex, binary), and operations with arbitrary bit-width (page 127, 129).
   • Semantics largely follow SMT-LIB QF_BV (page 129).
   • A key distinction: division by zero in BTOR results in the largest unsigned integer (page 129).

2. Under-Approximation Techniques (pages 65-68, Section 3.3):

   • Aimed at speeding up satisfiable instances and producing "smaller" models by restricting bit domains.
   • Techniques (page 66):
     • Sign-extension: Most significant bits are forced equal to the (n-1)th bit (last effective bit).
     • Zero-extension/One-extension: Most significant bits are forced to 0 or 1.
     • Bit-partitioning: Bits are partitioned into equivalence classes, with all bits in a class having the same value (page 67).
   • CNF Layer Implementation (page 67, Section 3.3.1): Under-approximations are added as incremental clauses to the SAT solver, controlled by a fresh boolean assumption variable e. Refinement involves disabling e and introducing a new approximation with a new assumption variable (page 68).
   • Early Unsat Termination (page 69, Section 3.3.3): If the under-approximated formula is unsatisfiable without using the assumption variable e, the original formula is unsatisfiable.

3. Unconstrained Bit-Vector Variables (page 72, Section 3.4.1):

   • If an operand v of a function f is unconstrained (appears only once) and f is "invertible" with respect to v, then f(...) can be replaced by a fresh bit-vector variable.
   • Example: v3 + t = v1 & v2. If v1, v2 are unconstrained, v1 & v2 can be replaced by v4. If v3 is unconstrained, v3 + t can be v5. The formula becomes v4 = v5 (page 74).
   • Corner cases exist (e.g., multiplication by an even constant, v < 000) where this is not sound (page 75).

4. Symbolic Overflow Detection (pages 77-84, Section 3.5):

   • Boolector directly supports symbolic overflow predicates for fixed-size bit-vector arithmetic (add, subtract, multiply, divide) in two's complement.
   • Addition (page 78):
     • Unsigned: Carry-out of MSB c[n-1] is 1. Implemented by adding operands extended with a 0-bit and checking the new MSB r[n].
     • Signed: (Operands have same sign) AND (result has different sign), or c[n-1] ⊕ c[n-2] (page 79).
   • Subtraction (page 79): a - b as a + (-b).
     • Unsigned: Overflow if c[n-1] (from the addition a + (-b)) is 0.
     • Signed: Defined by specific cases of operand signs and result sign.
   • Multiplication (page 80): Considers an n+1 bit product r.
     • Unsigned: (Sum of leading zeros in a and b, Za + Zb) < n-1 OR r[n] is 1. A "leading zeros examination principle" is detailed (Figure 3.8, page 81; formula page 82).
     • Signed: (Sum of leading bits L(a) + L(b)) < n OR r[n] ⊕ r[n-1] is 1. A "leading bits examination principle" is detailed (Figure 3.9, page 83; formula page 84).
   • Division (page 84):
     • Signed: Overflow only if the smallest representable integer is divided by -1.
     • Unsigned: Never overflows.

5. BTOR Format for Bit-Vectors (pages 129-131, Appendix A.2):

   • Lists unary (not, neg, redand, inc, etc.), binary (and, add, mul, eq, sll, uaddo, etc.), ternary (cond), and miscellaneous (slice) operators with their bit-width specifications.
   • Includes Verilog reduction operators, VHDL rotate operators, and specific overflow detection operators (e.g., umulo).

This summary covers the main theoretical aspects of bit-vectors and arrays as presented in the dissertation, including their formal definitions, the decision procedures developed, and key implementation strategies related to these theories within Boolector.

The empty type, denoted as $\bot$, Void, Never, 0, or ! is a type that contains no terms. It is impossible to construct an instance (i.e. inhabitant) of the empty type.

Under the Curry-Howard Correspondence (BHK interpretation), the empty type corresponds directly to falsity. Just as there is no proof for the proposition false, there are no inhabitants (values) for the empty type. A function that claims to return the empty type (e.g., f : A -> Void) signifies that the function can never actually be called with a valid value of type A (if the system is consistent), or that it never terminates normally (e.g., it loops forever or throws an exception). This is how negation is defined, as the existence of a function from ParseError: KaTeX parse error: Undefined control sequence: \rarrow at position 3: A \̲r̲a̲r̲r̲o̲w̲ ̲Void implies that it can never be evaluated, meaning that A must also be an empty type and therefore false.

Set-theoretically it can be thought of as the empty set.

The existential quantifier, denoted by the symbol $\exists$ (a left-to-right reflected "E"), is a type of quantifier used in first-order logic and other predicate logics. It expresses that there is at least one member of the domain of discourse for which a certain property or relation holds.

The expression $\exists x. P(x)$ is read as "there exists an $x$ such that $P(x)$ is true" or "for some $x$, $P(x)$ holds."
Here, $P(x)$ is a predicate, and $x$ is a variable bound by the quantifier. The statement $\exists x. P(x)$ is true if and only if there is at least one value of $x$ from the domain for which $P(x)$ is true. If $P(x)$ is false for every value of $x$ in the domain, then $\exists x. P(x)$ is false.

Under the Curry-Howard correspondence, the existential quantifier $\exists$ corresponds to Σ-types (dependent pair types) in dependent type theory. A proof of $\exists x : A. P(x)$ is a pair consisting of a witness $a$ of type $A$ and a proof of $P(a)$.

An expression or term is a kind of well-formed formula, usually used in the context of programming languages and type theory. Expressions can represent a value to be computed, a computation process itself, or a proof of some statement. They can be assigned types, and the inhabitants of types.

Examples of terms:

• In lambda calculus: $x$, $λx.x$, $(f a)$
• In arithmetic: $x + 5$, $(y * 2) - z$
• In a programming language: $\text{add}(\text{arg1}, \text{arg2})$. $a + b$

False is one of the two terms of the boolean type, the other being true.

It is often used as a constant within propositional logic, commonly represented by the symbol $\bot$.

The Curry-Howard Correspondence establishes that programs are proofs and types are propositions. This suggests that techniques developed for automated theorem proving and finding proofs in logical systems, such as SAT/SMT solvers, could potentially be adapted to automatically finding or synthesizing programs that inhabit given types (i.e., satisfy type specifications).

A finite automaton is a model of computation that consists of a finite set of states and transitions between those states based on input symbols. It is the simplest model of computation, capable of recognizing of regular languages.

A First Order Logic (FOL) is a formal logic that builds on propositional logic (PL) in the sense that it is essentially propositional logic but with the additions of predicates and quantifiers. FOL collectively is an umbrella term for many theories such as Integer Arithmetic, Real Arithmetic, Bit-Vector, Array, and Set Theory. First Order Logic is generally assumed to be classical (i.e. assumes principles like the law of the excluded middle), and is thus equivalent to the classic dependently typed lambda calculus via the Curry-Howard Correspondence. Its constructive counterpart is Intuitionistic First Order Logic.

FOL adds the following structures to propositional logic, but the details of some of these structures depends on the specific FOL theory.

• Sorts (sets of things)
• Predicates: Express properties of objects or relationships between objects (e.g., $P(x)$, $R(x, y)$).
• Functions: Map objects to other objects (e.g., $f(x)$, $g(x, y)$).
• Quantifiers:
  • Universal Quantifier: $\forall x, P(x)$.
  • Existential Quantifier: $\exists x, P(x)$.

Examples:

• "All humans are mortal" $\rArr$ $\forall x. (\text{Human}(x) \rightarrow \text{Mortal}(x))$.
• "Joey and Jill can become friends with anyone" $\rArr \forall p : \text{Person}. (\text{CanBecomeFriendsWith(Joey, p)} \land \text{CanBecomeFriendsWith(Jill, p)})$.

A first order logic theory, is a formal system that extends first order logic with extra logical inference rules. These rules come in two flavors:

1. Signature ($\Sigma$): A set of non-logical symbols particular to the theory. This typically includes:

   • Constant symbols (e.g., $0, 1$ in arithmetic).
   • Function symbols (e.g., $+, \times$ in arithmetic, along ith their arities).
   • Predicate symbols (e.g., $\leq, =$ in arithmetic, along with their arities).
   • (Optionally, sorts if using many-sorted first-order logic, as seen in the examples within first order logic).
   • These can be thought of as Axioms.

2. A collection of ways to construct more complicated formulas from basic symbols. Expressed as more inference rules.

A structure is considered a model of a first-order theory if it provides an interpretation for the symbols in the signature such that all axioms of the theory are true under that interpretation. Intuitively, this should be some kind of "physical realization" of a theory.

Examples

Many specific logical systems are instances of first-order theories:

• Integer Arithmetic: Theory of Integer Arithmetic.
• Theory of Real Arithmetic: Theory of Real Arithmetic.
• Zermelo-Fraenkel Set Theory (ZFC)
• Theories used in SMT solvers, such as:
  • Arrays: Theory of Arrays.
  • Bit Vectors: Theory of Bit Vectors.
  • Uninterpreted Functions: Theory of Uninterpreted Functions.

A formal grammar is:

• A symbol set: A set of symbols $\Sigma$
• A characterizing function: A Function in some turing-complete model of computation that takes in a sequence of symbols and returns true or false depending on whether or not the sequence is valid within the grammar

A Formal Logic is a Formal System that provides the foundational syntax and rules of inference for constructing a logical system and their associated formulae.

Examples include Propositional Logic, Predicate Logic, also referred to as First Order Logic and various modal or temporal logics. Each logic allows reasoning about different kinds of statements and structures.

Conceptual Structure

Many formal logics can be conceptually characterized by:

1. Syntax
   • A description of what structures exist in the logic (true, false, symbols, quantifiers, etc.) and what constitutes a well-formed formula
2. Semantics
   • A way to assign truthity or falsity to well-formed formulas. This includes notions like logical assignment, satisfying assignment, a deductive system or set of rules of inference.

A Formal System is a general term that includes a set of Well-Formed Formulas, created by a Formal Grammar, and some kind of inference rule, either logical or type-theoretic.

Examples of formal systems include instances of Formal Logic and Type Theory.

A function is a mapping between two sets, a domain and a codomain, such that every element in the domain is associated with exactly one element in the codomain.

Functions can be specified in various ways, including explicit formulas, algorithms, or tables of values. Some functions can't be specified or computed, for those that do see: Computable Function.

Function types, denoted as $A \rightarrow B$, represent functions that take an argument of type $A$ and return a result of type $B$.

Logically via the Curry-Howard Correspondence function types can be interpreted as $A \rightarrow B$ or logical implication, meaning to prove $A \rightarrow B$ you need a proof that given a proof of $A$ you can construct a proof of $B$. Set-theoretically it can be interpreted as the set of functions from set $A$ to set $B$. In category theory function types correspond to exponential objects.

Implicational Intuitionistic Propositional Logic (IIPL) is an incredibly simple formal logic wherein logical sentences are constructed using propositional variables combined with only one connective: logical implication.

• Logical implication: $A \rightarrow B$

It is equivalent to the simply typed lambda calculus via the Curry-Howard Correspondence where every proposition and proof in IIPL corresponds to a type and term in STLC.

Intuitionistic First Order Logic (IFOL) is a Formal Logic that extends Intuitionistic Propositional Logic with quantifiers over individuals, but without assuming the Law of the Excluded Middle or its equivalents for quantified statements. It provides a constructive interpretation of logical connectives and quantifiers.

Differences from Traditional First Order Logic:

1. Constructive Existence: To prove $\exists x. P(x)$ in IFOL, one must provide a specific term $t$ (a witness) and a proof of $P(t)$. It's not enough to show that the non-existence of such an $x$ leads to a contradiction.
2. No Law of Excluded Middle for Quantifiers: The statement $\forall x. (P(x) \lor \neg P(x))$ is not generally a theorem in IFOL. Similarly, $\neg (\forall x. P(x)) \leftrightarrow (\exists x. \neg P(x))$ holds in one direction ($\exists x. \neg P(x) \rightarrow \neg \forall x. P(x)$) but the other direction ($\neg \forall x. P(x) \rightarrow \exists x. \neg P(x)$) is not generally provable.

Relationship to Type Theory

Intuitionistic First Order Logic is Martin-Lof Type Theory under the Curry-Howard Correspondence. Propositions in IFOL correspond to types in MLTT, and proofs in IFOL correspond to terms (programs) in MLTT.

Intuitionistic Propositional Logic (IPL) is a formal-logic that is a variant of propositional logic where the law of the excluded middle is not assumed as an axiom. IPL is an instance of Implicational Intuitionistic Propositional Logic with the following additional constructions:

• True: $\top$
• False: $\bot$
• Logical Conjunction: $A \land B$
• Logical Disjunction: $A \lor B$
• Logical Negation: $\neg A$

In IPL, a proposition is considered true only if there is a constructive proof for it. This means that to prove a statement or formula, one must provide a direct construction or evidence of its truth, rather than relying on the impossibility of its negation.

IPL is equivalent to intuitionistically-typed lambda calculus via the Curry-Howard Correspondence, where proofs in IPL correspond to terms in STLC and propositions correspond to types.

The Intuitionistically typed lambda calculus (ITLC) is a type theory and extension of simply-typed lambda calculus that, in addition to function types adds:

• Empty Types
• Unit Types
• Product Types
• Sum Types
• Negation: (can be constructed from Function type and Empty type)

The ITLC is not a standard term in the literature, but it does provide a core building block of other type theories.

It is equivalent to intuitionistic propositional logic via the Curry-Howard Correspondence where every type and term in ITLC corresponds to a proposition and proof in IPL.

Formally, the added rules can be described using the following sequent calculus declarations. (See more on the sequence calculus on the type theory page)

$$\frac{}{\Gamma \vdash () : \text{Unit}} \text{unit}$$

$$\frac{}{\Gamma \vdash \text{absurd} : \text{Void} \rightarrow A } \text{absurd}$$

$$\frac{\Gamma \vdash a : A \quad \Gamma \vdash b : B}{\Gamma \vdash (a,b) : A \times B} \text{pair}$$

$$\frac{\Gamma \vdash t : A \times B}{\Gamma \vdash \text{fst}(t) : A} \text{fst}$$

$$\frac{\Gamma \vdash t : A \times B}{\Gamma \vdash \text{snd}(t) : B} \text{snd}$$

$$\frac{\Gamma \vdash a : A}{\Gamma \vdash \text{inl}(a) : A + B} \text{in-left}$$

$$\frac{\Gamma \vdash b : B}{\Gamma \vdash \text{inr}(b) : A + B} \text{in-right}$$

$$\frac{\Gamma \vdash s : A + B \quad \Gamma \vdash f : A \rightarrow C \quad \Gamma \vdash g : B \rightarrow C}{\Gamma \vdash \text{case}(s, f, g) : C} \text{case}$$

The lambda calculus (λ-calculus) is a particular type of expression or more broadly, a well-formed formula in some formal grammar that encodes computation using function abstraction, variable binding, application, and substitution.

It is a universal Model of Computation, equivalent in power to Turing machines.

Fun fact: when implementing the lambda calculus, it can be encoded as a data type like as follows:

enum LambdaExpression {
	Variable { name : String }
	Abstraction { bound : String, body: LambdaExpression }
	Application { left: LambdaExpression, right: LambdaExpression }
}

The law of the excluded middle (LEM) is an (optional) axiom in logic presupposes that there is no "3rd value" between any proposition $A$ or $\neg A$.

Formally, it can be expressed as:

$A \lor \neg A$

This principle is a key difference between intuitionistic propositional logic and propositional logic.

A list (or sequence) is an abstract data type representing a finite, ordered collection of items where the same item may occur multiple times.

Logical conjunction is a binary logical operation typically meaning "and". In Propositional Logic, the conjunction of two formulae $A$ and $B$, written $A \land B$, is True if and only if both $A$ and $B$ are true; it is False otherwise.

The truth table for logical conjunction is:

Logical disjunction, a.k.a. "or", is a binary logical operation. In Propositional Logic, the disjunction of two formulae $A$ and $B$, written $A \lor B$, is True if at least one of $A$ or $B$ is true, and False otherwise.

The truth table for logical disjunction is:

A logical formula is a well-formed formula associated with a formal logic, and can usually be interpreted as either true or false, potentially with respect to some assignment.

It is equivalent to a type from type theory.

Logical implication is a binary logical operation encoding the idea of "if... then...". In Propositional Logic, the implication $A \rightarrow B$ is False only when $A$ is True and $B$ is False; it is true in all other cases.

The truth table for logical implication is:

Logical negation is a unary operation that reverses the truth value of a proposition. In Propositional Logic, the negation of a formula $A$, written $\lnot A$, is True if $A$ is False, and False if $A$ is True.

The truth table for logical negation is:

Martin-Lof Type Theory (MLTT) is a foundational Type Theory developed by Per Martin-Lof that builds on the simply typed lambda calculus by adding dependent types, identity, types, universe types, and inductive types. It serves as a basis for modern proof assistants like Lean, Agda and Coq.

MLTT adds the following to the simply typed lambda calculus (some of it doesn't just add but also replaces).

• Dependent Types: Types that can depend on values.

  • Π-types (Dependent Function Types): Generalizes function types. If $B(x)$ is a type for each $x:A$, then $\Pi x:A. B(x)$ is the type of functions that take an $x$ of type $A$ and return a term of type $B(x)$. This corresponds to universal quantification ($\forall x. P(x)$) under the Curry-Howard Correspondence.
  • Σ-types (Dependent Pair Types): Generalizes product types. If $B(x)$ is a type for each $x:A$, then $\Sigma x:A. B(x)$ is the type of pairs $(a,b)$ where $a:A$ and $b:B(a)$. This corresponds to existential quantification ($\exists x. P(x)$) under the Curry-Howard Correspondence.

• Identity Types ($Id_A(x,y)$ or $x =_A y$): A type representing the proposition that $x$ is equal to $y$ (where $x, y : A$). Proofs of identity are terms of this type.

• Universe Types ($U_0, U_1, \dots$): Types whose terms are themselves types. This allows for type-level computation and reasoning about types, forming a hierarchy to avoid paradoxes.

• Inductive Types: Rich ways to define data types like natural numbers, lists, trees, etc., along with their principle of induction.

MLTT is inherently constructive. A proof of a proposition (represented as a type) is a program (a term inhabiting that type). For example, to prove an existentially quantified statement (a Σ-type), one must construct a term to "inhabit" the existential type and prove that the existential property is true.

It is related to Intuitionistic First Order Logic via the Curry-Howard Correspondence, but Martin-Lof is more general in a sense that most, if not all first order logic theories can be formulated using MLTT directly via inductive types instead of needing to be added via extra deduction rules.

A model of computation is a formal, mathematical abstraction of computation. It defines a set of allowable operations and their effects, specifying how outputs are derived from inputs.

Different models capture different aspects or levels of computational power. Common examples include finite automata, pushdown automaton, turing machines, and lambda calculi. Many models, like Turing machines and lambda calculus, are equivalent in power (Turing-complete) and define the limits of what is theoretically computable.

Negation types, denoted as $\neg A$ or Not A, represent the negation of a type $A$. They are constructed as function types from $A$ to the empty type $\bot$, i.e., $A \rightarrow \bot$.

Logically via the Curry-Howard Correspondence negation types can be interpreted as logical negation, meaning to prove $\neg A$ you need a proof that given a proof of $A$ you can construct a proof of $\bot$ (i.e. a contradiction). Set-theoretically, if $A$ is a set, $\neg A$ can be thought of as the set of functions from $A$ to the empty set.

The Nelson-Oppen theory combination algorithm is a technique used in SMT solvers to handle formulae involving multiple logical theories (e.g. arithmetic and uninterpreted functions). The core idea is to separate a mixed-theory formula into formulas that are only in one theory, connecting them via new variables.

This is achieved by:

1. Identifying terms that mix symbols from different theories (e.g. $f(x+1)$: $f(...)$ is uninterpreted, $x + 1$ is arithmetic).
2. Introducing "fresh" variables to represent these subterms within a clause belonging to a specific theory.
3. Adding interface equality constraints that link these new variables back to the original terms they replaced.

Example: $f(x+1) = y$ might be reduced into two parts:

• Theory A (Arithmetic): v = x+1
• Theory B (Uninterpreted Functions): f(v) = y
  (where v is a new shared variable)

This separation allows each theory's solver to independently check the separate parts, deriving new clauses/equalities, until we derive a contradiction or we find a valid assignment.

Paper Link: Here

Summary generated by Gemini 2.5 Pro Preview 05-06:

This paper, "On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi" by Gerd Hillebrand and Paris Kanellakis (posthumously), presents a comprehensive functional framework for descriptive computational complexity. It establishes precise syntactic characterizations for various complexity classes—Regular, First-order, PTIME, PSPACE, k-EXPTIME, k-EXPSPACE (for $k \geq 1$), and Elementary sets—using simply typed lambda calculus (TLC) and let-polymorphic lambda calculus (core-ML), augmented with constants and an equality predicate (TLC$^=$, core-ML$^=$).

Core Idea and Framework:
The central idea is that typed lambda terms can represent not only programs but also their inputs and outputs. The complexity of functions computable within this framework is directly tied to the "functionality order" of the lambda terms used. Specifically, increasing the maximum allowed functionality order by one corresponds to an increase in computational power, often by one alternation in an alternating Turing machine model.

Key Contributions:

1. A Unified Functional Framework for Complexity: The paper completes a research program (initiated in [21, 19, 20]) to provide a functional counterpart to the logical framework (e.g., Fagin's theorem for NP, fixpoint logic for PTIME) in descriptive complexity.
2. Syntactic Characterization of Complexity Classes: It provides fixed-order typed lambda calculi that precisely capture several important complexity classes.
3. Highlighting the Role of Functionality Order: The paper demonstrates a clear hierarchy: higher functionality orders allow for the expression of more complex computations.
4. The Importance of Constants and Equality: The inclusion of order 0 atomic constants (from a domain $o$) and an order 1 equality predicate ($Eq: o \rightarrow o \rightarrow \tau \rightarrow \tau \rightarrow \tau$) is crucial for moving beyond simple Boolean/regular functions to database-like queries and higher complexity classes.
5. Semantic Evaluation Technique: This is the primary technical contribution. To prove upper bounds (i.e., that a language fragment only computes functions within a certain class), the paper introduces a "semantic evaluation" mechanism. This is necessary because standard $\beta$-reduction can be too slow (e.g., a PTIME function might take exponential time to reduce syntactically). The semantic evaluator ($Eval_k$) uses a hybrid strategy: call-by-value for redexes up to a certain order $k$ and call-by-name for higher-order redexes, effectively trading recursion depth for storage of intermediate results.
6. Let-Polymorphism (core-ML): The framework is extended to core-ML (TLC with $let$ expressions). Let-polymorphism often allows characterizations that are "program uniform" in TLC to become "language uniform" in core-ML, meaning inputs can be typed more generally.

Methodology and Definitions:

• Lambda Calculi:
  • TLC: Church's simply typed lambda calculus.
  • TLC$^=$: TLC augmented with a type constant $o$ (for domain elements), a countable set of expression constants of type $o$, and an equality constant $Eq$.
  • core-ML / core-ML$^=$: The $let$-polymorphic versions.
• Functionality Order: Defined recursively: order(type variable/constant) = 0; order($\alpha \rightarrow \beta$) = max(1 + order($\alpha$), order($\beta$)).
• Input/Output Conventions:
  • Outputs are always Booleans (type $Bool := \tau \rightarrow \tau \rightarrow \tau$).
  • For pure TLC: Inputs are Booleans or lists of Booleans (encoded as list iterators).
  • For TLC$^=$: Inputs are ordered finite structures. The domain $d$ is a list of constants from $O$. Relations $r_i$ are lists of tuples of constants from $O$. These list iterators typically have a principal type of order 2.
• Typing Conventions:
  • Language Uniform (e.g., $TLI_k^L$): All program terms type their inputs in the same fixed way.
  • Program Uniform (e.g., $TLI_k^P$): Each program has a fixed type, and its inputs must be typed to match that specific program. The same input data might have different types for different programs.
• Lower Bounds (Expressibility): Achieved by simulating Turing machines. This involves:
  • Constructing Church numerals of (hyper)-exponential size.
  • Using higher-order types to create (hyper)-exponentially large domains (e.g., $D_k$).
  • Lifting input relations and predicates to these larger domains.
• Upper Bounds (Containment): Proven using the novel semantic evaluation technique ($Eval_k$), which evaluates terms in a finite model based on the constants present in the query and input. The complexity of $Eval_k$ is analyzed based on the order $k$ and the structure of the term.

Main Results:

1. Pure TLC (without constants/equality):

   • BOOL (Language Uniform): Terms of type $Bool \rightarrow ... \rightarrow Bool$ express exactly the Boolean functions.
   • REG (Program Uniform): Terms of type $\{Bool\}^* \rightarrow Bool$ (list of Booleans to Boolean) express exactly the characteristic functions of regular languages.

2. TLC$^=$ (with constants and equality):

   • First-Order Queries (Language Uniform): TLI$_0^L$ (lambda terms of order 3 over finite structures) capture first-order logic with order. This is analogous to the Schwichtenberg-Statman theorem for extended polynomials.
   • PTIME (Program Uniform): Characterized by TLC$^=$ terms of order 4.
   • PSPACE (Program Uniform): Characterized by TLC$^=$ terms of order 5.
   • k-EXPTIME (Program Uniform): Characterized by TLC$^=$ terms of order 2k+4.
   • k-EXPSPACE (Program Uniform): Characterized by TLC$^=$ terms of order 2k+5.
   • (The paper denotes these fragments as TLI$_k^P$ with different $k$ indexing, but the resulting orders are as above).

3. core-ML$^=$ (with constants, equality, and let-polymorphism):

   • The program uniform characterizations for PTIME, PSPACE, k-EXPTIME, and k-EXPSPACE in TLC$^=$become **language uniform** in core-ML$^=$.
   • MLREG also expresses regular languages language uniformly.

Significance and Implications:

• Provides a deeper understanding of the expressive power inherent in the type systems of functional programming languages.
• Establishes a direct link between a fundamental syntactic feature (functionality order) and computational complexity.
• The characterizations are often more "economical" in terms of basic primitives compared to some logical characterizations.
• The semantic evaluation technique is a significant contribution for analyzing the complexity of typed lambda calculi when syntactic reduction is insufficient.
• The PTIME vs. PSPACE distinction is elegantly captured by a difference in functionality order (e.g., order 1 vs. order 2 types for intermediate data, leading to order 4 vs. order 5 for the overall language fragment).

Limitations (as noted in Discussion):
The framework, being deterministic, does not provide a syntactic characterization for NP. Capturing NP would likely require adding a non-deterministic primitive (like a "coin" operation), which would violate properties like Church-Rosser.

Personal Note:
The paper includes a touching dedication by Gerd Hillebrand to his co-author and mentor, Paris Kanellakis, who tragically passed away shortly after they finished the work.

In summary, this paper offers a robust and elegant framework connecting the typed lambda calculus, a cornerstone of functional programming, with fundamental computational complexity classes. Its key insights revolve around the role of functionality order and the novel semantic evaluation technique for proving tight complexity bounds.

Peirce's Law is a principle in logic named after the philosopher and logician Charles Sanders Peirce. It can be defined as follows:

$\forall P, Q. ((P \rightarrow Q) \rightarrow P) \rightarrow P$

Intuitively: "If it's true that $P$ is true whenever $P$ implying $Q$ is true, then $P$ must be true."

Or alternatively: "If we have a function $f$ that produces $P$ given any proof that $P \rightarrow Q$, then $P$ must be true. Classically, either $P$ holds (and we're done) or $P$ is false, in which case $P \rightarrow Q$ holds vacuously, so $f$ produces $P$ — contradicting $P$ being false." This classical case-split is exactly why the law requires LEM and is not intuitionistically provable.

Peirce's Law is a theorem of classical propositional logic but is not provable in intuitionistic propositional logic. Adding Peirce's Law as an axiom to an intuitionistic system is one way to make the logic classical. It is in some sense equivalent to law of the excluded middle in that both result in a classical logic when added to an intuitionistic logic, but is in definition akin to the type-theoretical equivalent of LEM [[equivalent:call with current continuation]].

A Π-type (Pi-type), also known as a dependent function type or dependent product type, is a type constructor in type theories with dependent types, such as Martin-Lof Type Theory.

Given a type $A$ and a family of types $B(x)$ indexed by terms $x : A$, the Π-type, written as $\Pi x:A. B(x)$ or $(x:A) \rightarrow B(x)$, represents the type of functions that take a term $a : A$ and return a term of type $B(a)$. The return type $B(a)$ depends on the input value $a$.

Under the Curry-Howard Correspondence, Π-types correspond to universal quantifiers ($\forall$) in logic. A proof of $\forall x:A. P(x)$ is a function that, given any $a:A$, produces a proof of $P(a)$.

A predicate is a symbol in predicate logic and its supersets (such as first order logic) that represents a property of objects or a relation among objects. It can be thought of as a function that maps tuples of objects to a truth value (True or False).

• A predicate with one argument (a unary predicate) expresses a property. For example, $\text{Human}(x)$ could mean "$x$ is human."
• A predicate with two arguments (a binary predicate) expresses a relation between two objects. For example, $\text{Loves}(x, y)$ could mean "$x$ loves $y$."
• A predicate with $n$ arguments (an $n$-ary predicate) expresses a relation among $n$ objects.

When the variables in a predicate are instantiated with specific objects from a domain, the predicate becomes a proposition that is either true or false. For example, if $\text{Socrates}$ is an object in the domain, $\text{Human}(\text{Socrates})$ is a proposition.

Predicates are fundamental building blocks for constructing logical formulas in predicate logic. They are combined with quantifiers and logical connectives to make assertions about domains of discourse, this combination of predicates, quantifiers, and some other things results in First Order Logic.

The principle of explosion, also known as ex falso quodlibet (from a falsehood, anything follows), is a fundamental principle in logic. It states that from a contradiction, any statement can be derived.

Formally, it can be expressed as:

$\bot \rightarrow A$

A product type, denoted as $A \times B$ or Pair A B, represents a value that is a pair of values, one of type $A$ and one of type $B$. Values of a pair type are typically constructed using a pairing operation (e.g., (a, b) where a is of type A and b is of type B).

Logically via the Curry-Howard Correspondence product types can be interpreted as $A \land B$ or logical conjunction, meaning to prove $A \land B$ you need a proof of both $A$ and $B$. Set-theoretically it can be interpreted as the cartesian product of sets $A$ and $B$. In category theory product types correspond to categorical products.

A propositional formula is a type of logical formula that uses symbols to express the framework of propositional logic.

For the purposes of this ontology, we will use the same symbols that have been used in class.

• Propositional variables are represented by single-letter names.
• Logical conjunction of two sub-formulae is represented by $A \land B$, where $A$ and $B$ are any valid propositional formulae.
• Logical disjunction of two sub-formulae is represented by $A \lor B$, where $A$ and $B$ are any valid propositional formulae.
• Not $\lnot A$
• Xor $A \oplus B$
• Implies $A \rightarrow B$
• True $\top$
• False $\bot$

A propositional literal is either a propositional variable or its logical negation.

Propositional Logic is simply the intuitionistic propositional logic combined with the law of the excluded middle, or double negation elimination (they are equivalent axioms), enabling proofs by contradiction.

I.e. adding either of these rules of inference encoding the LEM/double negation axiom:

$$\frac{}{\Gamma \vdash A \lor \neg A} \text{LEM}$$

$$\frac{}{\Gamma \vdash \neg \neg A \rightarrow A} \text{double-neg}$$

A propositional variable (or sentence letter) is a kind of variable and a basic element in propositional logic. It represents an atomic proposition—a statement that can be assigned either true or false.

In propositional formulae, they are often represented by single letters like $p, q, r, A, B$. An assignment maps propositional variables to truth values.

A pushdown automaton (PDA) is a type of finite automaton that employs a stack in addition to finite state control. It is a Model of Computation more capable than finite automata but less capable than Turing machines.

A defining property of pushdown automaton are that they are the weakest Model of Computation capable of recognizing context-free languages.

A quantifier is a construction defined by an inference rule that specifies how many individuals in the domain of discourse satisfy a proposition or property. Quantifiers bind variables in a formula, turning an open formula (which has a free variable and thus no definite truth value) into a formula that has a definite truth value (assuming all variables are bound).

The most common quantifiers are:

• Universal Quantifier ($\forall$): "for all" or "given any".
• Existential Quantifier ($\exists$): "there exists" or "for some".

In the wild

Quantifiers are essential components of First Order Logic, and higher order logics as well.

A Rule of Inference is clearly defined rule for drawing a conclusion from a set of premises. Every formal system has a deductive system as a part of its formal grammar that consists of rules of inference that allow us to take an axiom and derive a theorem.

For an example of inference rules, see the typing rules of the simply typed lambda calculus.

Satisfiability is the property of some logical formulae whereby there exists some satisfying assignment given which the formula evaluates to true.

It is related but distinct from validity.

A satisfiability solver is an algorithm that, given a logical formula, determines whether or not it is satisfiable, and if it is, returns a satisfying assignment, sometimes referred to as a model.

A satisfying assignment is a kind of assignment which, taken with a logical formula, causes that formula to be interpreted as true.

A Σ-type (Sigma-type), also known as a dependent pair type or dependent sum type, is a type constructor in type theories with dependent types, such as Martin-Lof Type Theory.

Given a type $A$ and a family of types $B(x)$ indexed by terms $x : A$, the Σ-type, written as $\Sigma x:A. B(x)$ or $(x:A) \times B(x)$, represents the type of pairs $(a, b)$ where $a : A$ and $b : B(a)$. The type of the second component $B(a)$ depends on the value of the first component $a$.

Under the Curry-Howard Correspondence, Σ-types correspond to existential quantifiers ($\exists$) in logic. A proof of $\exists x:A. P(x)$ is a pair consisting of a witness $a:A$ and a proof of $P(a)$.

The Simply typed lambda calculus (STLC) is a type theory that extends and restricts the lambda calculus by assigning [[uses:type
|types]] to lambda terms.

In simply typed lambda calculus, every term has a unique type, and the type system enforces that functions are only applied to arguments of the correct type. This is achieved through type checking rules that verify the consistency of type assignments.

It is equivalent to implicational intuitionistic propositional logic via the Curry-Howard Correspondence where every type and term in STLC corresponds to a proposition and proof in IIPL.

The types in STLC consist of the following primitives:

• Function Type

And the following typing rules, see the type theory page for more info on how these work.

Typing Rules:

$$\frac{\Gamma, x:A \vdash b : B}{\Gamma \vdash \lambda x.b : A \rightarrow B} \text{function}$$

$$\frac{\Gamma \vdash (\lambda x.b) : A \rightarrow B \quad \Gamma \vdash a : A}{\Gamma \vdash (\lambda x.b)\, a \equiv b[x:=a] : B} \text{beta-reduction}$$

An SMT solver is an implementation of algorithms that can solve first order logic formula, usually conjoined with some extra theory $T$.

SMT solvers work by combining the techniques of SAT solvers (like CDCL) with theory-specific solvers. The core SAT solver handles the boolean structure of the formula, while theory solvers handle the constraints imposed by the theory $T$.

The process generally involves:

1. Boolean Abstraction: The input formula is abstracted into a propositional formula by replacing theory atoms (theory-specific formulas that resolve to a boolean e.g., $x + y > z$) with new propositional variables.

2. SAT Solving: A SAT solver is used to find a satisfying assignment for the boolean abstraction, if any exists.

3. Theory Check: The assignment from the SAT solver is given to the theory solver, which checks whether the assignment is consistent with the theory.

4. Conflict Resolution: If the theory solver finds a conflict (i.e., the set of theory atoms is inconsistent), it generates a "theory lemma" (a constraint implied by the theory) that explains the conflict. This lemma is added to the boolean abstraction as a clause, and the process repeats from step 2.

5. Satisfiable/Unsatisfiable: If the SAT solver finds an assignment that is consistent with the theory, the original formula is satisfiable. If the SAT solver exhausts all possibilities (including those refined by theory lemmas) without finding a consistent assignment, the original formula is unsatisfiable.

Welcome to the Automated Reasoning Ontology!

This is an ontology to catalogue and investigate concepts in Automated Reasoning. Specifically to answer the question: To what degree can existing logical frameworks and their satisfiability algorithms be generalized and applied to inferring programs in different type theories?.

Before You Start

For an improved ontology viewing experience it is recommended to tweak the settings on the sidebar to hide uses and mention links.

Types

Ontologies have types for their nodes and links between nodes, and this one is no exception! The node and link types (and their meanings) are as follows:

Node Types

• start - unique type of the node you are reading right now.
• structure - a formally intensionally definable concept, i.e. assume you can define this mathematically.
• category - an informally (extensionally) defined concept, perhaps defined in terms of shared experience or other colloquial terms.
• algorithm - a specific function or program
• source - a note linking to and sometimes summarizing an external document.
• argument - a note arguing for a certain point of view (e.g., Feasibility of Program Inference).
• undefined - notes that don't have a good category yet.

Link Types

• is-a - if a concept (a structure or a category) inherits traits/properties from another concept, the concept inheriting traits should link to the supertype using the is-a link.
• is-broadly - Basically the same as is-a but for more longer-range subtyping relations in order to create a better visualization.
• uses - if a concept uses another concept in its definition, for example, a structure that is constructed from other structures this link can be used.
• part - if a concept is a part of another concept, i.e. some other concept is an integral aspect (piece that is composed), this can be used as a "stronger" connection than uses to make the graph nicer (has a stronger force for the force-graph).
• mention - if any note mentions another note, but not in any kind of particular way, this link type may be used.
• cites - should be used to link to source nodes, to cite that source.

If you're curious about the source code of this repository, check out the following link: https://github.com/zontasticality/ar-ontology

AI Disclosure

Gemini 2.5 Pro 03-25 and Gemini 2.5 Pro 05-06 output was used verbatim for helping readers explore sources for the reader's convenience. Models were also used as a writing aid due to the sheer amount of content required to create a comprehensive ontology. For the ontology AI output was used for idea-generation and drafting purposes only and rewritten.

A sum type, denoted as $A + B$ or Either A B, represents a value that can be either of type $A$ or of type $B$. Values of a sum type are typically tagged or constructed in a way that indicates which variant they belong to (e.g., Left(a) where a is of type A, or Right(b) where b is of type B).

Logically via the Curry-Howard Correspondence sum types can be interpreted as $A \lor B$ or logical disjunction, meaning to prove $A \lor B$ you only need a proof of one or the other (and an indication of which one you used). Set-theoretically it can be interpreted as the disjoint union of sets $A$ and $B$. In category theory sum types correspond to coproducts.

Paper Link: Here

This paper details the history of Intuitionistic Logic and specifically L. E. J. Brouwer's contributions to the field.

This is the main source for the Brouwer-Heyting-Kolmogorov Interpretation node.

Summary

Summary generated by Gemini 2.5 Pro Preview 05-06:

1. Introduction and Brouwer's Foundational Ideas:
The paper begins by situating intuitionistic logic as a system of reasoning developed from Brouwer's philosophical stance on mathematics.

• Brouwer's Philosophy: Mathematics is an exclusively mental activity, independent of and prior to language and logic. Mathematical objects (including proofs) are mental constructions.
• First Act of Intuitionism: This was the separation of mathematics from language, rooted in the "intuition of the bare two-oneness." This initially led to intuitionistic arithmetic and a theory of rationals but struggled with the continuum due to an insistence on predicative definability (finitely specifiable, hence denumerable entities).
• Negation as Absurdity: Brouwer interpreted negation not as mere falsity but as absurdity (leading to a contradiction). He objected to the universal law of excluded middle ($A \lor \neg A$), seeing it as an a priori claim that every problem is solvable, and to the law of double negation ($\neg\neg A \supset A$) as asserting every consistent statement holds.
• Early Developments: Brouwer's 1907 dissertation laid groundwork, criticizing existing philosophies of mathematics. His 1908 paper "The unreliability of the logical principles" questioned the universal validity of classical logical laws for infinite systems.

2. Formalization and Early Interpretations:

• Heyting's Formalization (1930): Heyting, at Brouwer's suggestion, formalized intuitionistic propositional logic (IPC), first-order predicate logic (IQC), and parts of intuitionistic mathematics (arithmetic, species).
  • IPC: Presented with axioms for $\supset, \land, \lor, \neg$ (e.g., $\neg A \supset (A \supset B)$ effectively replacing $A \lor \neg A$). Heyting demonstrated the independence of his axioms.
  • IQC: Extended IPC with quantifiers ($\forall, \exists$) and identity ($\equiv$). The universal quantifier implies a uniform construction; the existential quantifier implies a witness has been found or a method to find one is known.
• Glivenko's Contributions (1928-1929): Independently worked on formalizing IPC. Proved Glivenko's Theorems:
  1. If $A$ is provable classically, $\neg\neg A$ is provable intuitionistically.
  2. If $\neg A$ is provable classically, $\neg A$ is provable intuitionistically.
• Kolmogorov's Problem Interpretation (1925, 1932):
  • His 1925 work on "minimal logic" (implication and negation) was largely unnoticed in the West.
  • His 1932 interpretation viewed logical formulas as "problems": $A \land B$ is the problem of solving A and B; $A \lor B$ is solving A or B; $A \supset B$ is reducing the solution of B to A; $\neg A$ is deriving a contradiction from a solution of A. This forms part of the Brouwer-Heyting-Kolmogorov (BHK) explication of intuitionistic logic.

3. Intuitionistic Arithmetic (HA):

• Heyting's Arithmetic: Developed within his predicate calculus, including axioms for natural numbers, successor, and induction. He defined $+, <, >$.
• Kleene's Arithmetic (HA): Became the standard formalization, with constant 0, unary successor $'$, binary $+, \cdot$, and predicate $=$. Includes logical axioms, induction schema, and specific arithmetical axioms.

4. Proof Theory of Intuitionistic Logic and Arithmetic:

• Relationship to Classical Logic: IFOL (IQC) is a proper subsystem of classical FOL. ISOL is inconsistent with classical SOL. Intuitionistic language is richer.
• Negative Translations (Gödel, Gentzen, Kolmogorov): Showed that classical first-order arithmetic can be faithfully translated into the negative fragment of intuitionistic arithmetic. This established proof-theoretic equivalence for certain classes of statements and clarified the relationship between classical and constructive consequences. For example, a formula $A$ is classically provable iff $A^*$ (its translation, often involving $\neg\neg$ for primes/disjunctions/existentials) is intuitionistically provable.
• Constructive Properties (Disjunction and Existence):
  • Disjunction Property (DP): If $A \lor B$ is a closed provable formula in IPC/IQC, then $A$ is provable or $B$ is provable.
  • Existence Property (EP/EPN): If $\exists x A(x)$ is a closed provable formula in IQC (or HA), then $A(t)$ (or $A(n)$ for a numeral $n$ in HA) is provable for some term $t$. These were stated by Gödel and proved by Gentzen for logic, and by Kleene for arithmetic.
• Gentzen's Sequent Calculus (LJ): Introduced a system for natural deduction where derivations are trees. His Hauptsatz (cut-elimination theorem) implies that proofs can be normalized, from which DP and EP follow more directly.
• Admissible vs. Derivable Rules: A rule is derivable if its conclusion can be deduced from its premises within the system. It's admissible if, whenever its premises are theorems, its conclusion is also a theorem. In IPC, there are admissible rules that are not derivable (e.g., independence of premise rules like $\neg A \supset (B \lor C) \vdash (\neg A \supset B) \lor (\neg A \supset C)$, Mints' rule). Visser's rules provide a basis for all admissible propositional rules. Markov's rule is an important admissible rule for IQC/HA involving decidable predicates.

5. Interpretations (Semantics) of Intuitionistic Logic and Arithmetic:

• Algebraic Semantics: IPC can be interpreted in Heyting algebras (lattices with an additional operation $\supset$).
• Topological Semantics (Mostowski, Rasiowa & Sikorski): IQC can be interpreted using open sets of a topological space. Both algebraic and topological semantics are sound and complete for IPC/IQC.
• Recursive Realizability (Kleene, Nelson): For HA. A number $e$ "realizes" an arithmetical sentence $E$ if $e$ codes a construction satisfying $E$ according to BHK.
  • Nelson's Theorem: Every theorem of HA is realizable.
  • This interpretation proves the consistency of HA with Church's Thesis ($CT_0$) (every effectively calculable function is recursive) and Markov's Principle ($MP$) (related to decidability of predicates over natural numbers).
• Kripke Semantics (Beth, Kripke): "Possible worlds" semantics.
  • A Kripke model consists of a set of nodes (worlds) $K$ with a partial order $\leq$ (accessibility) and a forcing relation $\Vdash$. Forcing is persistent (if $k \Vdash A$ and $k \leq k'$, then $k' \Vdash A$).
  • $k \Vdash A \supset B$ iff for all $k' \geq k$, if $k' \Vdash A$ then $k' \Vdash B$.
  • $k \Vdash \neg A$ iff for all $k' \geq k$, $k' \not\Vdash A$.
  • For IQC, domains $D(k)$ are associated with nodes, expanding along $\leq$.
  • Sound and complete for IPC and IQC. Veldman provided an intuitionistically acceptable completeness proof for IQC using "exploding nodes."
• Beth Models: Similar to Kripke models but with a different condition for forcing disjunctions and existential quantifiers based on "barring" by subtrees.

6. The Second Act of Intuitionism: The Continuum and Choice Sequences:
Brouwer's later work tackled the intuitionistic continuum.

• Choice Sequences (infinitely proceeding sequences, ips): Accepted as legitimate mathematical entities, even if not fully defined in advance. Generated by "spreads" (laws defining allowed choices).
  • Fan/Finitary Spread: Only finitely many choices available at each step.
• Brouwer's Fan Theorem: A total integer-valued function on a fan is uniformly continuous (its value is determined by a finite initial segment of the choice sequence input, with a uniform bound on the length of this segment).
• Continuity Principle: Any total function defined on a spread (e.g., from choice sequences to numbers) is continuous. This principle contradicts classical logic (e.g., it implies $\neg \forall \alpha (\forall x \alpha(x)=0 \lor \neg \forall x \alpha(x)=0)$).
• Bar Theorem (Bar Induction): A principle of induction over well-founded trees of finite sequences, essential for proving the Fan Theorem. Initially "proved" by Brouwer, later largely accepted as an axiom.
• Kleene and Vesley's FIM (Foundations of Intuitionistic Mathematics, 1965): A formal system for intuitionistic analysis, two-sorted (numbers and choice sequences). Includes HA, countable choice, Brouwer's Principle for Functions (a strong form of continuous choice), and Bar Induction.
  • FIM is inconsistent with classical logic but consistent relative to its subsystem B (without Brouwer's Principle).
• Heyting's Arithmetic of Species ($HAS_0$) and $HA^\omega$ (Arithmetic of Finite Types): Extensions of HA dealing with collections (species) and higher-type objects, respectively. Troelstra studied these, proving properties like the Uniformity Principle ($UP$) which also has non-classical consequences.