Can a non-classical logic be used as a meta-logic to develop classical logic?

Question

I have read much about non-classical logics such that paraconsistent logics , relevance logics , substructural logics , non-monotonic logic and so on.

I think that the meta-logic logicians use to develop those formal systems is classical logic , by classical I mean that contradiction is not allowed , the law of excluded middle holds and so on.

Now , Can this be reversed ? Can we use non-classical logic to develop classical logic and the other non-classical logic ?

Answer 1

Will attempt an answer, by Goedel's Dialectica Interpretation classical logic (in fact classical mathematics) can be embedded into intuitionistic logic (or Heyting Logic).

Another route is to construct a meta-system that refers to another system (sth like category-theory can talk about algebra, which however itself is a type of algebra)

Answer 2

Classical two valued logic can be viewed as a special limited case of three valued logic. Every classical two-valued theorem is a special case of a three valued theorem (provided the excluded middle applies to all the atomic propositions in a formula), and there are many theorems that are identical in form, but there are a number of classical two-valued theorems that need to be modified or restricted to apply in the more general case, and there are a few that apply only in the more general cases. The extensions of the "and" and the "or" operations are fairly obvious and straightforward. There are three possible extensions of negation: a standard negation, a strong negation, and a weak negation. The major difficulty is finding an appropriate extension of the conditional to three values. The material conditional does not work, the conditional given by Lukasiewicz doesn't work, and the strict conditional suggested by Lewis and used in modal logic doesn't work. There is one that does, although it has been little examined or studied. A related notion is that of logical equivalence: the biconditional equivalences suggested in most treatments of three valued logic do not have the properties of a mathematical equivalence that the classical biconditional does.

By using a strong negation and the appropriate conditional, it is possible to express theorems of three valued logic that correspond to the Heyting axioms of intuitionistic logic. It is also possible to express theorems of three valued logic that correspond to the Lewis systems axioms of modal logic. It should be noted that the three valued tautologies are not identical to the axioms of intuitionism or modal logic. The differences in the interpretation and semantics make them distinct.

As an example, truth tables for one formula using various conditionals can be compared.

Using the material conditional $(p \supset q)$ defined as $(\sim p \lor q)$, consider the formula:

$(p \supset ( q \supset r)) \supset (( p \supset q) \supset ( p \supset r))$

(t T (t T t)) T ((t T t) T (t T t))
(t U (t U u)) U ((t T t) U (t U u))
(t F (t F f)) T ((t T t) F (t F f))

(t T (u T t)) T ((t U u) T (t T t))
(t U (u U u)) U ((t U u) U (t U u))
(t U (u U f)) U ((t U u) U (t F f))

(t T (f T t)) T ((t F f) T (t T t))
(t T (f T u)) T ((t F f) T (t U u))
(t T (f T f)) T ((t F f) T (t F f))

(u T (t T t)) T ((u T t) T (u T t))
(u U (t U u)) U ((u T t) U (u U u))
(u U (t F f)) U ((u T t) U (u U f))

(u T (u T t)) T ((u U u) T (u T t))
(u U (u U u)) U ((u U u) U (u U u))
(u U (u U f)) U ((u U u) U (u U f))

(u T (f T t)) T ((u U f) T (u T t))
(u T (f T u)) U ((u U f) U (u U u))
(u T (f T f)) U ((u U f) U (u U f))

(f T (t T t)) T ((f T t) T (f T t))
(f T (t U u)) T ((f T t) T (f T u))
(f T (t F f)) T ((f T t) T (f T f))

(f T (u T t)) T ((f T u) T (f T t))
(f T (u U u)) T ((f T u) T (f T u))
(f T (u U f)) T ((f T u) T (f T f))

(f T (f T t)) T ((f t f) T (f t t))
(f T (f T u)) T ((f t f) T (f t u))
(f T (f T f)) T ((f t f) T (f t f))

Using the strict Lewis conditional $(p \prec q)$ defined as $\sim \Diamond (p \land \sim q)$ or $ \Box (p \supset q) $

$(p \prec ( q \prec r)) \prec (( p \prec q) \prec ( p \prec r))$

(t T (t T t)) T ((t T t) T (t T t))
(t F (t F u)) T ((t T t) F (t F u))
(t F (t F f)) T ((t T t) F (t F f))

(t T (u T t)) T ((t F u) T (t T t))
(t F (u F u)) T ((t F u) T (t F u))
(t F (u F f)) T ((t F u) T (t F f))

(t T (f T t)) T ((t F f) T (t T t))
(t T (f T u)) T ((t F f) T (t F u))
(t T (f T f)) T ((t F f) T (t F f))

(u T (t T t)) T ((u T t) T (u T t))
(u F (t F u)) T ((u T t) F (u F u))
(u F (t F f)) T ((u T t) F (u F f))

(u T (u T t)) T ((u F u) T (u T t))
(u F (u F u)) T ((u F u) T (u F u))
(u F (u F f)) T ((u F u) T (u F f))

(u T (f T t)) T ((u F f) T (u T t))
(u T (f T u)) T ((u F f) T (u F u))
(u T (f T f)) T ((u F f) T (u F f))

(f T (t T t)) T ((f T t) T (f T t))
(f F (t F u)) T ((f T t) T (f T u))
(f F (t F f)) T ((f T t) T (f T f))

(f T (u T t)) T ((f T u) T (f T t))
(f F (u F u)) T ((f T u) T (f T u))
(f F (u F f)) T ((f T u) T (f T f))

(f T (f T t)) T ((f T f) T (f T t))
(f T (f T u)) T ((f T f) T (f T u))
(f T (f T f)) T ((f T f) T (f T f))

The strict Lewis conditional works in this case, but it does not in others.

Using the standard Lukasiewicz conditional $p \to q$ defined by the table:

$p q (p \to q)$

 t t    T
 t u    U
 t f    F
 u t    T
 u u    T
 u f    U
 f t    T
 f u    T
 f f    T

$(p \to ( q \to r)) \to (( p \to q) \to ( p \to r))$

(t T (t T t)) T ((t T t) T (t T t))
(t U (t U u)) T ((t T t) U (t U u))
(t F (t F f)) T ((t T t) F (t F f))

(t T (u T t)) T ((t U u) T (t T t))
(t T (u T u)) T ((t U u) T (t U u))
(t U (u U f)) T ((t U u) U (t F f))

(t T (f T t)) T ((t F f) T (t T t))
(t T (f T u)) T ((t F f) T (t U u))
(t T (f T f)) T ((t F f) T (t F f))

(u T (t T t)) T ((u T t) T (u T t))
(u T (t U u)) T ((u T t) T (u T u))
(u U (t F f)) T ((u T t) U (u U f))

(u T (u T t)) T ((u T u) T (u T t))
(u T (u T u)) T ((u T u) T (u T u))
(u T (u U f)) U ((u T u) U (u U f))

(u T (f T t)) T ((u U f) T (u T t))
(u T (f T u)) T ((u U f) T (u T u))
(u T (f T f)) T ((u U f) T (u U f))

(f T (t T t)) T ((f T t) T (f T t))
(f T (t U u)) T ((f T t) T (f T u))
(f T (t F f)) T ((f T t) T (f T f))

(f T (u T t)) T ((f T u) T (f T t))
(f T (u T u)) T ((f T u) T (f T u))
(f T (u F f)) t ((f T u) T (f T f))

(f T (f T t)) T ((f T f) T (f T t))
(f T (f T u)) T ((f T f) T (f t u))
(f T (f U f)) T ((f T f) T (f T f))

This fails because of the value of u for the formula in the 15th line.

Using a strict or definite Lukasiewicz conditional defined as: $\Box ( p \to r)$

$p q (p \Rightarrow q)$

  t t    T
  t u    F
  t f    F
  u t    T
  u u    T
  u f    F
  f t    T
  f u    T
  f f    T

$(p \Rightarrow ( q \Rightarrow r)) \Rightarrow (( p \Rightarrow q) \Rightarrow ( p \Rightarrow r))$

(t t (t t t)) t ((t t t) t (t t t))
(t f (t f u)) t ((t t t) f (t f u))
(t f (t f f)) t ((t t t) f (t f f))

(t t (u t t)) t ((t f u) t (t t t))
(t t (u t u)) t ((t f u) t (t f u))
(t f (u f f)) t ((t f u) t (t f f))

(t t (f t t)) t ((t f f) t (t t t))
(t t (f t u)) t ((t f f) t (t f u))
(t t (f t f)) t ((t f f) t (t f f))

(u t (t t t)) t ((u t t) t (u t t))
(u t (t f u)) t ((u t t) t (u t u))
(u f (t f f)) t ((u t t) f (u f f))

(u t (u t t)) t ((u t u) t (u t t))
(u t (u t u)) t ((u t u) t (u t u))
(u f (u f f)) t ((u t u) f (u f f))

(u t (f t t)) t ((u f f) t (u t t))
(u t (f t u)) t ((u f f) t (u t u))
(u t (f t f)) t ((u f f) t (u f f))

(f t (t t t)) t ((f t t) t (f t t))
(f t (t f u)) t ((f t t) t (f t u))
(f t (t f f)) t ((f t t) t (f t f))

(f t (u t t)) t ((f t u) t (f t t))
(f t (u t u)) t ((f t u) t (f t u))
(f t (u f f)) t ((f t u) t (f t f))

(f t (f t t)) t ((f t u) t (f t t))
(f t (f t u)) t ((f t u) t (f t u))
(f t (f t f)) t ((f t u) t (f t f))

The strict version of the Lukasiewicz conditional repairs the deficiency allowed because the standard version permits conditionals with a value of u.