What are non-classical metatheories like? How do you use a metatheory that isn't classical?
It is straightforward to use a classical system to analyze simple non-classical ones. However, this is the only way I know to work with non-classical systems, by mapping them back to a system that's more expressive, but classical above a certain level of metaness.
Apologies for the long-winded example, it's meant to illustrate what I mean by the metatheory being "essentially classical" even in cases when the object of study is nonclassical.
A word on notation: I will use Łukasiewicz notation for connectives in the object language and English words
implies for meta-level stuff.
When talking about first order logic I will use ordinary symbols (⇒, ∧, ¬) for the object language and English words
if ... then for meta-level stuff.
I'm interested in nonclassical logic, particularly propositional logics because you only have one type of non-logical symbol. Also, what they're trying to achieve is interesting: how do atomic, non-analyzable things-capable-of-bearing-truth-values interact?
I know of a handful of ways of talking about nonclassical logics, but they're all embedded in a classical substrate.
The most powerful for propositional logics, in my opinion, is just translating formulas inductively into a classical first order logic with a single sort.
K be conjunction,
A be disjunction,
C be implication,
N be negation, and
F be bottom.
We can turn well-formed formulas in our propositional calculus into closed terms in classical first order logic with a single one-place predicate
t for designating the chosen truth values. Note that the quantifiers are all universal and all constrained to appear on the left edge of the wff. When we induct, we construct our matrix and a quantifier train to close our formula separately. I'm doing this so I don't need to talk about the truth values of open formulas in FOL.
x (where a is a variable) ---> ∀a. t(x) Kxy ---> ∀xy. t(k(x, y)) Axy ---> ∀xy. t(a(x, y)) Cxy ---> ∀xy. t(c(x, y)) Nx ---> ∀x. t(n(x))) F ---> t(f)
KaNb maps to
KaNb does not map to
I can come up with logics with more interesting relationships between truth-values than
some are chosen and some are not, such as defining an order on them
<=. E.g. F <= U <= T would be true in most three-valued logics. I can even state interesting facts like
A are covariant in both their arguments,
C is contravariant in its first argument and covariant in its second argument. In this translation procedure, the kinds of things I want to say about truth values on the left hand side affect my choice of predicates on the right hand side.
I can represent things like inference rules by using classical connectives in my FOL on the right hand side.
a b ---- ---> ∀ab.(t(a) ∧ t(b)) ⇒ t(k(a,b)) Kab
I can also talk about semantics on the left hand side by talking about models on the right hand side.
How do you work with a foundation that's nonclassical though? If my meta-level reasoning includes things like uncertainty, vagueness, modality, or rejects classically valid inferences like double negation elimination, how do you actually use it in practice rather than just studying it as a mathematical object?