I'm interested in the following logic (3FOL), which is similar to first-order logic (FOL) but is three-valued rather than classical. It is a variant of free logic with neutral semantics.
What are some good properties to investigate when looking at a logic that's similar to classical FOL?
The first thing I tried to do was prove compactness by translating 3FOL into FOL with multiple sorts, shown at the bottom.
My metatheory is ordinary classical logic.
I have three truth values $F, U, T$. $U$ and $T$ are true. $F$ and $U$ are false.
I define the connectives $\lor, \lnot, \square$ as follows. I'm considering $\square$ to be a somewhat artificial connective that exists only to define $\models$ using classical logic rather than LP at the meta-level.
$\lnot \varphi$ is true if and only if $\varphi$ is false.
$\lnot \varphi$ is false if and only if $\varphi$ is true.
$\varphi \lor \psi$ is true if and only if $\varphi$ is true or $\psi$ is true.
$\varphi \lor \psi$ is false if and only if $\varphi$ is true.
$\square \varphi$ is true if and only if $\varphi$ is exclusively true.
$\square \varphi$ is false if and only if $\square \varphi$ is not true.
$ \varphi \land \psi$ is an abbreviation for $\lnot(\lnot \varphi \lor \lnot \psi)$.
Let $D$ be the domain. In a model $M$, if $P$ is an $n$-ary predicate symbol let its interpretation be a subset of $P^n$. Let the interpretation of $f$, an $n$-ary function symbol, be a partial function from $D^n$ to $D$.
Let $V$ be the set of variable symbols.
Let a variable context $v$ be a mapping from a subset of $V$ to interpretations of variables.
Let $t$ be a term. $t$ is defined in $v$ if and only if no function in $t$ is applied outside of its domain.
Now onto the semantics.
$$ M, v \models \square P(t_1, \cdots) \;\;\text{iff all terms in $t_1, \cdots$ are all defined in $v$ and $(t_1, \cdots) \in P^M$} $$
$$ M, v \models \square \lnot P(t_1, \cdots) \;\;\text{iff all terms in $t_1, \cdots$ are all defined in $v$ and $(t_1, \cdots) \not\in P^M$ } $$
$$ M, v \models P(t) \;\;\text{iff}\;\; M, v \not\models \square \lnot P(t) $$
$$ M, v \models \lnot P(t) \;\;\text{iff}\;\; M, v \not\models \square P(t) $$
$$ M, v \models \varphi \lor \psi \;\;\text{iff}\;\; M, v \models \varphi \;\text{or}\; M, v \models \psi $$
$$ M, v \models \lnot(\varphi \lor \psi) \;\;\text{iff}\;\; M, v \models \lnot \varphi \;\text{and}\; M, v \models \lnot \psi $$
$$ M, v \models \square \varphi \;\;\text{iff}\;\; M, v \not\models \lnot \varphi $$
$$ M, v \models \lnot \square \varphi \;\;\text{iff} \;\; M, v \models \lnot \varphi $$
Let $v'$ be $v$ extended with an arbitrary value for $x'$.
$$ M, v \models \forall x \mathop. \varphi(x) \;\;\text{iff}\;\; M, v' \models \varphi(x') \; \text{for all values of $v'$} $$
$$ M, v \models \lnot \forall x \mathop. \varphi(x) \;\; \text{iff} \;\; M, v' \models \lnot \varphi(x') \; \text{for some value of $v'$} $$
And finally,
$$ M \models \varphi \;\; \text{if and only if} \;\; M, v \models \varphi \; \text{for all full variable assignments $v$ } $$
For the proof of compactness, I define the following translation into ordinary $FOL$ for the $\square$-free fragment of 3FOL.
Let the sort $3$ denote the three truth values.
Let the sort $D$ denote the domain extended with an additional element $c$.
For each $n$-ary predicate symbol $P$, let $P^*$ be a function from $D^n$ to $3$. The image of each predicate is constrained to be $\{T, F\}$. This constraint can be imposed with one sentence per predicate symbol.
For each $n$-ary function symbol $f$, let $f^*$ be a function from $D^n$ to $D$. Each $f$ is constrained to send $c$ to $c$. This constraint can be imposed with one sentence per function symbol.
First, convert the sentence to prenex normal form. This technically isn't allowed since the domain is allowed to be empty in 3FOL.
Let each positive atomic formula $P(t)$ be sent to the term $P(t)$.
Let $(\lnot x)^*$ be $n(x^*)$ where $n$ is the $\lnot$-function.
Let $(x \lor y)^*$ be $a(x^*, y^*)$ where $a$ is the $\lor$-function.
Let $(Q_1 Q_2 Q_3 \cdots \varphi)^*$ where $Q_i$ is a quantifier binding a variable be $Q_1 Q_2 Q_3 \cdots (T = \varphi^*) \lor (U = \varphi^*)$.
This translation preserves the existence of models in both directions, therefore (3FOL) has the compactness property.
Addendum
One interesting thing that you can do with models of this logic is take sections, where you restrict the domain. Some functions that were previously total may become partial.
For example, suppose $M \models T$ and $S \subset M$. It's possible to define $M|_S$ as follows. The domain of $M|_S$ is $S$, if $P$ is the interpretation of an $n$-ary predicate, then its interpretation in $M|_S$ is $P \cap S^n$. If $f$ is an $n$-ary function, then its interpretation is $P \cap S^{(n+1)}$.
A function that was previously total may become partial, but the end result will still be a 3FOL structure.
Best Answer
Sorry to be brief, but here are some things one would want to check for right away: Soundness, Completeness, and as you mentioned, Compactness.
Have a look at other logics that are close to First-Order Logic. The first thing that comes to mind is Intuitionistic Logic, but there are others, for instance modal logics.