How can we formalize the claim that these two languages are equally expressive?

Question

Let T be a stripped-down version of propositional logic, whose only connectives are ¬ and ➝, and suppose T can prove all the usual theorems that can be formed from only these two connectives. Let T’ be the same theory but with the additional connective ∨, and the axiom schemas (⍺ ∨ β) ➝ (¬⍺ ➝ β) and (¬⍺ ➝ β) ➝ (⍺ ∨ β) [where ⍺ and β denote arbitrary propositional variables A, B, C, ...].

Can we formalize the notion that T and T’ are equally expressive?

Intuitively, T can express every proposition that T’ can, because we can replace all the ∨'s with ¬'s and ➝'s, yielding a formula in T that is equivalent to the original (according to T’). That is, if ψ is a formula of T’, and ψ* is the formula obtained by making the replacement (⍺ ∨ β) ➝ (¬⍺ ➝ β) in ψ until no ∨'s remain, then T’ can prove ψ* ➝ ψ and it can also prove ψ ➝ ψ*. Indeed, the Wikipedia article on extensions by definition highlights an analogous fact (in the different context of predicate logic) and then claims

Semantically, the formula ψ* has the same meaning as ψ, but the [new symbol in T’] has been eliminated.

But can this last claim (that the two meanings are identical) be justified rigorously, apart from just "seeing" that the two formulas mean the same thing? A first instinct is to point to the syntactic fact that T’ can prove the two formulas are equivalent—but this has an issue. For each formula ψ in T’, instead of defining ψ* as above, one can let ψ* be any formula of T, as long as it is either a theorem (non-theorem) of T whenever ψ is a theorem (non-theorem) of T’. Then the equivalence of ψ and ψ* still holds in T’, even if the two formulas have nothing to do with each other.

Answer 1

I think what lies behind your question is the fact that you (and the linked Wikipedia article) are using the word 'meaning' rather too loosely. Your example is concerned with truth conditions, which are purely extensional. In classical propositional logic, ⍺ ∨ β is logically equivalent to ¬⍺ ➝ β so they share the same truth conditions. But it does not follow that those sentences mean the same thing. If they did, then by extension every logical truth would mean the same as every other logical truth.

Following Frege, it is common to say that a sentence has an intension as well as an extension. Given that George Orwell is identical with Eric Blair it follows that the sentences, "George Orwell wrote 1984" and, "Eric Blair wrote 1984" have the same truth conditions. But they are not equivalent in their intension. Someone might believe one and not the other. The concept of the meaning of an expression is more fine-grained than its truth conditions. Two sentences may even be necessarily extensionally equivalent but differ hyperintensionally.

When adding a new feature to a language, such as a connective, it may be that the new language constitutes a conservative extension of the original. This implies that the new language cannot prove any new theorems about the language of the original theory. Of course it can prove theorems about the new connective, so it is more expressive in that sense, but it does not extend what is provable in the original language.

What may be related to your question is the issue of under what conditions two systems of formal logic might be regarded as the same. Given two formal systems, are they distinctly different, or are they just the same system expressed in a different way? In recent years, Eduardo Barrio and co-workers have explored this issue by reference to a formal logic called ST that is closely related to classical logic. I've given a couple of references and you can find more on philpapers.org. If you don't have time to read the papers, the short version of Barrio's view is that for two systems to be identical, it is not sufficient for them to have the same set of theorems, nor the same set of valid inferences. They must share the same valid metainferences and valid metametainferences all the way up the hierarchy of consequence relations.

Eduardo Barrio, Federico Pailos and Damian Szmuc, (Meta)Inferential Levels of Entailment beyond the Tarskian Paradigm, Synthese 198, (S22) pp. 5265-5289 (2019).

Eduardo Barrio, Lucas Rosenblatt and Diego Tajer, The Logics of Strict-Tolerant Logic, Journal of Philosophical Logic 44, pp. 551-571 (2015).

Answer 2

I'm approaching this from the semantics of expressivity that I'm used to, that used in reference to programming languages. It seems to me that the notion is fundamentally the same for mathematical logic, a connection implicitly recognized by the Curry-Howard correspondence.

The article seems to rightly account for an important distinction and reports expressivity as a polyseme. On the one hand, the range of ideas, which I would characterize as the ontological primitives of the language such as types, data structures, syntactic constructs, among others is, according to the article, is known as 'theoretic expressivity'. This is in distinction to the concision and ease of features using the language which is called by the article 'practical expressivity'.

Thus, the scenario you craft, though it's in mathematical logic rather than a language for programming has essentially the same distinction. We can talk about the variety of axioms and definitions that put forth in terms of interpretations of a model (PhilSE), for instance, and by adding axioms and definitions enriches the expressivity of the model which would be theoretic expressivity.

In computer science, practical expressivity is often called sugaring or syntactic sugar. This, of course, doesn't affect the theoretic expressivity, but simply makes it easy to write and comprehend the programming constructs. So, through the eyes of a computer scientist, you're simply asking whether or not the example you provides has increased expressivity.

So... yes, the language has more practical expressivity, because a definition reduces an expressions complexity by substituting one term for a complex of terms, but no, the language does not have more theoretical expressivity, because fundamentally no new meanings have been added to the language. I've looked in some resources I have (textbook on model theory, Encyclopedia of Philosophy, Encyclopedia of Computer Science, SEP, et al.) and I can't find any authoritative accounting other than the WP article.

Answer 3

Here is an approach using models, suppose our vocabulary contains countably many prop symbols. Let L1 denote the negation + implication fragment of prop logic, let L2 extend L1 with 'v' with the classic semantics. Build up their model theoretic semantics in the typical manner, giving rise to ⊨L1 and ⊨L2.

Now, L1 is at least as expressive as 𝐿2, in symbols, 𝐿1≤𝐿2 , if every 𝐿1 -sentence ϕ is equivalent to some 𝐿2-sentence ψ in the following manner: for all structures M(⊨L1)ϕ⟺M(⊨L2)ψ.

Now, clearly L1 is bounded by L2 in terms of expressive power. For the other direction, use your proposed translation and we are done.

Crucially, the notion of structure remains the same in our meta- theory. (this may not be the case when moving to a logic second order and above, see: Henkin vs standard semantics). I suppose there is likely a proof from algebraic logic as well, discussing minimal generating sets, but I leave this to someone else.