Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 20th 2019
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAndrej Bauer was going to speak about 'General type theories' at the [HoTTEST seminar](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html) but has delayed. One meta-theorem to be proved is > 1. Presupposition theorem: if a judgement is derivable then so are its presuppositions. Does anyone know how 'presupposition' is defined here?

   Andrej Bauer was going to speak about ’General type theories’ at the HoTTEST seminar but has delayed. One meta-theorem to be proved is

   1. Presupposition theorem: if a judgement is derivable then so are its presuppositions.

   Does anyone know how ’presupposition’ is defined here?

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 20th 2019
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSo I see there was considerable discussion at [Initiality Project: plans](https://nforum.ncatlab.org/discussion/9183/initiality-project-type-theory/) with some variation of point of view. Is there anything to draw from this which has a bearing on the discussion of presuppositions in informal settings, as we [discussed once](https://golem.ph.utexas.edu/category/2013/02/have_you_left_off_beating_your.html). I like the idea of making sense of a proposition by constructing a context in which it may be formed.

   So I see there was considerable discussion at Initiality Project: plans with some variation of point of view. Is there anything to draw from this which has a bearing on the discussion of presuppositions in informal settings, as we discussed once. I like the idea of making sense of a proposition by constructing a context in which it may be formed.

3. • CommentRowNumber3.
   • CommentAuthoratmacen
   • CommentTimeJun 20th 2019
   • PermaLink
   Author: atmacen
   Format: MarkdownItexAt the initiality project, I preferred the terms "validity in" and "validity out" for two ways of reducing presuppositions to ordinary logic. These both come in syntactic and semantic versions. Having a "presupposition theorem" indicates that Bauer's framework is using (syntactic) validity out. From your nCafe post, Russell's reading: > There is something which is presently king of France, anything else which is presently king of France is the same as that thing, and it is bald. is an instance of semantic validity out. For "The present king of France is bald." to be valid, the presupposition "There is something which is presently king of France, [and] anything else which is presently king of France is the same as that thing." (or just "There's a unique present king of France.") has to be true. So Russell turned the statement with the presupposition to a statement that instead implies the presupposition, and doesn't itself have any presupposition. The semantic validity in reduction would be "If there's a unique present king of France, it's bald.". (I guess "validity in/out" are pretty bad terms for general presuppositions. At initiality project, the presuppositions were things like context validity and type validity.) Jon Sterling had a blog, which disappeared, but it had a post about presuppositions. He cited something about "invincible quantifiers" or something, which supposedly has to do with the semantic validity in and out reductions. A lot of his blog is on the Wayback machine, but apparently not that post. Maybe he'll show up and remind me. I bring it up because it sounded like a categorical explanation of the reductions.

   At the initiality project, I preferred the terms “validity in” and “validity out” for two ways of reducing presuppositions to ordinary logic. These both come in syntactic and semantic versions. Having a “presupposition theorem” indicates that Bauer’s framework is using (syntactic) validity out.

   From your nCafe post, Russell’s reading:

   There is something which is presently king of France, anything else which is presently king of France is the same as that thing, and it is bald.

   is an instance of semantic validity out.

   For “The present king of France is bald.” to be valid, the presupposition “There is something which is presently king of France, [and] anything else which is presently king of France is the same as that thing.” (or just “There’s a unique present king of France.”) has to be true. So Russell turned the statement with the presupposition to a statement that instead implies the presupposition, and doesn’t itself have any presupposition.

   The semantic validity in reduction would be “If there’s a unique present king of France, it’s bald.”. (I guess “validity in/out” are pretty bad terms for general presuppositions. At initiality project, the presuppositions were things like context validity and type validity.)

   Jon Sterling had a blog, which disappeared, but it had a post about presuppositions. He cited something about “invincible quantifiers” or something, which supposedly has to do with the semantic validity in and out reductions. A lot of his blog is on the Wayback machine, but apparently not that post. Maybe he’ll show up and remind me. I bring it up because it sounded like a categorical explanation of the reductions.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 21st 2019
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThanks for this. It sounds rather like: Someone makes a claim $P$. We look for a context in which it makes sense, say $\Gamma \vdash P true$. Then the Russellian 'validity out' approach turns this into a large dependent sum made from $\Gamma$ and $P$, while the 'validity in' approach forms a dependent product out of the dependent sum that is $\Gamma$ and $P$.

   Thanks for this. It sounds rather like:

   Someone makes a claim $P$. We look for a context in which it makes sense, say $\Gamma \vdash P true$. Then the Russellian ’validity out’ approach turns this into a large dependent sum made from $\Gamma$ and $P$, while the ’validity in’ approach forms a dependent product out of the dependent sum that is $\Gamma$ and $P$.

5. • CommentRowNumber5.
   • CommentAuthoratmacen
   • CommentTimeJun 21st 2019
   • PermaLink
   Author: atmacen
   Format: MarkdownItexYes, that sounds about right. But the technical point of the reductions is to avoid some extra typing-like machinery in the first place. BTW when dealing with type theory itself, the presuppositions have to do with judgments, not types. So to analyze the use of judgment presuppositions in terms of a typing context, this would be a context in a metalanguage or [[logical framework]], using a judgments-as-types representation. So for example the judgment that some object-level context is valid, is a type in the metalanguage, which can be put in a metalanguage context. (This would be *not* using HOAS. If you use HOAS, you don't deal with object language contexts.)

   Yes, that sounds about right. But the technical point of the reductions is to avoid some extra typing-like machinery in the first place.

   BTW when dealing with type theory itself, the presuppositions have to do with judgments, not types. So to analyze the use of judgment presuppositions in terms of a typing context, this would be a context in a metalanguage or logical framework, using a judgments-as-types representation. So for example the judgment that some object-level context is valid, is a type in the metalanguage, which can be put in a metalanguage context. (This would be not using HOAS. If you use HOAS, you don’t deal with object language contexts.)