Skip to main content
3 of 4
deleted 262 characters in body

Hypothesis: interaction-based model for maximum consistent theories

We are looking for a proof or counter-examples to the following

Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ x_1 = x_1, \dots, x_n = x_n \rangle$, where the $\Gamma$ mapping is defined in a compact encoding for $\lambda$-terms, $M, N \in \Lambda_0$ are combinators, and $n \geq 1$, if and only if $\lambda K\beta\eta \vdash M = N$.

In the case if the hypothesis holds true, we have an effective model for the $\lambda K\beta\eta$ equational theory.