5
$\begingroup$

This is a question about a structure that can be used to investigate all kind of structures that can be investigated. Many years ago with Joseph Gubeladze we discussed something similar but I only remember it was something more profound than what I am able to ask now.

I'm afraid I cannot say anything sensible about it. All I know is some amount of ($n$-)categorical semantics for type theories, which inspires some vague suggestions like writing down axioms for the relations between entities $a$, $b$, $c$, $d$, ... with the semantical meanings like "$a$ is the theory of proofs of $b$ in $c$", or "$a$ is a description in $b$ of an interpretation of $c$ in $d$", or, in type-theoretic context, "$a$ is a term of type $b$ in the type theory $c$", or, in category-theoretic context, $a\in\hom_b(c,d)$, or $a=\hom_b(c,d)$, or ...

Did anyone write down such axioms and use them to study some properties of such "abstract theories"?

Improve this question
$\endgroup$
6
  • 3
    $\begingroup$ I don't have an exact reference, but in the spirit of what you are describing might be Martin Hyland's Proof theory in the abstract and Categorical proof theory of classical propositional calculus by Bellin et al. These are rather specific, though. $\endgroup$
    – Andrej Bauer
    Commented Jun 29, 2021 at 11:54
  • $\begingroup$ @Andrej thank you! I definitely have to examine both. Besides, their specifics are akin to mine. But I gather there has been not much of a followup activity? $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Jun 29, 2021 at 13:57
  • $\begingroup$ There was quite a bit of activity around categorical models of the Dialectica interpretation, but those focus on semantics, whereas you are asking about a category-theoretic framing of proof theory, as far as I understand. $\endgroup$
    – Andrej Bauer
    Commented Jun 29, 2021 at 18:17
  • 1
    $\begingroup$ @მამუკაჯიბლაძე Could you perhaps check whether the answer below looks genuine? $\endgroup$
    – Stefan Kohl ♦
    Commented Jul 4, 2021 at 20:13
  • 3
    $\begingroup$ @StefanKohl Yes it does, Joseph reminded me of some details of what we then discussed. $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Jul 4, 2021 at 21:20

1 Answer 1

Reset to default
-3
$\begingroup$

მამუკა, მე როგორც მახსოვს, (მაგას "ბადეებს" ვეძახდით) ესეთი არაფორმალურ სურათი გვქონდა: ერთი სტრუქტურის/თეორიის... ა.შ. შესაბამისი ბადე იყო მეორე ბადეში ჩაქარგული. ამ ნაქარგში/ინტერპრეტაციაში ერეოდა მეორე ბადის თავისებურებები და თვისებები, რომლებიც უნდა განცალებული იქნას პირველწყაროს ნაქარგისგან. მნიშვნელოვანია სწორედ განიმარტოს ნაქარგების სიფაქიზის ზრდის მიმართულების ცნება, რომელიც გამოიწვევს პირველწყაროსადმი უფრო და უფრო ზუსტი მიახლოებების ცნებას.

Improve this answer
$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .