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,
123456715
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.
