Resources, references, or examples for logics with finitely many sentences

Question

Are there any interesting logics with only finitely many sentences total? Is there a reason why potential logics with this property would be trivial or badly behaved?

I'm looking for a reference to read more or an example of such a logic that's interesting as a mathematical object.

---

I was recently looking at some examples of interesting logics that are fragments of better-known logics, such as two-variable logic and a list of intermediate logics that are interesting logics between intuitionistic propositional logic and classical propositional logic.

One thing that I haven't come across yet, though, is a modern logic (possibly described as a fragment of another logic) with structural constraints on well-formed formulas that are so strong that only finitely many sentences are possible or only finitely many sentences up to renaming of variables are possible. Traditional term logic, even with the addition of non for modifying predicates, has finitely many sentences up to renaming of variables.

I can think of a few weird properties of such finite-number-of-sentences logics off the top of my head like the fact that ordinary introduction rules like $A, B \vdash A \land B$ will sometimes fail if the conclusion is too big to be well-formed.

NOTE: removed reference to $\alpha$-equivalence, replaced with up to renaming of variables which is more clear.

Answer 1

If the total number of formulas is finite, then you can simply write down an exhaustive list of all theorems of the logic. All you need to know about the logic is then contained in this list.

That is, even if you come up with some seemingly complex semantics or proof theory for such a logic, in the end you cannot express more than the problem of whether a formula is contained in a given finite list. And this problem is trivial.

EDIT: I extend this answer to reply Gregory's question below. So why is checking containment in a finite list fundamentally different from checking containment in a countably infinite list? Let us look at an example:

$L$: all prime numbers below $10$.

One way to check whether $n\in L$ is to first verify $n<10$ and then look at the divisors of $n$. But you can also check that $n\in L\iff n\in\{2,3,5,7\}$. The point is now that you can check $n\in L$ without knowing what a prime number is, simply by comparing $n$ to the $4$ possible values in $\{2,3,5,7\}$. In this sense, the problem whether $n\in L$ is not related to factorization at all.

Nothing similar holds for infinite lists, say for the list $P$ of all primes. Of course you can try to say $n\in P\iff n\in\{2,3,5,7,9,11,\ldots\}$, but then in order to explain what the "$\ldots$" means, you'll have to explain what a prime number is.

The same observation as above applies to any finite problem (by this I mean a problem with only finitely many solution instances). Even if you have an initial description of the problem which sounds meaningful (such as being prime and $<10$), there is always a meaningless but equivalent description (such as being either $2,3,5$ or $7$).

For this reason it is also hard to imagine a reasonable logic with only finitely many sentences in total.

(small disclaimer: Artificially, you can create logics where the set of theorems is unknown even if it is finite. For example, your logic could contain as formula only a single atom $p$, and you declare $p$ to be a theorem if the Collatz conjecture is true)

Answer 2

All automated (computer based) theorem provers involve some logic with a finite number of sentences.

I would consider some of those automated theorem provers of interest, since they have gotten used to solve open problems in mathematics and logic, such as when the Robbins problem got solved. Some others might not have solved any open problem, but have the ability to solve open problems with human assistance (or one might think of the computer as the human's assistant). Also, model finders with only a finite number of possible sentences, I would think of interest, since they save people time, as computers work faster than humans in some situations.

Answer 3

I've come up with a semantics for a simple logic that captures some of the intuition behind having finitely many statements. It does this by keeping track of the length of formulas and declaring all formulas above a certain length to always have a designated truth value and hence always be tautologies. This logic still has infinitely many possible sentences in theory, but in practice all the overly long sentences can be identified.

Here's a semantics for a simple logic inspired by the paraconsistent logic LP.

This logic has the connectives $\land, \to, \nrightarrow, \barwedge, \lnot $

The logic FDE (first-degree entailment) has independent truth and falsity conditions.

Let's generalize that somewhat and have a truth conditions as well as a notion of size, which is a positive integer.

The size of $A \land B$ is $1 + \text{the size of $A$} + \text{the size of $B$}$.
$A \land B$ is true if and only if $A$ is true and $B$ is true.

The size of $\lnot A$ is the $1 + \text{the size of $A$}$.
$\lnot A$ is true if and only if $A$ is not true.

The semantics for the rest of the connectives can be defined in terms of the semantics for $\land$ and $\lnot$. The truth conditions are identical to the truth tables of the connectives is classical logic and the size of $A \circ B$ (where $\circ$ is a binary connective) is the size of $A \land B$.

For example,
the size of $A \nrightarrow B$ is the size of $A \land B$.
$A \nrightarrow B$ is true if and only if $A \land \lnot B$ is true.

Let $k$ be the limit on the length of a sentence.

$A$ has a designated truth value if and only if $A$ is true or the size of $A$ is greater than $k$.

Here are some inference rules for such a logic.

The introduction rules are the ordinary introduction rules for classical logic.

For example $\frac{A \;\text{and}\; B}{A \land B}$ is valid because the rule is classically valid and the length of the conclusion is strictly greater than the length of any of the inputs.

The ordinary conjunction elimination rule will not work though, but the following alternative will if we introduce a shriek $\vdash !$, which asserts the non-designatedness of a proposition.

$$ \frac{A \land B \;\; \text{and} \;\; A \nrightarrow A \vdash ! \;\; \text{and}\;\; B \nrightarrow B \vdash ! }{A} $$