1
$\begingroup$

Given a formula in intuitionistic sentential logic, there is a nice, compact textual representation for a witness of its tautology, namely a program in a typed lambda calculus with introduction and elimination forms for $\land$ ($*$) and $\lor$ ($+$) .

If I want to show $ (A + B) \to (B + C) \to B + (A * C) $, I can use the following proof, written in OCaml-like syntax for legibility.

fun x y -> match (x, y) with
| (Right b, _) -> Left b
| (_, Left b)  -> Left b
| (Left a, Right c) -> Right (a, c)

Similarly, if I want to show that $(A \lor B) \to (B \lor C) \to B \lor (A \land C)$ is satisfiable as a first order formula, it suffices to consider the case $\{A=\top, B = \top, C=\top\}$ .

If I want an explicit witness for the tautology of a first order statement, I can do something similar to the OCaml-like syntax (meant to be syntactic sugar over a lambda calculus expression), if I add a magical term inhabiting $x + \lnot x$ or $\lnot \lnot x \to x$, for instance.

What should I do if I want a compact textual representation demonstrating/witnessing the satisfiability of a formula in intuitionistic sentential logic?

There's an example of a Heyting algebra from Wikipedia that assigns the intuitionistic connectives functions from $\mathscr{P}(\mathbb{R})^n \to \mathscr{P}(\mathbb{R})$, with $n$ being the arity of the connective.

$$[\bot] = \emptyset$$ $$[\top] = \mathbb{R}$$ $$[A * B] = [A] \cap [B]$$ $$[A + B] = [A] \cup [B]$$ $$[A \to B] = \text{int}((\mathbb{R} \setminus [A]) \cup [B]) $$

Which suggests to me that one way of providing the a witness of the satisfiability of an expression in intuitionistic sentential logic would be to pick an open subset of $\mathbb{R}$ for every variable and then how that the $[\cdot]$ of the expression is a non-empty set.

Is there a better way of showing the satisfiability of an expression?

Is the notion of satisfiability for an expression in intuitionistic sentential logic (which I'm thinking of as little more than an analogy) even meaningful?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.