If I take the inference rules for the implication-free fragment of classical logic (listed below) and drop the pair of rules for disjunction elimination, do I get a complete Hilbert calculus for LP (Logic of Paradox)?
One thing that I am uncertain about, though, is whether pruning away disjunction elimination without adding back a weaker rule in its place actually gives me LP instead of some other system.
I also have a higher-level motivation for this question. I like trying to come up with semantics for various propositional logics, but I'm not good at proving or disproving the completeness of a given semantics. I'm trying to pick a simple example of a nonclassical logic so I can get a feel for how to build a completeness argument.
Additionally, the original question contains one huge oversight, as Troposphere points out in the comments. LP has exactly the same set of tautologies as classical logic. However, it has a different consequence relation. The property that I'm most curious is "completeness" with respect to the consequence relation. (I'm not sure whether this property is actually called completeness though.)
What follows is an explanation of the question in detail and my attempt to solve the problem myself.
I will assume classical logic and ordinary mathematics in the background for the purposes of this question.
Let's define the logic of paradox using the following truth table.
and not
F U T
------- -----
F F F F F T
U F U U U U
T F U T T F
And let disjunction be defined as follows $a \lor b$ = $\lnot(\lnot a \land \lnot b)$.
Logic of paradox has the following sound and complete semantics. This semantics is transparently based on the semantics of Belnap's four-valued logic.
$F$ is $\{0\}$.
$T$ is $\{1\}$.
$U$ is $\{0, 1\}$.
The designated truth values are $T$ and $U$.
We can defined the semantics of the primitive operations as follows. Let $\oplus$ be xor or equivalently addition modulo 2. Let $\triangle$ be the symmetric difference. These operations are really defined in $2^{\{0, 1\}}$, but they both preserve set non-emptiness.
$[\lnot x] = \{ 1 \oplus n : n \in [x] \}$
$[x \land y] = ([x] \triangle \{1\} \cap [y] \triangle \{1\}) \triangle \{1\} $
Logic of paradox, given the signature $\land, \lor, \lnot$ has the following inference rules (which are also valid in classical logic).
$$ \frac{A}{A \lor B} \;\; \text{is disjunction introduction} $$ $$ \frac{A \land B}{A} \;\; \text{and} \;\; \frac{A \land B}{B} \;\; \text{are conjunction elimination} $$ $$ \frac{A \; \text{and} \; B}{A \land B} \;\; \text{is conjunction introduction} $$ $$ \frac{A}{\lnot\lnot A} \;\; \text{is double negation introduction} $$ $$ \frac{\lnot\lnot A}{A} \;\; \text{is double negation elimination} $$
For my axioms, I will take the following axiom schema (which I nonstandardly call the axiom schema of tautological horn clauses).
$$ \lnot x_1 \lor \lnot x_2 \lor \cdots \lor \lnot x_n \lor \cdots \lor A \;\; \text{where $A$ is in $\{x_1, x_2, \cdots, x_n \}$} $$
I will also take all sentences of the form $\lnot \Gamma_1 \lor \lnot \Gamma_2 \lor \cdots \lor \varphi$ where $\Gamma \vdash \varphi$ is a substitution instance of a primitive inference rule.
The classically-valid pair of rules $\frac{A \lor B \; \text{and}\; \lnot A}{B}$ and $\frac{A \lor B \;\text{and}\; \lnot B}{A}$ is not valid in LP..
I'm pretty sure that the collection of rules above with the disjunction-elimination pair of rules forms a Hilbert calculus for classical logic. The rules are certainly sound with respect to classical logic. I'm pretty sure that these inference rules also guarantee that all the connectives are truth-functional, which gives us classical logic because our background logic is classical logic.
I'm less confident that the rules above without disjunction elimination are complete with respect to the intended semantics of LP.
One property that LP has is that all the connectives are $U$-preserving, so if both arguments are $U$, the result will be $U$ as well. Intuitively, this is the thing that knocks out disjunction elimination. Knowing that the negation of a proposition is true in LP is simply not as informative as it would be in classical logic.
One thing that I am uncertain about, though, is whether pruning away disjunction elimination without adding back a weaker rule in its place actually gives me LP instead of some other system.