- Is it possible to turn the syntactic consequence relation $\vdash$ into a preorder?
- Does this perspective/construction have a name?
- Assuming it is possible, can we get this preorder by considering all possible preorders and intersecting just the ones that respect the inference rules?
- Is the induced preorder, assuming it's valid, useful for checking whether a given semantics "works"?
- I'm really really not sure what the proper way is to handle unconditional tautologies.
I was thinking earlier today whether it's possible to generate a preorder on well-formed formulas from inference rules today, and I concluded that it was. Here's my attempt to construct a preorder out of an arbitrary system specified by inference rules.
I will define $a^+$ as the set of all elements strictly above $a$ relative to some preorder $R$. I'm defining $a^+$ somewhat weirdly (without including $a$ itself) because I think it's related to the notion of a filter, but I'm really not sure at all and don't understand what filters are or why they exist.
$$ z \in a^+ \;\;\text{if and only if}\;\; R(a, z) \land a \ne z $$
First, let's impose the technical constraint that if a given system of inference rules has an inference rule with no premises, then it also has a designated truth constant $\top$ or a designated truth formula such as $1=1$. I don't think this is really necessary, I just want to always have a nonempty island of truth if that makes sense.
Suppose $\frac{\Gamma_1, \cdots, \Gamma_n}{\varphi}$ is an inference rule. If $\Gamma$ is empty, we replace it with a singleton set containing our truth constant.
If I have a given preorder $R$, I define consistency of $R$ with an inference rule as follows.
Let $S^+$, where $S$ is a set of well-formed formulas, be defined as follows using the definition of $a^+$ on well-formed formulas from earlier
$$ S^+ = \bigcup_{x \in S} x^+ $$
We can now talk about an inference rule being consistent with a possible relation $R$.
$$ \frac{\Gamma_1 \cdots \Gamma_n}{\varphi} \;\; \text{is consistent with $R$} \\ \textit{if and only if} \\ \Gamma ^ + = (\Gamma \cup \{\varphi\}) ^+ $$
The intuition is that an inference rule is valid if it only leads to conclusions that could have been reached already.
Additionally, I further impose the constraint that $R$ is closed under uniform substitution of variables and syntactic metavariables ... maybe that can be phrased as an inference rule, I'm not sure.
Anyway, I then consider the set of all possible preorders on $L$, let's call it $P$.
Let $P'$ denote the elements of $P$ that are consistent with every inference rule and closed under uniform substitution of variables and syntactic metavariables.
Then I take the intersection of all elements of $P'$, call it $\le'$.
$$ \le' \;\; \text{is equal to} \;\; \cap P' $$
So, I now have a preorder $\le'$ on the set of well-formed formulas in my logic.
I think this preorder is just $\vdash$ viewed through a different lens, so I'm wondering if we can rephrase questions about possible semantics in the following way.
Can I say that a given denotation function $\Delta$ respects the semantics of logic if and only if $\Delta(\varphi) \subset \Delta(\psi) \iff \varphi \le' \psi$?
My denotation function is a thing assigns interpretations to open well-formed formulas. It's probably inductively defined and may also assign interpretations to other things like function symbols and closed terms.
Here's an example for classical propositional calculus.
$$ V \in \Delta(\varphi) \\ \textit{if and only if} \\ \text{ $V$ is a set of variables and $V \subset \text{FV}(\varphi)$ and $\varphi$ holds if the true variables are exactly $V$ } $$