Homotopy equivalence in Propositional Logic

Let $$\scr S, \scr S'$$ be two signatures with $$S$$ and $$S'$$ being two models in the language $$\scr S, \scr S'$$

Let $$f$$ and $$f'$$ be two reconstrual extentions as follows:

$$f: S \to S'$$ and $$f': S' \to S$$

The functions $$f$$ and $$f'$$ are just transformations preserving deductive entailments:

Let's say, $$\phi \vdash_{\scr S} \psi$$ for $$f(\phi) \vdash_{\scr S' } f(\psi)$$

Or, in general, $$S \vdash \phi \implies S' \vdash f(\phi)$$

Let's say there is an Identity function $$I_{s,s'}$$ mapping $$S \to S$$ and $$S' \to S'$$

If $$f(f')=I_s$$ and $$f'(f)=I_{s'}$$ then models $$S$$ and $$S'$$ are said to be homotopy equivalent.

What does homotopy equivalence mean in this context (Or, in general, when speaking of Models)? If my understanding is correct, there is a notion of continuity at play when we speak of homotopies. However, in this case how can we even speak of continuity since for propositional logic our universe of discourse, in most cases, is countable at most.

Relevant definitions:

Definition 1.4.3:

Let $$T$$ be a theory in $$\Sigma$$, let $$T'$$ be a theory in $$\Sigma'$$ and let $$f: \Sigma \to \Sigma'$$ be a reconstrual. We say that $$f$$ is a translation or interpretation of $$T$$ to $$T'$$, written $$f:T \to T'$$, just in case:

$$T \vdash \phi \implies T' \vdash f(\phi)$$

Definition 1.4.6:

"For each theory $$T$$ the identity relation $$1_T: T \to T$$ is given by the identity reconstrual on $$\Sigma$$. If $$f: T\to T'$$ and $$g: T'\to T$$ are translations (basically reconstrual extentions as given earlier) we let $$gf$$ denote the translation from $$T \to T$$ given by $$(gf)(p)=g(f(p))$$ for each atomic sentence $$p$$ of $$\Sigma$$. Theories $$T$$ and $$T'$$ are said to be homotopy equivalent, or simply equivalent, just in case there are translations $$f: T \to T'$$ or $$g: T' \to T$$ such that $$f(g) \simeq T'$$ and $$g(f)\simeq T$$

Source screen-shots:

Book: The Logic in Philosophy of Science, by Halvorson.

Theorem 4.6.17, attributed to Barrett by Halvorson says:

"Let T1 and T2 be theories with a common definitional extension. Then there are translations F:T1→T2 and G:T2→T1 that form a homotopy equivalence."

The scholia on the proof says: "We prove the converse of this theorem in 6.6.21."

Thus, if there exist two translations that form a homotopy equivalence, the two theories will have a common definitional extension.

The text on p. 126 reads: "The previous results show, first, that a definitional extension is conservative: it adds no new results in the old vocabulary. In fact, Proposition 4.6.13 shows that a definitional extension is, in one important sense, equivalent to the original theory. You may want to keep that fact in mind as we turn to a proposal that some logicians made in the 1950s and 1960s, and that was applied to philosophy of science by Glymour (1971). According to Glymour, two scientific theories should be considered equivalent only if they have a common definitional extension."

So, if two scientific theories should be considered equivalent, then they will have a common definitional extension.

Thus, Halvorson would appear to interpret Glymour's position that if two theories should be considered equivalent, then they will have a homotopy equivalence. Conversely, if no homotopy equivalence can get formulated (in other words, no homotopy equivalence exists), then the two theories should get considered distinct.

Consequently, it appears that Halvorson would argue that Glymour's position on scientific theories (and perhaps Halvorson's also?) comes as the separation/distinctness of scientific theories becomes clear from the impossibility of a homotopy equivalences, and that if two scientific theories are the same, then there must exist a homotopy equivalence. Apparently, homotopy equivalence provides a way to test whether two scientific are distinct or equivalent.