nForum - Discussion Feed (closed category) 2022-09-27T07:58:19-04:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher gintaras comments on "closed category" (95567) https://nforum.ncatlab.org/discussion/4632/?Focus=95567#Comment_95567 2021-09-29T04:43:17-04:00 2022-09-27T07:58:18-04:00 gintaras https://nforum.ncatlab.org/account/3039/ The opposite ordered space remains ordered space. So we can ask which of two categories is closed with mappings$L^x_{y,z}$. Other categories doesn't allow opposite category. For example the category ... The opposite ordered space remains ordered space. So we can ask which of two categories is closed with mappings
$L^x_{y,z}$. Other categories doesn't allow opposite category. For example the category of Sets or Additive groups.
We can add two functions $+g$ if we have addition in target space, but not in source space.
So the category can be closed wih mappings $L^x_{y,z}$ without having defined mappings $R^x_{y,z}$.
Interesting closed category is provided by uniform mappings of uniform spaces. ]]>
Mike Shulman comments on "closed category" (85065) https://nforum.ncatlab.org/discussion/4632/?Focus=85065#Comment_85065 2020-06-03T05:37:31-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Added remark that a symmetric closed category is automatically associative as a promonoidal category, hence a weaker representability condition suffices to make it monoidal. diff, v62, current

Added remark that a symmetric closed category is automatically associative as a promonoidal category, hence a weaker representability condition suffices to make it monoidal.

]]>
Mike Shulman comments on "closed category" (82188) https://nforum.ncatlab.org/discussion/4632/?Focus=82188#Comment_82188 2020-01-07T20:51:17-05:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Added one axiom to prounital closed categories. diff, v60, current

Added one axiom to prounital closed categories.

]]>
Keith Harbaugh comments on "closed category" (77263) https://nforum.ncatlab.org/discussion/4632/?Focus=77263#Comment_77263 2019-04-09T19:09:02-04:00 2022-09-27T07:58:19-04:00 Keith Harbaugh https://nforum.ncatlab.org/account/1567/ Added link to published version of Oleksandr Manzyuk, _Closed categories vs. closed multicategories (TAC Vol. 26, 2012). Hope I got your formatting schemes not too messed up! diff, v58, current

Added link to published version of Oleksandr Manzyuk, _Closed categories vs. closed multicategories (TAC Vol. 26, 2012). Hope I got your formatting schemes not too messed up!

]]>
Mike Shulman comments on "closed category" (69406) https://nforum.ncatlab.org/discussion/4632/?Focus=69406#Comment_69406 2018-06-11T03:09:14-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Change “semi-closed category” to “prounital closed category” diff, v56, current

Change “semi-closed category” to “prounital closed category”

]]>
Mike Shulman comments on "closed category" (69405) https://nforum.ncatlab.org/discussion/4632/?Focus=69405#Comment_69405 2018-06-11T03:08:06-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ You mean a multicategory where there are universal binary maps A,B&rightarrow;A&otimes;BA,B \to A\otimes B but not a universal nullary map &sdot;&rightarrow;I\cdot \to I? Yes, ...

You mean a multicategory where there are universal binary maps $A,B \to A\otimes B$ but not a universal nullary map $\cdot \to I$?

Yes, that’s what I meant. Since that’s the monoidal analogue of prounital closed categories, which (conjecturally) correspond to multicategories that have nullary maps, but have a “binary internal-hom” but not a “nullary one”.

]]>
Noam_Zeilberger comments on "closed category" (69401) https://nforum.ncatlab.org/discussion/4632/?Focus=69401#Comment_69401 2018-06-10T15:17:50-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ “prounital”? Sounds good to me! There’s no name for a multicategory that has binary tensor products but not a unit, either. You mean a multicategory where there are universal binary ...

“prounital”?

Sounds good to me!

There’s no name for a multicategory that has binary tensor products but not a unit, either.

You mean a multicategory where there are universal binary maps $A,B \to A\otimes B$ but not a universal nullary map $\cdot \to I$? I don’t know a name for that, but I think the multicategory equivalent of a semigroup category is a multicategory with no nullary operations that is representable in the standard sense, so “representable constantless multicategory” (adopting the terminology you suggested before), or “representable non-unitary multicategory” (using Fresse’s terminology for the corresponding operads, which I don’t find particularly evocative).

]]>
Mike Shulman comments on "closed category" (69399) https://nforum.ncatlab.org/discussion/4632/?Focus=69399#Comment_69399 2018-06-10T12:36:19-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ “prounital”?

“prounital”?

]]>
Mike Shulman comments on "closed category" (69393) https://nforum.ncatlab.org/discussion/4632/?Focus=69393#Comment_69393 2018-06-10T09:15:21-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Hrm, I suppose you’re right. There’s no name for a multicategory that has binary tensor products but not a unit, either.

Hrm, I suppose you’re right. There’s no name for a multicategory that has binary tensor products but not a unit, either.

]]>
Noam_Zeilberger comments on "closed category" (69386) https://nforum.ncatlab.org/discussion/4632/?Focus=69386#Comment_69386 2018-06-09T05:07:18-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ Re #41, I wouldn’t call these “semi-closed categories” since that name has already been used by Bourke (#16) for the weaker structure consisting of just a bifunctor [&minus;,&minus;]:C ...

Re #41, I wouldn’t call these “semi-closed categories” since that name has already been used by Bourke (#16) for the weaker structure consisting of just a bifunctor $[-,-] : C^{op} \times C \to C$ equipped with the compositor transformations $[Y,Z] \to [[X,Y],[X,Z]]$ satisfying a pentagon axiom. And as you know (#17), that terminology is natural because such semi-closed categories indeed correspond to (biased-lax/skew) semigroups in $Prof$ with a representability requirement.

What’s tricky here is that a “non-unital” closed category is actually equipped with a unit (in $Prof$), it is just not representable. I’m not sure if there is a succinct way of conveying that…perhaps something like a “semi-closed category with a presheaf of global elements”?

]]>
Mike Shulman comments on "closed category" (69337) https://nforum.ncatlab.org/discussion/4632/?Focus=69337#Comment_69337 2018-06-07T00:52:22-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ I suppose a better name for “non-unital closed categories” would be “semi-closed categories”, by analogy to other uses of “semi-” for non-unitality (e.g. semigroup, semisimplicial set, ...

I suppose a better name for “non-unital closed categories” would be “semi-closed categories”, by analogy to other uses of “semi-” for non-unitality (e.g. semigroup, semisimplicial set, semicategory…)

]]>
Mike Shulman comments on "closed category" (69336) https://nforum.ncatlab.org/discussion/4632/?Focus=69336#Comment_69336 2018-06-07T00:49:48-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ List some examples of closed monoidal categories whose closed structure is more natural than their monoidal structure. diff, v54, current

List some examples of closed monoidal categories whose closed structure is more natural than their monoidal structure.

]]>
Mike Shulman comments on "closed category" (69208) https://nforum.ncatlab.org/discussion/4632/?Focus=69208#Comment_69208 2018-06-01T11:49:24-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ I don’t really understand all this skew business, and I’m not really motivated to put in the effort right now, since I don’t know or care about any of the relevant examples yet, and from a pure ...

I don’t really understand all this skew business, and I’m not really motivated to put in the effort right now, since I don’t know or care about any of the relevant examples yet, and from a pure category-theoretic point of view it seems bizarre to me to have the unit morphisms pointing in different directions. (Even more bizarre than a noninvertible biased associator.) I accept that they do arise naturally in some contexts and are useful for some purposes, but the correspondence between non-unital closed categories and closed multicategories seems to me something much more basic, that should be simple to motivate, explain, and prove, without having to descend into this more exotic skew business.

]]>
Noam_Zeilberger comments on "closed category" (69207) https://nforum.ncatlab.org/discussion/4632/?Focus=69207#Comment_69207 2018-06-01T11:25:07-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ By the way, I think you meant M:C op&times;C op&times;C&rightarrow;SetM : C^{op}\times C^{op}\times C\to Set. Oops…I mean, that was just to prove my point that keeping track of all ...

By the way, I think you meant $M : C^{op}\times C^{op}\times C\to Set$.

Oops…I mean, that was just to prove my point that keeping track of all the directions/signs can be tricky! :-)

]]>
Noam_Zeilberger comments on "closed category" (69206) https://nforum.ncatlab.org/discussion/4632/?Focus=69206#Comment_69206 2018-06-01T11:20:49-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ Those are the same as my calculations: it’s just that since &lambda;\lambda is an isomorphism, it could just as well point the other way. The reason I think it should point the other way is ...

Those are the same as my calculations: it’s just that since $\lambda$ is an isomorphism, it could just as well point the other way. The reason I think it should point the other way is because the criterion of correctness for the definition should be that it coincides with closed multicategories, and we know that multicategories can be identified with normal unbiased lax monoids in $Prof$.

Hmm. It’s subtle, but I have a different intuition. Or I guess it’s rather that I don’t want to start from an assumption of left normality. I think the notion of “skew” multicategory discussed by Bourke and Lack is quite natural, and there, what corresponds to the left unitor is the mapping from “tight” morphisms $A_0;A_1,\dots,A_n \to B$ to “loose” morphisms $A_0,A_1,\dots,A_n \to B$. My intuition coming from programming languages is that this corresponds to an inclusion of (“pure”) values into (“effectful”) computations, and so I think it will be interesting to consider closed skew multicategories which are not left normal (corresponding to extensions of the lambda calculus with effects). That is quite informal intuition, though.

In any case, I wanted to elaborate a bit more formally what I was alluding to at the end of #29, because I think it might be related to your ideas in #22, and possibly to this question of left normality. Given a (unital or non-unital, not necessarily left normal) skew closed category $C$, we can consider its category of covariant presheaves $[C,Set]$ as a right-skew monoidal category (or alternatively $[C,Set]^{op}$ as a left-skew monoidal category of course). Then it is interesting to consider _monoids_in $[C,Set]$, which correspond to “deductively closed presheaves” $R : C \to Set$, in the sense that the multiplication map gives an extranatural transformation

$m : R(a \to b) \times R(a) \to R(b)$

corresponding to “modus ponens”, while the unit gives a natural transformation

$u : U(a) \to R(a)$

corresponding to the inclusion of all “tautologies” into $R$.

Let me restrict now to the unital, 2-enriched case, because that’s what I considered in the aforementioned paper (but I think it can be extended to the non-unital, Set-enriched case). In this case, a monoid $R$ in $[C,2]$ (where $C$ is a unital skew closed preorder) corresponds to an upwards closed subset of $C$ such that the following pair of conditions hold:

$\frac{a \to b \in R \quad a \in R}{b \in R} \qquad \frac{}{I \in R}$

Given such a monoid, we can construct a new preordered category $C/R = (C,\le_R)$ with the same objects as $C$ but where $a \le_R b$ iff $a\to b \in R$. The fact that this relation is transitive relies on both the multiplication $m$ of $R$ and the original associator $\alpha$/compositor $L$ of $C$, while the fact that it is reflexive relies on the unit $u$ of $R$ together with the left unitor $\lambda$ of $C$. There is also an evident embedding $i : C \to C/R$ (again relying on the left unitor $\lambda$), in the sense that the preorder $\le_R$ is an extension of $\le$.

But now we might wonder whether $C/R$ is (skew) closed, and whether we can legitimately see it as a quotient. And here is where things get more interesting: although we can show that the original operation $a\to b$ is monotone in $b$ relative to the coarser order $\le_R$, it need not be antitone in $a$. So this is where we need to impose an additional condition of closure under “double-negation introduction”:

$\frac{a \in R}{(a \to b) \to b \in R}$

Note that this dni-condition is equivalent (at least in the 2-enriched case) to the existence of a natural transformation $-\otimes R \Rightarrow R\otimes-$, where $\otimes$ is the multiplication operation in $[C,2]$. Given this additional closure condition, we can prove that $a \to b$ is antitone in $a$ relative to $\le_R$ and thus defines a functor $(C/R)^{op} \times C/R \to C/R$, which together with the original unit $I$ turns $C/R$ into a left normal skew-closed category. Moreover we can show that $(C/R, i : C \to C/R)$ has the appropriate universal property of the quotient.

I did not try to work this out, but my intuition was that in the $Set$-enriched case, $R$ could be thought of as (generated by) a family of typed combinators, which is then used to construct a closed category $C_R$ with additional structure. Perhaps that aligns with some of your ideas?

]]>
Mike Shulman comments on "closed category" (69205) https://nforum.ncatlab.org/discussion/4632/?Focus=69205#Comment_69205 2018-06-01T11:17:23-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ By the way, I think you meant M:C op&times;C op&times;C&rightarrow;SetM : C^{op}\times C^{op}\times C\to Set. I think I see the point now that viewing them as left-normal skew monoids, ...

By the way, I think you meant $M : C^{op}\times C^{op}\times C\to Set$.

I think I see the point now that viewing them as left-normal skew monoids, whose corresponding LBC-algebras are also left-normal and hence equivalently left-normal lax monoids, would make the identification of non-unital closed categories with closed multicategories literally a consequence of Bourke-Lack rather than requiring the argument to be redone in the biased-lax case. Morally I still think the latter ought to be done, though… but I might be too lazy to do it.

]]>
Mike Shulman comments on "closed category" (69204) https://nforum.ncatlab.org/discussion/4632/?Focus=69204#Comment_69204 2018-06-01T09:34:32-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Those are the same as my calculations: it’s just that since &lambda;\lambda is an isomorphism, it could just as well point the other way. The reason I think it should point the other way is ...

Those are the same as my calculations: it’s just that since $\lambda$ is an isomorphism, it could just as well point the other way. The reason I think it should point the other way is because the criterion of correctness for the definition should be that it coincides with closed multicategories, and we know that multicategories can be identified with normal unbiased lax monoids in $Prof$.

]]>
Noam_Zeilberger comments on "closed category" (69203) https://nforum.ncatlab.org/discussion/4632/?Focus=69203#Comment_69203 2018-06-01T08:27:31-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ Pondering a bit more what you are saying and trying to connect it to things that I know, I think that the definition of “non-unital closed category” you are aiming for should begin with a skew ...

Pondering a bit more what you are saying and trying to connect it to things that I know, I think that the definition of “non-unital closed category” you are aiming for should begin with a skew monoid in $Prof$ (like I was suggesting in #21) rather than a biased lax monoid. Keeping track of the directions can be tricky (nice table at lax monoidal category, by the way!), so let me spell out my calculations.

Start with a right-skew monoid $(A, M : A \otimes A ⇸ A, U : 1 ⇸ A, \alpha, \lambda, \rho)$ in $Prof$, where we write $A = C^{op}$ for the opposite of some (non-unital closed) category $C$, so that $M$ and $U$ correspond to functors $M : C \times C \times C^{op} \to Set$ and $U : C \to Set$. Now we ask that $M$ is representable by a functor $[-,-] : C^{op} \times C \to C$ in the sense that

$M(c,a;b) = C(c,[a,b])$

By profunctor composition the two halves of associativity $L = M(M(-,-),-)$ and $R = M(-,M(-,-))$ are calculated as follows

$L(d,e,a;c) = \int^b C(d, [e,b]) \times C(b, [a,c]) \cong C(d,[e,[a,c]]) \qquad R(d,e,a;c) = \int^b C(d,[b,c]) \times C(e,[a,b])$

so that the right-to-left associator $\alpha : R \Rightarrow L$ yields the family of “compositor” maps

$L_{b,c}^a : [b,c] \to [[a,b],[a,c]]$

in $C$. Now, consider the profunctors $U_L = M(U,-)$ and $U_R = M(-,U)$. I calculate them as follows:

$U_L(a;b) = \int^c U(c) \times C(c,[a,b]) \cong U([a,b]) \qquad U_R(c;b) = \int^a C(c,[a,b]) \times U(a)$

Therefore the left unitor $\lambda : A \Rightarrow U_L$ corresponds to a transformation

$C(a,b) \to U([a,b])$

while the right unitor $\rho : U_R \Rightarrow A$ corresponds to a transformation

$U(a) \to C([a,b],b)$

So this is what one could call a “non-unital skew closed category”. If you additionally impose that $\lambda$ is an isomorphism (= left normality) then I think what comes out is what you are calling a “non-unital closed category”.

]]>
Mike Shulman comments on "closed category" (69197) https://nforum.ncatlab.org/discussion/4632/?Focus=69197#Comment_69197 2018-05-31T17:44:24-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Ah, nice! I thought there might be some argument like that, but I didn’t see it.

Ah, nice! I thought there might be some argument like that, but I didn’t see it.

]]>
Noam_Zeilberger comments on "closed category" (69195) https://nforum.ncatlab.org/discussion/4632/?Focus=69195#Comment_69195 2018-05-31T17:38:52-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow? Yes. (And I proved something similar as Prop. 2.23 in the above link.) The ...

Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow?

Yes. (And I proved something similar as Prop. 2.23 in the above link.) The key is to prove the following rule as a lemma (in the notation of #28):

$\frac{A \to B}{(B \to C) \to (A \to C)}$

Proof: Assume $A \to B$. By the “evaluation”/”dni” rule, we have $((A \to B) \to (A \to C)) \to (A \to C)$ (taking $A \to C$ as the “answer type” of double-negation introduction). Composing this with the “B” axiom $(B\to C) \to ((A \to B) \to (A \to C))$, we obtain $(B \to C) \to (A \to C)$. (Here I am using the auxiliary lemma that it is possible to compose a deduction $f : X \to Y$ with a deduction $g : Y \to Z$ to obtain a deduction $h : X \to Z$: first we apply modus ponens on the axiom $(Y \to Z) \to ((X \to Y) \to (X \to Z))$ together with $g$ to obtain a deduction $g' : ((X \to Y) \to (X \to Z))$, then we apply modus ponens on $g'$ with $f$ to obtain $h : X \to Z$.)

Now we can derive the functoriality rule

$\frac{A_2 \to A_1 \quad B_1 \to B_2}{(A_1 \to B_1) \to (A_2 \to B_2)}$

as follows. Suppose given $f : A_2 \to A_1$ and $g : B_1 \to B_2$. First we apply modus ponens on the B axiom and $g$ to obtain $g' : (A_2 \to B_1) \to (A_2 \to B_2)$. Then we apply the lemma to $f$ to obtain $f' : (A_1 \to B_1) \to (A_2 \to B_1)$. Finally we compose $f'$ and $g'$ to obtain the desired $h : (A_1 \to B_1) \to (A_2 \to B_2)$.

]]>
Mike Shulman comments on "closed category" (69193) https://nforum.ncatlab.org/discussion/4632/?Focus=69193#Comment_69193 2018-05-31T16:36:58-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow? (I don’t quite follow the notation.)

Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow? (I don’t quite follow the notation.)

]]>
Mike Shulman comments on "closed category" (69192) https://nforum.ncatlab.org/discussion/4632/?Focus=69192#Comment_69192 2018-05-31T16:35:24-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Following the link from Bourke-Lack to their companion paper, I see that my MO question is answered there in the case of skew-monoidal categories. The biased-lax case where both unit morphisms go in ...

Following the link from Bourke-Lack to their companion paper, I see that my MO question is answered there in the case of skew-monoidal categories. The biased-lax case where both unit morphisms go in the same direction ought to be basically the same but simpler.

]]>
Noam_Zeilberger comments on "closed category" (69190) https://nforum.ncatlab.org/discussion/4632/?Focus=69190#Comment_69190 2018-05-31T14:27:03-04:00 2022-09-27T07:58:19-04:00 Noam_Zeilberger https://nforum.ncatlab.org/account/1141/ What does &le;\le mean in a Hilbert system? Or is that your point in #24 that it doesn’t mean anything? Well, I guess my point is more that assuming one admits such binary judgments then ...

What does $\le$ mean in a Hilbert system? Or is that your point in #24 that it doesn’t mean anything?

Well, I guess my point is more that assuming one admits such binary judgments then functoriality is naturally formulated this way, but it is still a rule schema that would be required in addition to modus ponens.

I think of a Hilbert system as a deductive system whose judgments are simply $P\;true$ (usually written just “$P$”) for some proposition $P$, with no hypotheticals, and in which most properties of the system are expressed by axioms and often the rule that has premises is modus ponens $\frac{A \to B \quad A}{B}$.

Yeah, I’m okay with that terminology.

But some Hilbert systems have other rules, and it seems like this one could be formulated as $\frac{A_2\to A_1 \quad B_1 \to B_2}{(A_1\to B_1)\to (A_2\to B_2)}$. Is that right?

Right. What I understood from Zielonka’s paper is that he proves that having such a rule schema is in a sense unavoidable. But let me look again at his paper and try to be a bit more careful. Looks. Right…

First of all, he is talking about the (non-)existence of a “finite axiomatization where the only rule of inference is the cut rule”. This is not exactly a “Hilbert system” in your sense, but pretty close, what we would probably understand as a freely generated multicategory. He starts by setting up an infinite hierarchy of axioms, including all sequents of the form

$x/y, y \to x$

as axioms of rank 0 (so he is interpreting $x/y$ as right division), then all sequents

$\to x/x$ $\to ((x/z)/(y/z))/(x/y))$

as axioms of rank 1, and finally a sequent of the form

$\to x/(x/y)$

of rank $n+1$ whenever $\to y$ is an axiom of rank $n$. Call $C$ the system with all such axioms (closed under the cut rule), and $C_n$ the system with axioms restricted to rank $\le n$. What Zielonka shows is that $C$ is logically equivalent to (the $/$-fragment of) Lambek’s sequent calculus $L$, but there are sequents which are derivable in $C_{n+1}$ which are not derivable in $C_n$. Therefore $L$ is not finitely axiomatizable.

Okay, so that is starting to ring some bells, and I see that it’s more interesting than I suggested above. Rather than a direct transcription of functoriality, the engine of his axiom hierarchy can be written as the following rule (shifting notation a bit)

$\frac{\vdash A} {\vdash (A \to B) \to B}$

which is actually quite similar to your “evaluation” operation! (In my paper there is also an idea which I think is related of a “dni-closed” deductively closed subset [of an “imploid” = thin skew closed category], which serves as an analogue of a normal subgroup. The idea is that closure under double-negation introduction can be seen as a commutation condition necessary for the construction of quotients, and which is satisfied in particular for the subset of elements above the unit.)

]]>
Mike Shulman comments on "closed category" (69186) https://nforum.ncatlab.org/discussion/4632/?Focus=69186#Comment_69186 2018-05-31T12:40:09-04:00 2022-09-27T07:58:19-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ I think of a Hilbert system as a deductive system whose judgments are simply PtrueP\;true (usually written just “PP”) for some proposition PP, with no hypotheticals, and in which most properties ...

I think of a Hilbert system as a deductive system whose judgments are simply $P\;true$ (usually written just “$P$”) for some proposition $P$, with no hypotheticals, and in which most properties of the system are expressed by axioms and often the rule that has premises is modus ponens $\frac{A \to B \quad A}{B}$. But some Hilbert systems have other rules, and it seems like this one could be formulated as $\frac{A_2\to A_1 \quad B_1 \to B_2}{(A_1\to B_1)\to (A_2\to B_2)}$. Is that right?

]]>