6
$\begingroup$

There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism).

But I can imagine a different connection: There seems to be a similarity between type checking and checking whether a particular mathematical structure satisfies a set of axioms.

We might say that propositions (axioms) are formalized as types (just as in the CH-isomorphism), but that now, an instance of a proposition (i.e. an instance of that type) is not a proof of the proposition, but a model of it. Type checking then takes the role of checking whether a particular mathematical structure is indeed a model of that axiom.

Is there a formalization of "checking whether a structure is a model of a proposition" as type checking? Could you explain such a formalization, or point to an explanation of it?

$\endgroup$
3
$\begingroup$

The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.

For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1\times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1\land Q_2$.

On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $\varphi_1$ and $\varphi_2$, there's no canonical way of constructing a model of the conjunction $\varphi_1\land \varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.

It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $\varphi$ essentially an encoding of a proof of $\varphi$, and then relying on the usual Curry-Howard correspondence.

$\endgroup$
  • $\begingroup$ very interesting $\endgroup$ – user56834 Feb 4 at 15:56
  • $\begingroup$ Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory? $\endgroup$ – user56834 Feb 7 at 18:27
  • $\begingroup$ I'm asking that because I think your point is interesting and I'd like to understand it better $\endgroup$ – user56834 Feb 9 at 6:00
2
+100
$\begingroup$

Yes, there are two notions of "fit into" here:

  • Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
  • Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.

I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.

  • For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
  • Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
  • Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
  • In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
  • If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.

Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.

Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.

$\endgroup$
  • 1
    $\begingroup$ @user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges. $\endgroup$ – Nikolaj-K Feb 3 at 15:38
  • $\begingroup$ I re-read it, and I admit I was being uncharitable. My apologies. $\endgroup$ – user56834 Feb 9 at 6:21
  • $\begingroup$ What do you think of Alex Kruckman's answer? $\endgroup$ – user56834 Feb 9 at 6:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.