Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: type in the meta-theory v.s. term of a type

Noah Chrein (Apr 10 2024 at 19:12):

Hello, I am new to type theory, I mostly spend my time in formal category theory. I'm reading up on New and Licata's virtual equipment type theory and I realized I've just never asked the following question.

what is real the difference between "claiming something is a type" $T \;\;\text{Type}$ and saying something is a term in the type of types $T:Type$? I'm not talking about "size" issues, i.e. universes. More generally, I don't understand why we distinguish between claiming something is part of the meta-theory and typing relations. In this paper they model the type theory of the equipment of categories and profunctors:

So $\text{Cat}$ is a feature of the meta theory and they write "$\mathbb C \;\;\text{Cat}$" why not consider a type of categories and say something like "$\mathbb C:\text{Cat}$"?

Do we write $A\;\; B$ when $B$ is a feature of the meta theory and $A$ is an instance of $B$ and $a:A$ just when $a$ a term of $A$? Is there a way to write something like this $a:A:B$ and be precise? I.e. consolidate the features of the meta-theory and the types into different "levels" of typing relations? Is this what two level type theories seek to do? if so why stop at 2?

Why can't I write "$c : \mathbb C : \text{Cat}:\text{equip}$" for "an object c in the category of categories which is an equipment" and be precise?

Thank you for any insight.

Mike Shulman (Apr 10 2024 at 19:18):

The point is that a particular type theory may or may not contain a "universe" type whose elements are other types. The judgment $T \, \mathsf{type}$ is ontologically on the same status as $t : T$, but different, and doesn't require there to be any universe type.

Mike Shulman (Apr 10 2024 at 19:20):

The collection of all types in the object theory is indeed a type (or set) in the metatheory (depending on what the metatheory is), but it would be confusing to mix the typing colon of the object theory with the typing colon of the metatheory.

Julius Hamilton (Apr 10 2024 at 19:21):

And there is no way to get rid of the need for a meta-theory? Because Noah asks above “why stop at level 2”.

Mike Shulman (Apr 10 2024 at 19:26):

When we reason in some theory, there is no need for a metatheory; we simply reason in the theory. When we reason about some theory, we need to be reasoning in some other theory, and that other theory is the metatheory. Usually we don't need to simultaneously reason about the theory we are using to reason about some other theory.

Mike Shulman (Apr 10 2024 at 19:29):

But one certainly could.

Julius Hamilton (Apr 10 2024 at 19:32):

Isn’t it very common for there to be a type of types, in most type theories?

Mike Shulman (Apr 10 2024 at 19:37):

It's common in Martin-Lof style dependent type theories. But it's impossible in simple type theories, and for theories in between with limited amount of dependency like VETT one has to be careful with it. Taking such care often entails formally separating the judgment that something is a type from the judgment that it is an element of a type of types. In particular, it's almost never the case that one type of types can contain all types as its elements, due to size paradoxes, so it's useful to have a syntactic notion of "being a type" that's distinct from belonging to a type of types.

Julius Hamilton (Apr 10 2024 at 19:42):

Why do dependent type theories require a type of types? In order to express a “type signature” for functions on types?

Mike Shulman (Apr 10 2024 at 19:42):

They do not require it.

Mike Shulman (Apr 10 2024 at 19:43):

But it's useful to internally express polymorphic operations, as you suggest.

Mike Shulman (Apr 10 2024 at 19:43):

It's also used to talk generically about propositions and predicates, when represented using propositions-as-types.

Julius Hamilton (Apr 10 2024 at 19:44):

If propositions are types, and terms are proofs, then predicates are second-level (dependent) types?

Mike Shulman (Apr 10 2024 at 19:44):

It can be used in "encode-decode" style arguments to characterize equalities and other properties of inductive types. For instance, it ordinary MLTT without a type of types, it's not possible to prove that $0\neq 1$.

Mike Shulman (Apr 10 2024 at 19:44):

And in univalent type theories, it's used to build classifying spaces.

Mike Shulman (Apr 10 2024 at 19:45):

A predicate is a function to the type of propositions.

Noah Chrein (Apr 10 2024 at 19:46):

I have some more questions, when I get back to my computer I'll ask more. But thank you two for the discussion this is getting at what I'm asking

Julius Hamilton (Apr 10 2024 at 19:54):

Ordinarily, a proposition $P$ is actually just a variable in the set $\{0, 1\}$. A predicate is sort of like a function, except it needs a quantifier. Then it becomes a function from $x$ to $\{0, 1\}$.

If types are already propositions, what remains for predicates to “act on”? The terms are proofs of the propositions. There aren’t any “referents”.

Mike Shulman (Apr 10 2024 at 19:54):

By "ordinarily" I guess you mean "in set theory".

Mike Shulman (Apr 10 2024 at 19:55):

In type theory, a proposition is an element of a type of "propositions". This might be the whole type of types, or some sub-type of it consisting only of the subsingletons, but whatever it is, let's call it $\mathsf{Prop}$. If we assume the law of excluded middle, then $\mathsf{Prop}$ will have exactly two elements.

Mike Shulman (Apr 10 2024 at 19:56):

A predicate on a type $A$ is then a function $A \to \mathsf{Prop}$, sending each element $x:A$ to the proposition $P(x)$ that the predicate holds of $x$.

Mike Shulman (Apr 10 2024 at 19:57):

The phrase is "propositions as types", not "types as propositions". Not every type is a proposition; even if as $\mathsf{Prop}$ we use the universe of all types, not every type is treated as a proposition in practice. Types also play the role of sets in set theory, as the carriers of structure and the domains of predicates.

Julius Hamilton (Apr 10 2024 at 20:00):

So in one single “universe of types”, we have types whose terms have varying interpretations - some are like classes of objects - others are taken to represent “proofs” of a proposition?

Noah Chrein (Apr 10 2024 at 20:12):

I'm trying to imagine a meta type theory whose "types" are all (oo,n)-categories for all levels n. This way one could write, as a simple example
$c:\mathbb C:\mathbb C \text{at}:2\mathbb C \text{at}:3\mathbb C \text{at}$ for an object c of a category, in the 2 category of categories, all "witnessed" by 3 categories as:

here $\bullet$ is the 1 object 1category, 2category, 3category respectively. I.e. $\bullet \overset c \to \mathbb C:\mathbb C\text{at}$ is an object of $\mathbb C$. So my question is more along the lines of, can I think of typing $c:\mathbb C$ as a generalized object $c$ of $\mathbb C$? Could a type theory accommodate various levels of typing through a mechanism like this?

Mike Shulman (Apr 10 2024 at 20:12):

I would say that all types are collections of objects, and the kind of object they are a collection of depends on the type: function types are collections of functions, number types are collections of numbers, etc. In particular, then, proposition types are collections of proofs.

Mike Shulman (Apr 10 2024 at 20:13):

Noah Chrein said:

Could a type theory accommodate various levels of typing through a mechanism like this?

In theory, yes. Indeed, ordinary dependent type theory already has towers of elements as soon as it has multiple universes, e.g. the smallest universe belongs to the next universe $\mathsf{Type}_0 : \mathsf{Type}_1$, which belongs to the next universe $\mathsf{Type}_1 : \mathsf{Type}_2$, etc.

Noah Chrein (Apr 10 2024 at 20:15):

yes but typically, $\text{Type}_n$ carries no structure, except maybe an oo-groupoid structure or something like that. In my thoughts something like $\mathbb C \text{at}:\text{equip}$ should say that "$\mathbb C \text{at}$ inherits its structural properties from $\text{equip}$"

Noah Chrein (Apr 10 2024 at 20:16):

structural properties being e.g. the existence of a hom profunctor etc

Mike Shulman (Apr 10 2024 at 20:17):

In a type theory with multiple universes, you can have certain operations that only apply to certain universes. E.g. the "hom profunctor" type-former could apply only to types belonging to "equip", therefore including in particular your Cat.

Julius Hamilton (Apr 10 2024 at 20:25):

Ok. So a predicate is a function from any type to the type of propositions. It takes something, and “says something about it”. This is a function type, because there are multiple predicates, and they are all functions. Does that make predicates a dependent type, because they require you to specify the type of the domain?

Noah Chrein (Apr 10 2024 at 20:26):

okay thank you that's interesting, is there somewhere I can read up on this kind of operation, type formers only applying to certain types?

I am thinking of the hom profunctor as a generalized object:

where $\nrightarrow$ is like a "walking" profunctor virtual double category, and this generalized element is more precisely part of some a diagram encoding its universal property.

Mike Shulman (Apr 10 2024 at 21:32):

Julius Hamilton said:

Ok. So a predicate is a function from any type to the type of propositions. It takes something, and “says something about it”. This is a function type, because there are multiple predicates, and they are all functions. Does that make predicates a dependent type, because they require you to specify the type of the domain?

Each predicate is a function. The type of predicates on a type $A$ is thus a function type, namely $A\to \mathsf{Prop}$. If $A$ is a variable belonging to the type of types, rather than a fixed type like $\mathbb{N}$, then yes this is a family of types dependent on the type of types.

Mike Shulman (Apr 10 2024 at 21:34):

Noah Chrein said:

okay thank you that's interesting, is there somewhere I can read up on this kind of operation, type formers only applying to certain types?

Hmm, expressed like that it's such a generic idea that I doubt anyone's written much about it at that level. But you might get some of the flavor of it by reading about, say, [[pure type systems]], which have an arbitrary family of "sorts" along with "rules" for which pairs of sorts the $\Pi$-type can be applied to and produce something in a third sort.

Julius Hamilton (Apr 10 2024 at 21:36):

In a simple type theory, we can declare the existence of various types without claiming those types are part of a type of Types?

Julius Hamilton (Apr 10 2024 at 21:38):

Will we need at least a “type operator” to form product types?

Mike Shulman (Apr 10 2024 at 21:47):

Type-formation rules are written in terms of the judgment "$A \,\mathsf{type}$" of "being a type".

Mike Shulman (Apr 10 2024 at 21:47):

For instance, product types are

$$\frac{A \,\mathsf{type} \qquad B\,\mathsf{type}}{A\times B\,\mathsf{type}}$$

Mike Shulman (Apr 10 2024 at 23:56):

Noah Chrein said:

is there somewhere I can read up on this kind of operation, type formers only applying to certain types?

Here's another example, just posted on the arXiv this month: the paper Primitive Recursive Dependent Type Theory has $\Pi$-types that don't act on the smallest universe, only on the larger ones.

Julius Hamilton (Apr 11 2024 at 00:11):

Is simple type theory a theory in first-order logic?

Julius Hamilton (Apr 11 2024 at 00:18):

I think that first-order logic is a specification language. The variables are understood to take values in a domain of discourse. A collection of statements in first-order logic determine a theory.

Julius Hamilton (Apr 11 2024 at 00:18):

Is the domain of discourse the “universe of types”?

Mike Shulman (Apr 11 2024 at 00:30):

Julius Hamilton said:

Is simple type theory a theory in first-order logic?

No. All type theories are [[deductive systems]], on the same ontological plane with first-order logic itself, not a theory expressed in it.

Noah Chrein (Apr 11 2024 at 00:40):

Wow thank you that paper looks awesome!

Julius Hamilton (Apr 11 2024 at 02:05):

“(1) simply having a deductive system does not in itself necessarily yield an effective procedure for enumerating valid proof trees and theorems. (2) Deductive systems which do yield such an enumeration are sometimes referred to as formal systems.”

Why (1)?

Mike Shulman (Apr 11 2024 at 02:10):

You left off the important first part of that sentence:

Depending on the strength of the metalanguage used to define the judgments and steps

The point is that a general deductive system could have uncountably many rules, or rules with infinitely many premises, which aren't effectively enumerable.

Mike Shulman (Apr 11 2024 at 02:10):

(Assuming it is specified in a metatheory that includes infinity.)

Julius Hamilton (Apr 11 2024 at 02:16):

So you would have a metatheory that is capable of expressing an infinite schema of rules for a deductive system. This may still be an interesting deductive system, but it’s just not “effectively enumerable”.

Julius Hamilton (Apr 11 2024 at 02:18):

And “effectively enumerable” means there is no way to “traverse” them comprehensively, right? Like, it’s ok if they are infinite, as long as you can find a procedure that would, were you to go on, “enumerate all the judgments”.

Julius Hamilton (Apr 11 2024 at 02:20):

Does that mean that type theories can be either deductive systems or formal systems?

Julius Hamilton (Apr 11 2024 at 02:23):

“more general deductive systems are considered in proof theory and type theory, typically because by side-stepping these coding issues one can give a simpler account of computational phenomena such as cut-elimination.”

In what way does avoiding formal systems make it easier to define a cut-elimination rule?

Mike Shulman (Apr 11 2024 at 02:29):

"Effectively enumerable" means there is an algorithm that lists all the deduction trees, in the sense that it might run forever but will eventually get to any one of them. There could be infinitely many of them, as long as they can be listed by an algorithm.

Mike Shulman (Apr 11 2024 at 02:30):

According to the terminology on that page (which I'm not certain is standard in the literature), "formal systems" are a sub-class of "deductive systems", and a type theory in general is a deductive system that might or might not be a formal system.

Mike Shulman (Apr 11 2024 at 02:30):

I don't know what that remark about cut-elimimination means, though.

Julius Hamilton (Apr 11 2024 at 03:36):

Alright. I put it on Stack Exchange: https://cs.stackexchange.com/questions/167527/why-is-it-simpler-to-express-the-cut-elimination-rule-in-general-deductive-syste

I wonder if in a formal system you have to have a very explicit way of writing the cut elimination rule, but since deductive systems are more “relaxed”, you can write it in a more intuitive way.

Julius Hamilton (Apr 11 2024 at 03:38):

So Gödel’s incompleteness theorem only applies to effectively enumerable deductive systems?

Mike Shulman (Apr 11 2024 at 03:40):

It looks like that remark was added in revision #7 in 2012 by Noam Zeilberger, so you could also ask him directly.

Mike Shulman (Apr 11 2024 at 03:40):

Maybe it will work to summon @Noam Zeilberger.

Julius Hamilton (Apr 11 2024 at 04:07):

I’ll have to continue this tomorrow but I was hoping to understand how the concept of judgment differs from logic vs type theory. In logic, propositions are judged true. But in type theory we attempt to form a judgment of a type inhabitant, as $a : A$.

This makes me wonder if there is an implied metaphysics of type theory: it is all about statements of “what exists”, where “truth”(/proof) is just one of the many kinds of existing things. In logic, truth is “outside” the system, in the meta-theory. In type theory, truth is “inside” the system. Right?

Julius Hamilton (Apr 11 2024 at 04:13):

I also read that in the simplest type theories, like Church’s, the only way to construct new types was with functions. Ideas like product types came later.

It seems like type theories have much more formation rules, whereas logic has much more axioms. This reminds me of something I read - Hilbert-style deductive systems have extremely few formation rules (like, substitution), and lots of axioms (like for ZFC); “natural deduction” has a number of formation rules. Type theories tend to use natural deduction. Does this mean that type theories simply don’t have “axioms”, except declaring at the outset the existence of certain atomic types?

Julius Hamilton (Apr 11 2024 at 04:15):

Even then, those formation rules just have to be written in the meta-theory, which is why I feel like the difference is kind of illusory. Besides, can’t it be shown that certain types theories are isomorphic to intuitionistic logic?

Mike Shulman (Apr 11 2024 at 04:22):

Julius Hamilton said:

This makes me wonder if there is an implied metaphysics of type theory: it is all about statements of “what exists”, where “truth”(/proof) is just one of the many kinds of existing things.

I would say that proofs (a.k.a. "witnesses of truth") are one of the many types of existing things.

In logic, truth is “outside” the system, in the meta-theory. In type theory, truth is “inside” the system. Right?

I don't know what you mean by that. In both cases the "truth" judgment resides in the deductive system. If you mean that in logic that's outside any theory that we might formulate inside the logic, then yes.

Mike Shulman (Apr 11 2024 at 04:23):

Logic is really just a kind of type theory where we ignore the witnesses of the truth judgment.

Mike Shulman (Apr 11 2024 at 04:24):

I wouldn't say that logic "has axioms". Ordinarily what has axioms is a theory formulated in logic.

Mike Shulman (Apr 11 2024 at 04:25):

Same for type theories. Really they should be called "type [[doctrines]]", since one can formulate a "theory in MLTT" by asserting some types and terms as axioms in the same way that one can formulate a "theory in FOL" by asserting some propositions and statements as axioms.

Ryan Wisnesky (Apr 11 2024 at 04:27):

I think the "formal systems" remark means that one can use infinitary systems to help simplify tough proofs about finitary ones, such as considering Bohm trees when analyzing lambda calculus normalization

Zoltan A. Kocsis (Apr 11 2024 at 07:28):

Re axioms vs rules:
Somewhat confusingly, there are two different uses of "axiom".
As @Mike Shulman explains above, when mathematicians talk about axioms, they usually mean the axioms of some first-order theory formulated inside first-order logic. However, proof theorists talk differently: in proof-theoretic parlance, an axiom is usually just an unconditional rule of inference of a given proof system.

When we talk about a Hilbert-style deductive system, we usually talk about axioms in the latter sense.
For example, a Hilbert system for propositional logic might have axioms such as

1. Infer ⊢ A → B → A.
2. Infer ⊢ (A → B → C) → (A → B) → A → C.
3. Infer ⊢ ((A → B) → A) → A.
4. From ⊢ A and ⊢A → B infer ⊢B.

Among these four, one would call 1,2,3 axioms since they are unconditional, but not 4 (modus ponens), since it requires you to already have some other derivations before you use it.

Similarly, in a sequent system for propositional logic, we would call the identity inference rule "Infer A ⊢ A" an axiom, whereas we would not call the negation left inference rule "From Γ ⊢Ainfer Γ,¬A⊢ Δ" an axiom.

Usually, the identity rule (schema) is the only axiom in a sequent system, and modus ponens is the only conditional inference rule of a Hilbert-style system. So sequent systems tend to have lots of conditional inference rules but very few axioms, whereas Hilbert systems have many axioms but very few inference rules. Certain presentations of Prawitz-style natural deduction can do away even with the identity rule, so in a certain (handwavy!) sense these are said to have no axioms at all.

Both approaches have benefits and drawbacks, depending on what you wish to prove about your logic. As is well-known, sequent systems are very convenient for proving cut-elimination results. In turn, Hilbert systems are very handy for proof translations where the inductive steps are difficult (since there are a lot fewer of them): for example, the syntactic proof of conservativity of nonstandard analysis uses a very special Hilbert system, where even the quantifier rule is eliminated in favor of additional axioms.

Type theories tend to use natural deduction. Does this mean that type theories simply don’t have “axioms”, except declaring at the outset the existence of certain atomic types?

MLTT is its own system, one that comes with several sorts of judgments. Of the more traditional proof-theoretic systems, its presentation most closely resembles that of natural deduction. However, in my experience, type theory practitioners rarely if ever use the word "axiom" for unconditional inference rules.

This makes me wonder if there is an implied metaphysics of type theory: it is all about statements of “what exists”, where “truth”(/proof) is just one of the many kinds of existing things. In logic, truth is “outside” the system, in the meta-theory. In type theory, truth is “inside” the system. Right?

These are all just ways of speaking, and has no philosophical/metaphysical/ontological implications whatsoever.

The word "true" itself refers to like a hundred different things in mathematical logic, depending on context. None of these senses necessarily has anything to do with the metaphysical concept of truth, not even the Tarskian definition of truth in models. When I make the judgment that⊢ ¬¬A → A, I don't judge that _true_ in any sort of metaphysical sense: I just observe that I managed to derive it in whatever logic I'm considering that day... and "truth" is a convenient shorthand/metaphor that allows me to communicate what I actually did to others.

Zoltan A. Kocsis (Apr 11 2024 at 07:43):

Julius Hamilton said:

“more general deductive systems are considered in proof theory and type theory, typically because by side-stepping these coding issues one can give a simpler account of computational phenomena such as cut-elimination.”

In what way does avoiding formal systems make it easier to define a cut-elimination rule?

I can't be sure whether this is what @noamzoam had in mind, but a classic example of using more general deductive systems over strictly formal systems is Buchholz explaining Gentzen's consistency proof within infinitary proof theory, which gives a simple derivation of the reductions and ordinal assignment used by Gentzen uses in his consistency proof of Peano arithmetic in terms of cut-elimination for an infinitary system which has infinitely branching proof trees.

Noam Zeilberger (Apr 11 2024 at 08:32):

Zoltan A. Kocsis said:

Julius Hamilton said:

“more general deductive systems are considered in proof theory and type theory, typically because by side-stepping these coding issues one can give a simpler account of computational phenomena such as cut-elimination.”

In what way does avoiding formal systems make it easier to define a cut-elimination rule?

I can't be sure whether this is what @_noamzoam had in mind, but a classic example of using more general deductive systems over strictly formal systems is Buchholz explaining Gentzen's consistency proof within infinitary proof theory, which gives a simple derivation of the reductions and ordinal assignment used by Gentzen uses in his consistency proof of Peano arithmetic in terms of cut-elimination for an infinitary system which has infinitely branching proof trees.

Since it was over a decade ago I can't be sure what I meant either, but as I remember this is exactly the kind of thing I had in mind. In addition to Schütte's "little omega" rule (an infinitary rule discussed in that Buchholz paper, which allows you to conclude a universal statement $\forall x.P(x)$ about the natural numbers given proofs of $P(n)$ for all $n \in \mathbb{N}$), there is also Buchholz's big $\Omega$-rule that he introduced in the study of iterated inductive definitions, and which I got interested in during my PhD thesis. If one allows those kinds of rules then proofs may be visualized as trees that are "infinitely wide". But one can also consider proofs that are "infinitely deep", as Buchholz does in that paper making use of Grigorii Mints' "repetition" rule. A proof essentially becomes a program that you can query to progressively reveal bigger and bigger portions of this infinitary proof tree.

Noah Chrein (Apr 11 2024 at 15:14):

Mike Shulman said:

Same for type theories. Really they should be called "type [[doctrines]]", since one can formulate a "theory in MLTT" by asserting some types and terms as axioms in the same way that one can formulate a "theory in FOL" by asserting some propositions and statements as axioms.

This is perhaps another way to ask my question, can one construct a type theory (or something of a similar flavor) that includes all levels of doctrine inside of it? Perhaps, in such a way that the meta-theory itself can be resolved internally. There's a statement in nlab: propositional resizing that says

it is still possible to define a well-pointed cartesian closed lextensive coherent category object with a natural numbers object inside of any well-pointed cartesian closed lextensive coherent category with a natural numbers object.

That is, the meta-theory can specify its own structure and hence, in my naive understanding, handle itself internally.

Mike Shulman (Apr 11 2024 at 15:25):

Any particular sufficiently expressive theory can serve as its own metatheory. You can study ZFC inside of ZFC, or MLTT inside of MLTT, etc.

Mike Shulman (Apr 11 2024 at 15:25):

There are still just 2 levels, it's just that the 2 levels are formally the same theory.

Mike Shulman (Apr 11 2024 at 15:26):

One could try to formulate a notion of an "infinite tower of theories" each serving as the metatheory of the next. I think something like this is envisioned informally in the introduction to Cori and Lascar's book on Mathematical Logic (which also has one of the best explanations of theory/metatheory that I've seen), but I don't think I've seen it written out precisely.

Noah Chrein (Apr 11 2024 at 15:27):

What do you think it would take to make it precise?

Mike Shulman (Apr 11 2024 at 15:28):

I'm not sure what you mean. You'd have to write out a formal mathematical definition.

Noah Chrein (Apr 11 2024 at 15:30):

What kind of structure is necessary to capture the semantics of an infinite tower of theories each serving as a meta-theory of the next? In my work I consider something like a graded quasi virtual equipment, the gradings are essentially (profunctorial) representations of (higher) morphism at each level in this tower of theory. I'm wondering if you've thought about something like this, perhaps as a means of capturing the vague intuition of n-theories.

Mike Shulman (Apr 11 2024 at 15:31):

I have not.

Noah Chrein (Apr 11 2024 at 15:34):

That's okay, I think I am looking for some acute guidance in this particular matter but I'm not sure where to look. I'll take a look at the Cori/Lascar book though and see where that leads

Mike Shulman (Apr 11 2024 at 15:39):

Don't get your hopes too high, I don't think they have a lot to say. (-:

Julius Hamilton (Apr 11 2024 at 15:41):

Rene Cori, Daniel Lascar, Donald H. Pelletier - Mathematical Logic_ A Course with Exercises Part I_ Propositional Calculus, Boolean Algebras, Predicate Calculus, Completeness Theorems -Oxford Universi.pdf

I have part 2 but Zulip says file is too large.

Julius Hamilton (Apr 11 2024 at 15:44):

You’re concerned about the problem of infinite regress, right?

Mike Shulman (Apr 11 2024 at 15:44):

The passage I was thinking of is on page 3 of that file.

Mike Shulman (Apr 11 2024 at 15:45):

(I mean, the page numbered "3", which is the 25th page of the PDF.)

Julius Hamilton (Apr 11 2024 at 16:04):

2 perspectives on philosophy of mathematics that might give Noah ideas.

Chapter 12: Quine and the Web of Belief
Stewart Shapiro_ William J. Wainwright - The Oxford Handbook of Philosophy of Mathematics and Logic-OUP USA (2005).pdf

The idea of “coherentism”. https://plato.stanford.edu/entries/justep-coherence/

Noah Chrein (Apr 11 2024 at 17:39):

I've actually had this exact convo before at wolfram. Imo a type theory that includes all doctrines, and perhaps relaxes the "strictness" of typing relations to, say, structured witnesses of typing relations (i can only posit a toy model of this) could be a basis for coherentism. Nothing is "at the top" and one could imagine webs of typing relations instead of linear hierarchies of typing relations.

Noah Chrein (Apr 11 2024 at 17:42):

There would be a lot of logical soundness problems with doing this naively but tbh this is where my intuitions end

Julius Hamilton (Apr 11 2024 at 22:43):

2010.02752.pdf

Let me know if you want to read or discuss this paper together, I’ve been meaning to study Wolfram’s ‘multiway systems’ for a while

Daniel Geisler (Apr 11 2024 at 23:13):

I corresponded with Wolfram for almost forty years. I think I upset him when I asked if it was appropriate for me to use my Mathematica license to create an index of TWFs for @John Baez. Wolfram recruited me to work on multiway systems, but I didn't feel like moving on the his next "cool" project. Plus he seems to have a large number of bright people in his orbit. He seems to be more concerned about advancing Wolfram than advancing science. I recently had a conversation about Wolfram's Principle of Computational Equivalence not having a proof or that he hasn't produced any peer-reviewed material in forty years. So I am no longer willing to work with Wolfram or Mathematica. I could say much more, but I have more useful things to attend to.

Julius Hamilton (Apr 12 2024 at 00:28):

Awesome

Julius Hamilton (Apr 12 2024 at 00:31):

Is there a formal proof of the statement “any sufficiently expressive theory can serve as its own metatheory”?

Mike Shulman (Apr 12 2024 at 00:38):

Well, it's kind of implicit in the argument leading up to Godel's incompleteness theorems.

Julius Hamilton (Apr 12 2024 at 02:55):

I’m not ready to understand the incompleteness theorem. Could you sketch the argument for the above statement?

Julius Hamilton (Apr 12 2024 at 03:02):

The theory known as true arithmetic consists of all true statements about the standard integers in the language of Peano arithmetic. This theory is consistent and complete, and contains a sufficient amount of arithmetic. However, it does not have a recursively enumerable set of axioms, and thus does not satisfy the hypotheses of the incompleteness theorems.

• Wikipedia

True arithmetic:

The central result on true arithmetic is the undefinability theorem of Alfred Tarski (1936). It states that the set Th(N) is not arithmetically definable. This means that there is no formula φ(x) in the language of first-order arithmetic such that, for every sentence θ in this language, N ⊨ θ if and only if N ⊨ φ(#(θ)) (the numeral of the canonical Gödel number of the sentence θ).

069DAB04-4757-45FB-9B98-D006378137CA.jpg

I can’t see what about these axioms would imply that the theory is not effectively enumerable.

I think it’s saying that true arithmetic is not expressive enough to express the algorithm that could enumerate it.

And the idea is, if we make it more expressive, it could; but then it would become incomplete?

Mike Shulman (Apr 12 2024 at 03:09):

I was referring to the proof of the incompleteness theorem, which involves coding the formulas of a formal system as natural numbers, so that any theory that's expressive enough to talk about the natural numbers can also talk about any effective formal system.

Mike Shulman (Apr 12 2024 at 03:09):

If you want to talk about the incompleteness theorem itself, that should go in another topic.