Minimal logic is a fragment of intuitionistic logic that rejects not only the classical law of excluded middle (as intuitionistic logic does), but also the principle of explosion (ex falso quodlibet). Essentially, from proof-theoretical viewpoint, this means that in minimal logic the bottom $\bot$ is considered as a propositional variable, without any special inference rule involving it.

Question: Is there a semantics $\mathcal{S}$ for minimal logic such that a completeness theorem holds? By completeness theorem I mean a statement of the form (for both propositional and first-order languages):

For every formula $A$, $A$ is provable in minimal logic if and only if $A$ is valid in all $\mathcal{S}$-structures.

I guess such a semantics could be a generalization of intuitionistic Kripke models.

I would like also to have some references about completeness theorem in (propositional and/or first-order) minimal logic.

  • 4
    $\begingroup$ I find it boggling that one would throw in a gratuitous propositional constant without any axioms relating to it. I find it especially boggling that one would name the constant $\bot$ when it is not a bottom element. $\endgroup$
    – user14972
    Jan 28, 2018 at 22:52
  • $\begingroup$ Can I ask the reason of the recent downvote? $\endgroup$ Apr 5, 2018 at 19:04

2 Answers 2


Yes, tweaking Kripke semantics based on that for intuitionistic logic does the trick. If I recall right, there are slightly different ways of doing this.

Here's a version for minimal logic and some variants, in a recent paper by Almudena Colacito, Dick de Jongh and Ana Lucia Vargas.

  • $\begingroup$ Great reference, exactly what I was looking for. Thank you! $\endgroup$ Jan 29, 2018 at 0:41
  • $\begingroup$ Do you know which is the first paper where a completeness theorem for (propositional and/or first-order) minimal logic has been proved? Maybe it is already in the paper by Johansson introducing minimal logic (1937), but it is in German and I don't speak German. $\endgroup$ Jan 29, 2018 at 8:24
  • $\begingroup$ @Taroccoesbrocco Sorry, no I don't. $\endgroup$ Jan 29, 2018 at 8:55
  • 2
    $\begingroup$ @Taroccoesbrocco - you can see also Almudena Colacito's Thesis: Minimal and Subminimal Logic of Negation with some historical references: maybe useful the ref to H.Rasiowa's algebraic semantics (1974). $\endgroup$ Jan 29, 2018 at 9:17
  • $\begingroup$ @MauroALLEGRANZA - Very useful, thank you! $\endgroup$ Jan 29, 2018 at 9:49

Update 2023-12-06: The proof was incomplete. I didn't cover the case where the $\bot$ pseudovariable was assigned the interpretation $\varnothing$.

You can tweak the topological semantics for S4 and IPC to get a semantics for minimal logic.

I'll assume the following two results.

  1. The standard topology on $\mathbb{R}$ (call it $\tau^R$) with $\mathbb{R}$ as the sole distinguished truth value is a sound and complete semantics for IPC.
  2. Minimal logic is exactly equivalent to IPC with $\bot$ interpreted as an extra propositional variable.

Given those two results, we can define the following semantics for minimal logic.

Let each unary and binary connective be defined on $\tau^R$ as for IPC. $\land$ and $\lor$ are $\cap$ and $\cup$ respectively. $\to$ is $i(\cdot^c \cup \cdot)$ where $i$ is the interior and ${}^c$ is the complement. Let $\lnot \cdot $ abbreviate $\cdot \to \bot$ as usual.

Let $\bot$ be interpreted as $(-1, 1)$ (for concreteness, any fixed nonempty open set will do).

Here's a proof of the soundness and completeness of this semantics.

Let $v$ be a mapping from variable symbols including the $\bot$ pseudo-variable to $\tau^R$.

Suppose the interpretation of $\bot$ is not $\varnothing$. Let $k$ be an affine function sending the interpretation of $\bot$ to $(-1, 1)$. Let $v''$ be $v$ with $k$ applied to the interpretation of each function.

Suppose the interpretation of $\bot$ is $\varnothing$. Then define a function $F$ in the following way: $F(0) = \{-1, 1\}$, $F(\alpha)$ is $1 + \alpha$ when $\alpha > 0$, $F(\alpha)$ is $-1 + \alpha$ when $\alpha < 0$.

Let $F(X)$ be defined as $(-1, 1) \cup \bigcup_{x \in X} F(x)$.

Intuitively, $F$ duplicates the point $0$ and then parts the waters between the positive and negative reals. We then throw back in $(-1, 1)$.

I claim that $v \models \varphi$ if and only if $v'' \models \varphi$. As proof, observe that the affine functions $k$ and our line-splitter function $F$ commute with each operation $\cap, \cup, {}^c, i$. And that $kX$ is $\mathbb{R}$ if and only if $X$ is $\mathbb{R}$ and likewise for $F$.

Therefore this topological semantics is a sound and complete semantics for IPC with $\bot$ interpreted as an extra variable.

Therefore this topological semantics is a sound and complete semantics for minimal logic.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .