If we consider this sentence: ¬(P → Q) ⊢ ¬Q as a purely symbolic calculus, I would like to explore some kind of “reverse mathematics” where the question is, which axioms are needed in order for that string of symbols to be “true”?

This is how far I’ve come in my analysis. I’d really appreciate some more experienced people filling in some of the gaps in my knowledge.

Spaces excluded, we technically see 7 distinct symbols in the string above: ¬(P→Q)⊢

I did say “as a purely symbolic calculus”, but I am actually going to start with some assumptions about the interpretation of the symbols. ¬ is a unary function. → and ⊢ are binary functions. And P and Q are variables. I will not worry about (), which I see as just a convenient aid for parsing these symbols. I can also add in the punctuation symbol “,” (a comma).

We could consider replacing these familiar symbols with arbitrary ones to try to distance ourselves from common associations. The above sentence could be written,


Where 1 is “not”, 2 is “(“, 3 is P, 4 is “implies”, etc.

To standardize the form, I will always write the function before its list of arguments. So we have:

If 1(2(X, Y)), then 1(Y). (1 is negation, 2 is implication).

If we want to take out the turnstile symbol, I have only the issue that it seems we need to introduce an “equality” symbol:

3(1(2(X,Y)) 4 1(Y)

which says something like, “the entailment of the negation of the implication of two variables x and y is the negation of y”. (But I need to think way, way more about what introducing an equality symbol here might do or change.)

These questions make me wonder:

Ideally, I would have some kind of highly formal, parsible language, as above, which can actually be used to specify various logics. So I could use it to say, “give me the logic which has 2 unary functions, 5 trinary functions, and 2 variables”.

Basically, I’m super tired so I can’t present the train of thought as well as I wanted. Might have to come back to this tomorrow.

The short summary now is:

In order to do reverse mathematics on the sort of “arbitrary” string above, we ideally would be enumerating over all possible “logics” (under a certain definition of a “logic”), to see what relationship the “theorem” has to various axioms, perhaps? (Now I realize there may be 2 parameters of variation… 1. What is the logical language? 2. What are the axioms within that language?)

These ideas are getting pretty wild but I think it’s awesome how with cumulative hierarchies of sets, there is basically an “ordering” on sets (or some sort of partial ordering where all members of one generation are all “greater than” all members of a previous generation.)

So, I’m imagining you could maybe use a similar strategy to be able to order logics, from the most minimal, to a next generation of logics somehow built from the ones of the previous round.

Anyway, somehow some of the thoughts above led me to the question of if you need a more expressive logic to be able to describe a logic logically. I have been curious lately about how entailment symbols and material implication symbols are similar or different. It seems like an entailment symbol is actually just material implication, “one level up”. There are logical formation rules for how a first generation of symbols form expressions, but then there is a second logical system which has its own formation rules for how expressions for valid sentences. In other words, if we just replaced the word “well formed” with a 1 or a 0, we might see a hierarchy of more or less truth values.

I know this is super sloppy. Hoping to refine it tomorrow, with the aid of insight and feedback from commenters.

  • 3
    No. Primitive recursive arithmetic with bounded transfinite induction that Gentzen used to prove consistency of Peano arithmetic is incomparable in expressiveness or deductive strength to Peano arithmetic, neither stronger nor weaker.
    – Conifold
    Commented Mar 14 at 5:40
  • 1
    What’s the motivation to encode symbols as numbers in this case? To do some computation over them? Commented Mar 14 at 5:56
  • 1
    For self-reference in general see Raymond Smullyan, Diagonalization and Self-Reference (Oxford, 1994) as well as Melvin Fitting, Incompleteness in the Land of Sets (College, 2007) Commented Mar 14 at 8:32
  • @ayylien To remove associations we have on the symbols and focus purely on a symbol rearranging game (at least at first). They do not have to be numbers. They could be dots or shapes or colors or emoji or sounds or smells or anything identifiable as “a different thing”. Commented Mar 14 at 18:31
  • 2
    Your post seems to be conflating the strength of the language, i.e. what sentences a formal language is capable of expressing, with the strength of the logic, i.e. which sentences the logic proves as theorems. In general, logics are different and cannot be ordered in terms of strength. To a limited extent some logics may be ordered in that the set of the theorems of one may be a proper superset of the set of theorems of another. Classical logic is strictly stronger than intuitionistic logic, which in turn is strictly stronger than minimal logic.
    – Bumble
    Commented Mar 15 at 2:30

2 Answers 2


So, I've been thinking about this question, and I think I'll clarify how I see it. You ask:

Do you require a more expressive logic to describe a less expressive one?


But I want to widen the scope a bit, because I believe the best way to respond to this is that according to the Curry Howard correspondence, there is a general equivalency between logics, programs, and categorical structures. So, you're not thinking big enough, because what a formal logic is, is ultimately a grammar. Enter the Chomskyian hierarchy. From WP:

The Chomsky hierarchy (infrequently referred to as the Chomsky–Schützenberger hierarchy1) in the fields of formal language theory, computer science, and linguistics, is a containment hierarchy of classes of formal grammars. A formal grammar describes how to form strings from a language's vocabulary (or alphabet) that are valid according to the language's syntax.

Since you're familiar with NLP, let me say it this way: the answer to your question is yes, but not just in terms of logics, but the grammars that express them. Consider the difference between CFGs and CSGs. In the production rules of a CFG, one has a deterministic way to build a DAG from the grammar and avoid ambiguity when building an AST. But, this means the expressivity is impoverished.

So, when talking about two logics, if one is expressed in a CFG and another is not, the more expressive can express the propositions of the less expressive. However, ultimately, in formal systems, we tend to bottom out the semantics of the theory in a metatheory that is expressed in natural language which has the richest form of expressivity. So, we don't express FOL in a HOL and then describe it in NL, but rather just compare an FOL with an HOL in terms of semantics, completeness, etc. in NL.

  • I'm formalizing it (partially) in Coq right now, a computational system for logical proof. Eager to share. And I definitely thought of the Chomsky hierarchy but didn't cram it in. But it will come into play I feel. Commented Mar 15 at 16:31
  • @JuliusH. Sure. Cool. If you weren't aware, Coquand wrote the SEP article on Type Theory. plato.stanford.edu/entries/type-theory You might also be interested in LF. en.wikipedia.org/wiki/Logical_framework What exactly are you building?
    – J D
    Commented Mar 15 at 18:05
  • @JuliusH. please share! I'm learning coq rn so I'm curious what you got Commented Mar 15 at 18:49

consider this sentence: ¬(P → Q) ⊢ ¬Q . . . which axioms are needed in order for that string of symbols to be “true”?

I initially proposed P ⊢ ¬(P → Q) → ¬Q, but this is wrong. Sorry!

Edited answer:

An axiom X is an assumption. If X is an axiom, we don't just assume ¬(P → Q), we also assume X, so the expression we have to prove is not ¬(P → Q) ⊢ ¬Q, it is X ∧ ¬(P → Q) ⊢ ¬Q . . .

And if X ∧ ¬(P → Q) ⊢ ¬Q is true, the implication X ⊢ ¬(P → Q) → ¬Q is also true, but now X is "distinguished" from ¬(P → Q), and you have your answer: If X is true, then ¬(P → Q) → ¬Q is true.

Same thing, though, X ⊢ ¬(P → Q) → ¬Q is just true (but not "true"!).

which can actually be used to specify various logics.

There is just one logic that we know of, so anything which is not it is just not logic. There cannot be "various logics".

The way mathematicians use the word "logic" is just equivocation.

What mathematicians call "logics" are mathematical theories, not logics.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .